# is (infinitely often p) ∨ (infinitely often ¬p) valid?

i'm trying to prove every trace over PROP = {p} is a model of the formula. I am very stuck in figuring out a model pi that satisfies this formula, can anyone point me in the right direction?

The LTL formula for the given problem could be: $$G(F(p)) \lor G(F(\lnot p))$$. Consider a $$\omega$$-word $$w = w_1w_2w_3 \ldots$$ over $$\{\{\}, \{p\}\}$$:

Let $$w_i = w_iw_{i+1}\ldots$$ \begin{align*} & \; \; \; \; \; \; \; \; \; w \not\models G(F(p))\\ &\implies \exists i . w_i \not\models F(p)\\ &\implies \exists i. \forall j \geq i . w_j \models \lnot p\\ &\implies \exists i. \forall j \geq i . w_j \models F(\lnot p)\\ &\implies \exists i. w_i \models G(F(\lnot p))\\ &\implies w \models G(F(p)) \lor G(F(\lnot p)) \end{align*}

Therefore, $$G(F(p)) \lor G(F(\lnot p))$$ is valid.

Note that this doesn't mean that $$G(F(p)) \land G(F(\lnot p))$$ is not satisfiable. For example, consider the word $$w=\{p\}\{\}\{p\}\{\}\{p\}\{\}\ldots$$

• You're using $w_i$ to mean two different things. Commented May 22, 2020 at 7:48
• @YuvalFilmus By convention $w_i \models \psi$ means the first position of $w_i$ satisfies $\psi$. So, can you elaborate why you think I meant two different things by $w_i$... Commented May 22, 2020 at 7:51
• You wrote $w_i = w_i w_{i+1} \dots$ Commented May 22, 2020 at 7:51
• I am still missing where did I use anything other than $w_i = w_iw_{i+1}\ldots$... Commented May 22, 2020 at 7:53
• My only complaint is that $w_i$ signifies both an $\omega$-word and a single state. If this is common in the relevant community, then that's fine. Commented May 22, 2020 at 7:59

Consider a model $$\pi$$. Let $$T$$ be the set of times at which $$p$$ holds. If $$T$$ is infinite, then "infinitely often $$p$$" holds. If $$\overline{T}$$ is infinite, then "infinitely often $$\lnot p$$" holds. One of these two must hold, since there are infinitely many times.

You can use logical equivalences to show this is a valid LTL formula over models with the proposition $$p \in \mathrm{Prop}$$.

\begin{aligned} &\mathsf{G}\mathsf{F} p \vee \mathsf{G}\mathsf{F}\neg{}p\\ &= \langle \mathsf{GF}\varphi \vee \mathsf{GF}\psi \equiv \mathsf{G}(\mathsf{F}\varphi \vee \mathsf{F}\psi) \rangle\\ &\mathsf{G}(\mathsf{F} p \vee \mathsf{F}\neg{}p)\\ &= \langle \mathsf{F}\varphi \vee \mathsf{F}\psi \equiv \mathsf{F}(\varphi \vee \psi) \rangle\\ &\mathsf{G}\mathsf{F}( p \vee \neg{}p)\\ &= \langle\text{excluded middle} + p \in \mathrm{Prop} \rangle\\ &\mathsf{G}\mathsf{F}\top\\ &= \langle \mathsf{F}\top \equiv \top \rangle\\ &\mathsf{G}\top\\ &= \langle \mathsf{G}\top \equiv \top \rangle\\ &\top \end{aligned}

Most of the above equivalences are fairly easy to show by unfolding the semantics. The only annoying part is showing the $$\mathsf{G}(\mathsf{F} \varphi \vee \mathsf{F}\psi) \Rightarrow \mathsf{G}\mathsf{F} \varphi \vee \mathsf{G}\mathsf{F}\psi$$ direction of $$\mathsf{G}\mathsf{F} \varphi \vee \mathsf{G}\mathsf{F}\psi \equiv \mathsf{G}(\mathsf{F} \varphi \vee \mathsf{F}\psi)$$.

(see also A Calculational Deductive System for Linear Temporal Logic for a nice list of LTL theorems)