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