Supplement to Temporal Logic

Supplement: An Axiomatic System for CTL

To obtain a complete axiomatization of CTL it suffices to replace the axioms of the linear time temporal logic LTL by their path-quantified versions. For instance, the axioms characterizing the temporal operators \(G\) and \(U\) as fixed points now become:

  • \(\exists G \varphi \leftrightarrow (\varphi \wedge \exists X\exists G \varphi)\);
  • \(\forall G \varphi \leftrightarrow (\varphi \wedge \forall X\forall G \varphi)\);
  • \(\exists(\varphi U\psi) \leftrightarrow (\psi \vee (\varphi \wedge \exists X\exists(\varphi U\psi)))\);
  • \(\forall (\varphi U\psi) \leftrightarrow (\psi \vee (\varphi \wedge \forall X\forall (\varphi U\psi)))\).

The inference rules are modus ponens and the \(\forall G\)-necessitation rule: if \(\vdash \varphi\), then \(\vdash \forall G \varphi\).

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]