Today I had to prove some tautologies as an exercise, one of them was:

(Ga)->(Fb) equivalent aU(b v ¬a)

It is clear that I have to prove the implication in both ways. After putting into negation normal form i get that:

F(¬a v b) -> aU(b v ¬a) and viceversa.

I managed to prove the opposite implication, since aU(b v ¬a) implies that at some point we will either see b or ¬a, but I couldn't get around proving the other direction. I am sure it is because we have a and ¬a on the opposing sites of U, but the reasoning is not clear to me.

Can someone clear this up for me?


1 Answer 1


Let us try to prove that $F(\neg a \vee b) \rightarrow a\,\mathcal{U}\,(b \vee \neg a)$ is a tautology. For this, we have to show that every word that is a model of $F(\neg a \vee b)$ is also a model of $a\,\mathcal{U}\,(b \vee \neg a)$

Let $i \in \mathbb{N}$ be the least index of the word for which we have $w^i \models (\neg a \vee b)$, where $w^i$ denotes taking a word $w_0 w_1 w_2 \ldots$ and removing all letters up to $w_{i-1}$. By the assumption that $w \models F(\neg a \vee b)$, we know that such an index exists, so we can pick the least such index. Because $i$ is the least such index, we know that for all $0 \leq j < i$, we have $w^j \not\models (\neg a \vee b)$, and hence $w^j \models a \wedge \neg b$ and also also $w^j \models a$.

So we know that $w^i \models (\neg a \vee b)$ and for all $0 \leq j<i$, we have $w^j \models a$. By the definition of the until operator, we thus have $w \models a\,\mathcal{U}\,(\neg a \vee b)$.

  • $\begingroup$ Thank you for your response. You made a small error in your last statement, probably wanted to say w^j entails a, not w^i :) $\endgroup$
    – Stefan
    Jan 18, 2018 at 21:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.