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

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