Supplement to Temporal Logic

Supplement: Axioms for the Minimal FOTL with \(E\): the Free Logic Version

Here we abandon the classical rules for the quantifiers and adopt the rules of Free Logic instead, which is a logic that allows for terms that do not refer to any existing entity (cf. the entry on free logic). The application of the rule of Universal Instantiation is restricted by adding the predicate \(E\) for ‘existence at the current time instant’ and the rule of Universal Generalization is modified accordingly:

  • Universal Instantiation (\(\forall\)-Elimination):
    \(\vdash \forall x \varphi(x) \to (E(y) \to \varphi[y/x])\), where \(y\) does not occur free in \(\varphi\).

  • Universal Generalization (\(\forall\)-Introduction):
    If \(\vdash \psi \to (E(x) \to \varphi(x))\), then \(\vdash \psi \to \forall x \varphi(x)\), where \(x\) does not occur free in \(\psi\).

Thus, formulae like \(\exists x G (x=\tau)\), \(G \exists x(x=\tau)\), and \(\forall y G \exists x G (x=y)\) are no longer derivable.

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