In some circumstances, existence cannot be expressed in linear temporal logic. I don't understand why it can't be constructed with negations and global quantifiers.

For example, the wikipedia page (https://en.wikipedia.org/wiki/Linear_temporal_logic) states that:

No formula in LTL can define the language that is defined by the CTL formulas AG( p → (EXq ∧ EX¬q) ) or AG(EF(p)).

Why isn't the CTL formula AG(EF(p)) equivalent to the LTL formula G(¬G(¬p)) ?

  • Are you sure this is a philosophy question? This is more of a programming question than philosophy. That said, LTL is a subset of CTL which is in-turn a subset of CTL*, however, just because LTL is a subset it does not mean every relation holding in LTL holds in the supersets as well. My two cents. – Bertrand Wittgenstein's Ghost Dec 3 '18 at 6:21

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.