Tense Logic

Origin. Prior introduced tense logic (1957, 1967). Time as modal operators: past and future. P (it was the case), F (it will be the case). Philosophically motivated: McTaggart's A-series. Foundation for temporal logic in CS (linear time).

Models. Past and future as modalities. Modal logic for time: accessibility is temporal succession. P and F are past and future operators. G (always future), H (always past). Time may be linear, branching, discrete, dense, etc.

Formalism.

Basic operators:

• Pφ: "it was the case that φ" (past)
• Fφ: "it will be the case that φ" (future)
• Hφ: "it has always been that φ" (always past)
• Gφ: "it will always be that φ" (always future)

Duality: P = ¬H¬, F = ¬G¬ Like ◇ = ¬□¬ in modal logic.

Frame conditions:

• Transitivity: FFφ → Fφ (time is transitive)
• Linearity: PFφ → (Pφ ∨ φ ∨ Fφ) (future-connected, no forward branching; dually FPφ → (Pφ ∨ φ ∨ Fφ) is past-connected)
• No beginning: Hφ → Pφ (every moment has a predecessor)
• Density: Fφ → FFφ (between any two moments, another)
• Discreteness: Fφ → ○Fφ ∨ ○φ (next moment exists)

Prior's axioms:

• G(φ → ψ) → (Gφ → Gψ) (K for G)
• H(φ → ψ) → (Hφ → Hψ) (K for H)
• φ → GPφ (if now, then always-after was)
• φ → HFφ (if now, then always-before will be)

Metric tense: P_n φ: "n time units ago, φ" F_n φ: "in n time units, φ"

Symbols.

Metatheory. The minimal tense logic Kt — K for G, K for H, together with φ → GPφ and φ → HFφ — is sound and complete with respect to the class of all frames (W, R), with G read along R and H along its converse. Both converse axioms are Sahlqvist, hence canonical, and Kt has the finite model property, is decidable, and its satisfiability problem is PSPACE-complete. Correspondence theory applies unchanged: transitivity is FFφ → Fφ, density is Fφ → FFφ, and having no last moment is Gφ → Fφ. Kamp's theorem (1968) settles expressiveness for the binary operators: over Dedekind-complete linear orders, Until and Since are expressively complete for first-order logic in one free variable over <, and over arbitrary linear orders they are not, Stavi's two additional connectives being required to restore completeness. Gabbay's separation theorem (1981) states that over such orders every formula is a Boolean combination of pure-past, pure-present, and pure-future formulas. Burgess and Gurevich (1985) proved the temporal logic of the real line decidable.

Applies to. Philosophy of time. Natural language tense analysis. Action and event semantics. Planning (reasoning about past/future). Temporal databases (historical queries). Narrative and discourse. Legal reasoning (temporal provisions).

Limitations. The Priorean operators are strictly weaker than the binary ones: Until is not definable from F, P, G, and H, so the language of Prior's original systems falls short of first-order expressive completeness even over ℕ. Nor can it distinguish the flows most often at issue — Dedekind completeness has no tense correspondent, so (ℚ, <) and (ℝ, <) validate exactly the same F/P-formulas, and no axiom separates the rationals from the reals. Irreflexivity is not definable by any tense formula, and neither is the existence of an immediate successor, so discreteness has to be imposed by adding ○ as a primitive rather than by an axiom. Metric operators P_n and F_n destroy the finite model property. Lifting to first order is fatal for axiomatizability: first-order tense logic over ℕ is not recursively enumerable.

© 2026 Lingenic LLC