Loading [MathJax]/jax/output/HTML-CSS/jax.js

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 Kt

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

  3. Vacuous Generalization: xφφ, if x does not occur free in φ

  4. -Distributivity: x(φψ)(xφxψ)

  5. -Permutation: xyφyxφ

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

  7. Extensionality: xy(x=y(φ[x/z]φ[y/z]))

  8. Necessity of non-equality: xy(xyA(xy))
    (Recall that Aφ=HφφGφ.)

II. Inference rules  (where VD denotes derivability in FOTL(VD)):

  1. Modus Ponens: If VDφψ and VDφ, then VDψ

  2. G-Necessitation: If VDφ, then VDGφ

  3. H-Necessitation: If VDφ, then VDHφ

Copyright © 2020 by
Valentin Goranko <valentin.goranko@philosophy.su.se>
Antje Rumberg <antje.rumberg@uni-tuebingen.de>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.