## Supplement: Some Variations of the Axiomatic System for LTL

Note that (GFP$$_G$$) generalizes the induction axiom (IND): $$\varphi \wedge G(\varphi \rightarrow X\varphi)\rightarrow G\varphi$$. In fact, the axiom (GFP$$_G$$) can be replaced by the following induction rule, which is deducible in the system above:

• If $$\vdash \psi \rightarrow \varphi \land X\psi$$, then $$\vdash \psi \rightarrow G\varphi$$.

Likewise, (LFP$$_U$$) can be replaced by the following derivable rule:

• If $$\vdash (\psi \vee (\varphi \wedge X\theta)) \rightarrow \theta$$, then $$\vdash \varphi U \psi \rightarrow \theta$$.

Moreover, after defining $$G p$$ as $$\lnot (\top U \lnot p)$$, the axioms (FP$$_G$$) and (GFP$$_G$$) become deducible from the rest.

This is a file in the archives of the Stanford Encyclopedia of Philosophy.