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?


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)$.

| cite | improve this answer | |
  • $\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 '18 at 21:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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