# Validity of □(P→ Q) → (◊P → ◊Q) in linear temporal logic

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

• – David Richerby Dec 9 '18 at 15:56
• @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. – Paul Ogilvie Dec 9 '18 at 16:39
• @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. – David Richerby Dec 9 '18 at 17:04
• @DavidRicherby. Ah. With "proof" I was looking for a formal proof. – Paul Ogilvie Dec 9 '18 at 17:08
• @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. – David Richerby Dec 9 '18 at 17:13

## 3 Answers

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!

• 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 – zhou ziyao Dec 9 '18 at 17:52
• @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. – DCTLib Dec 10 '18 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).

• 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. – Pål GD Dec 10 '18 at 22:07
• 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). – Sue Dec 10 '18 at 23:40
• True, but the validity of the original statement would still hold: □(P→Q)→(◊P→◊Q). – Pål GD Dec 11 '18 at 8:54
• @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) – miracle173 Dec 28 '20 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.