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: Fφ → FFφ (time is transitive)
Linearity: PFφ ∨ φ ∨ FPφ (connected)
No beginning: Pφ → PPφ (past has past)
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.

Symbol	Unicode	Name	Meaning
P	—	Past	It was the case
F	—	Future	It will be the case
H	—	Always-past	It always was
G	—	Always-future	It always will be
○	U+25CB	Next	At next moment
●	U+25CF	Previous	At previous moment
U	—	Until	Until (binary)
S	—	Since	Since (binary)

Metatheory. Tense logic = modal logic with two modalities and interaction axioms. Completeness for various frame classes. Decidable for most tense logics. PSPACE-complete typically. Correspondence theory applies. LTL is future fragment. Full tense logic used in philosophy.

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. Linear time assumption strong. Branch-time needs CTL-like extensions. Metric time adds complexity. No standardization across communities. Philosophical debates about time influence formalisms. Less tool support than LTL/CTL.