1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ What means the square and the diamond? $\endgroup$ – Paul Ogilvie Dec 9 '18 at 15:54
  • $\begingroup$ @PaulOgilvie en.wikipedia.org/wiki/Temporal_logic#Temporal_operators $\endgroup$ – David Richerby Dec 9 '18 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 Ogilvie Dec 9 '18 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 Richerby Dec 9 '18 at 17:04
  • $\begingroup$ @DavidRicherby. Ah. With "proof" I was looking for a formal proof. $\endgroup$ – Paul Ogilvie Dec 9 '18 at 17:08
2
$\begingroup$

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!

$\endgroup$
  • $\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 '18 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 '18 at 16:47
0
$\begingroup$

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

$\endgroup$
  • $\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 '18 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 '18 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 '18 at 8:54

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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