Supplement to Temporal Logic

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.

Copyright © 2020 by
Valentin Goranko <>
Antje Rumberg <>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing this directive]