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$ @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
  • $\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 Richerby Dec 9 '18 at 17:13
4
$\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
0
$\begingroup$

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.
$\endgroup$

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.