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

5 events

when toggle format	what		by	license	comment
Dec 28, 2020 at 16:30	comment	added	miracle173		@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)
Dec 11, 2018 at 8:54	comment	added	John Kemeny		True, but the validity of the original statement would still hold: □(P→Q)→(◊P→◊Q).
Dec 10, 2018 at 23:40	comment	added	Sue		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).
Dec 10, 2018 at 22:07	comment	added	John Kemeny		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.
Dec 10, 2018 at 21:35	history	answered	Sue	CC BY-SA 4.0