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

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free