How can I prove that $\Box(P\rightarrow Q)\rightarrow (\Diamond P\rightarrow\Diamond Q)$ is valid in linear temporal logic (LTL)?
$\begingroup$
$\endgroup$
6
-
$\begingroup$ @PaulOgilvie en.wikipedia.org/wiki/Temporal_logic#Temporal_operators $\endgroup$– David RicherbyCommented 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$– Paul OgilvieCommented 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$– David RicherbyCommented Dec 9, 2018 at 17:04
-
$\begingroup$ @DavidRicherby. Ah. With "proof" I was looking for a formal proof. $\endgroup$– Paul OgilvieCommented 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$– David RicherbyCommented Dec 9, 2018 at 17:13
|
Show 1 more comment
3 Answers
$\begingroup$
$\endgroup$
2
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!
answered Dec 9, 2018 at 15:55
-
$\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$ Commented 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$– DCTLibCommented Dec 10, 2018 at 16:47
$\begingroup$
$\endgroup$
4
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:
- □(P→Q)
Assume for conditional proof, i.e. P→Q is true at any t in D - ◊P
Assume for conditional proof, i.e. P is true at some t in D - P
◊-Elimination on line 2, i.e. index at t1 where P is true - P→Q
□-Elimination on line 1, i.e. at t1 since P→Q true at any t in D - Q
MP on lines 3 and 4, at t1 - ◊Q
◊P-Introduction on line 5, at t1 - ◊P→◊Q
Discharge ◊P for conditional proof - □(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:
- □P
Assume for conditional proof - P
□-Elimination on line 1, at time t2 - ◊P
◊-Introduction on line 2, at t2 - □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:
- ◊(P→Q)
From T-Replacement - ◊P
Assume for conditional proof - P
◊-Elimination on line 2, i.e. index at t3 where P→Q is true - 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
t1has no successor, then □P is true for every P, and ◊P is true for no P. $\endgroup$ Commented 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$– SueCommented Dec 10, 2018 at 23:40
-
$\begingroup$ True, but the validity of the original statement would still hold: □(P→Q)→(◊P→◊Q). $\endgroup$ Commented 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$ Commented Dec 28, 2020 at 16:30
$\begingroup$
$\endgroup$
I suggest 2 methods to prove validity of $\Phi$:
- 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.
- 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.
