# Prove that $\text{EF p}$ can't be written in LTL

Why can't we somehow represent it's negation in LTL and go from there? I think maybe because it has (effectively) two existential quantifiers, so negating it does not work. But how do I prove it?

There is a delicate point here, about the semantics of LTL vs CTL.

Given a formula $$\psi$$ in LTL, we say that it holds in a structure $$K$$ if every path in $$K$$ satisfies $$\psi$$.

In CTL, however, the path quantifiers are built in to the formula.

To make this more precise, you can think of LTL as the fragment of CTL* of the form $$A\psi$$, where $$\psi$$ doesn't contain any path quantifiers (i.e., it's in LTL).

Now, you suggest negating your formula, so you obtain $$AG\neg p$$. This formula is not an LTL formula, due to the quantifier $$A$$. But it does have an LTL equivalent, namely $$G\neg p$$.

However, if you try to negate back to CTL, the negation of the LTL formula is now $$Fp$$, but the semantic of LTL means that it is interpreted as $$AFp$$, whereas you wanted $$EFp$$.

To sum up, you just cannot express the path quantifier $$E$$ in LTL.

To prove that the formula $$EFp$$ does not have an LTL equivalent, consider (towards a contradiction) some equivalent LTL formula $$\psi$$, and take a structure that has two "branches" -- one with $$p$$ and one without (e.g., two states with self loops). Since this structure satisfies the $$EFp$$, then it also satisfies $$\psi$$, meaning that every computation in it satisfies $$\psi$$. But now, if you remove one of the branches (the one with $$p$$), then $$\psi$$ is still satisfied (since you only removed computations). However, $$EFp$$ is not satisfies, so $$\psi$$ is not its equivalent.