How can I prove that $\Box(P\rightarrow Q)\rightarrow (\Diamond P\rightarrow\Diamond Q)$ is valid in linear temporal logic (LTL)?

  • $\begingroup$ @PaulOgilvie en.wikipedia.org/wiki/Temporal_logic#Temporal_operators $\endgroup$ Dec 9, 2018 at 15:56
  • $\begingroup$ @DavidRicherby, thank you for your reference. As for your answer, it is intuitively clear that if P->Q is Globally true, then when at some future moment P becomes true then Q will be/become true. However, with the axioms I cannot prove the statement. In particular, I can't find a rule that G->F. $\endgroup$ Dec 9, 2018 at 16:39
  • $\begingroup$ @PaulOgilvie The question says nothing about axioms. I argued (informally) that every model of $\Box(P\to Q)$ is also a model of $Diamond P\to\Diamond Q$, which means that everything is a model of the implication. $\endgroup$ Dec 9, 2018 at 17:04
  • $\begingroup$ @DavidRicherby. Ah. With "proof" I was looking for a formal proof. $\endgroup$ Dec 9, 2018 at 17:08
  • $\begingroup$ @PaulOgilvie So make my informal proof formal. And... are you the asker? If so, please merge your accounts. It's really confusing to post stuff under two completely different names. $\endgroup$ Dec 9, 2018 at 17:13

3 Answers 3


Think about what the formula means. The first part says that it's always true that $P$ implies $Q$; the second part says that, if $P$ is true somewhere, then $Q$ must be true somewhere, too. Well, if $P$ implies $Q$ then, if $P$ is true somewhere, then $Q$ had better be true in that place, too!

  • $\begingroup$ Can u be more specific? I know the meaning of the formula. But i dont know how to prove second part from the first one. Thx $\endgroup$
    – zhou ziyao
    Dec 9, 2018 at 17:52
  • 1
    $\begingroup$ @zhouziyao Actually, this answer contains exactly the proof idea, just written down slightly informally (but with all non-trivial steps included). Now, you only need to put this into formal notation and you have a proof. $\endgroup$
    – DCTLib
    Dec 10, 2018 at 16:47

Take this with a grain of salt, since I'm not sure what sort of inference rules you're allowed to use. Assuming the domain D is times t with standard ordering, I'd say:

  1. □(P→Q)
    Assume for conditional proof, i.e. P→Q is true at any t in D
  2. ◊P
    Assume for conditional proof, i.e. P is true at some t in D
  3. P
    ◊-Elimination on line 2, i.e. index at t1 where P is true
  4. P→Q
    □-Elimination on line 1, i.e. at t1 since P→Q true at any t in D
  5. Q
    MP on lines 3 and 4, at t1
  6. ◊Q
    ◊P-Introduction on line 5, at t1
  7. ◊P→◊Q
    Discharge ◊P for conditional proof
  8. □(P→Q)→◊P→◊Q
    Discharge □(P→Q) for conditional proof

Note, in one of the comments it was suggested proving □P→◊P might help. Here's a proof of that:

  1. □P
    Assume for conditional proof
  2. P
    □-Elimination on line 1, at time t2
  3. ◊P
    ◊-Introduction on line 2, at t2
  4. □P→◊P
    Discharge □P for conditional proof

Then by substitution, you can infer □(P→Q)→◊(P→Q). Call this T-Replacement. But I don't think that would be useful in proving □(P→Q)→◊P→◊Q. To see why, suppose you've inferred ◊(P→Q) from □(P→Q) by T-Replacement. Then:

  1. ◊(P→Q)
    From T-Replacement
  2. ◊P
    Assume for conditional proof
  3. P
    ◊-Elimination on line 2, i.e. index at t3 where P→Q is true
  4. P→Q
    ◊-Elimination on line 1, i.e. index at t4 where P→Q is true

But you can't combine lines 3 and 4 to use MP since they're indexed to different times. I don't think you can infer ◊P→◊Q from ◊(P→Q).

  • $\begingroup$ I don't think □P→◊P is valid (perhaps it is in LTL?). But if a state t1 has no successor, then □P is true for every P, and ◊P is true for no P. $\endgroup$
    – Pål GD
    Dec 10, 2018 at 22:07
  • $\begingroup$ I was assuming every t has a unique successor. Without that, there are bigger problems, it seems. If it's possible for a t1 to have no successor, then you can't prove □(P→Q)→(P→Q). But then I don't think you can prove ◊P→◊Q from □(P→Q). $\endgroup$
    – Sue
    Dec 10, 2018 at 23:40
  • $\begingroup$ True, but the validity of the original statement would still hold: □(P→Q)→(◊P→◊Q). $\endgroup$
    – Pål GD
    Dec 11, 2018 at 8:54
  • $\begingroup$ @PålGD □P→◊P is valid in LTL, every state has a successor in LTL but even if we allow states with no successors then ◊P is true if □P because the future states referenced by the ◊ operator include the present state. (Michael Huth, Mark Ryan: Logic in Computer Science) $\endgroup$
    – miracle173
    Dec 28, 2020 at 16:30

I suggest 2 methods to prove validity of $\Phi$:

  1. Proof by contradiction. Assume we can falsify $\Phi$, prove that actually it is impossible to achieve.The clue in https://cs.stackexchange.com/a/101284/88420 shows how to do it.
  2. Assume $\Phi$ valid, prove the unsatisfiability of $\neg \Phi$. Using a calculi probably we should derive $\phi \wedge \neg \phi$. A tool can confirm it, but I couldn't derive it by hand.

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.