Supplement to Temporal Logic

Supplement: Axiomatic System FOTL(VD) for the Minimal FOTL with Varying Domain Semantics

The axiomatic system below is an adaptation of similar axiomatic systems that can be found in Rescher and Urquhart (1971, Chapter XX) and McArthur (1976, Chapter 4).

I. Axiom schemes:

  1. All axioms of the minimal propositional temporal logic \(\mathbf{K}_{t}\)

  2. Restricted Universal Instantiation (\(\forall\)-Elimination):
    \(\forall y(\forall x \varphi(x) \rightarrow \varphi[y/x])\), for any \(y\) free for substitution for \(x\) in \(\varphi\)

  3. Vacuous Generalization: \(\forall x \varphi \leftrightarrow \varphi\), if \(x\) does not occur free in \(\varphi\)

  4. \(\forall\)-Distributivity: \(\forall x (\varphi \rightarrow \psi) \rightarrow (\forall x \varphi \to \forall x \psi)\)

  5. \(\forall\)-Permutation: \(\forall x \forall y \varphi \rightarrow \forall y \forall x \varphi\)

  6. Reflexivity of equality: \(\forall x (x = x)\)

  7. Extensionality: \(\forall x \forall y (x = y \rightarrow (\varphi[x/z] \rightarrow \varphi[y/z]))\)

  8. Necessity of non-equality: \(\forall x\forall y(x \neq y \rightarrow A (x \neq y))\)
    (Recall that \(A \varphi = H \varphi \land \varphi \land G \varphi\).)

II. Inference rules  (where \(\vdash_{\mathrm{VD}}\) denotes derivability in FOTL(VD)):

  1. Modus Ponens: If \(\vdash_{\mathrm{VD}} \varphi \rightarrow \psi\) and \(\vdash_{\mathrm{VD}} \varphi\), then \(\vdash_{\mathrm{VD}} \psi\)

  2. \(G\)-Necessitation: If \(\vdash_{\mathrm{VD}} \varphi\), then \(\vdash_{\mathrm{VD}} G \varphi\)

  3. \(H\)-Necessitation: If \(\vdash_{\mathrm{VD}} \varphi\), then \(\vdash_{\mathrm{VD}} H \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