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.