T Modal Logic

Origin. Robert Feys, "Les logiques nouvelles des modalités" (1937), introduced the system as t; von Wright, An Essay in Modal Logic (1951), arrived at the same logic and called it M. The two names converged on T, presented in Kripke-era notation as KT: the smallest normal modal logic containing □A → A. It is the weakest standard system in which necessity is veridical.

Models. Kripke frames with a reflexive accessibility relation. Reflexivity is exactly what the T axiom demands and exactly what it expresses: a frame validates □A → A iff every world sees itself. Since reflexive relations are serial, T contains D, and every T-frame is a D-frame.

Formalism.

Axioms: K: □(A → B) → (□A → □B). T: □A → A. KT = K + T.

Rules: Modus ponens. Necessitation: from ⊢ A infer ⊢ □A.

Frame condition: Reflexivity: ∀w. wRw. F ⊨ □p → p iff R is reflexive. First-order definable; T is a Sahlqvist formula, hence canonical.

Dual form: A → ◇A. What is true is possible.

Derivable: D: □A → ◇A, since □A → A and A → ◇A. Reflexive ⟹ serial, so KD ⊊ KT.

Not derivable: 4: □A → □□A (needs transitivity). B: A → □◇A (needs symmetry). 5: ◇A → □◇A (needs euclideanness).

Extensions: KT4 = S4 (reflexive, transitive). KTB = B, the Brouwerian system (reflexive, symmetric). KT4B = KT5 = S5 (equivalence relations).

Modalities: Unlike S4, which has 14 distinct modalities, and S5, which has 6, T has infinitely many pairwise non-equivalent modalities: □, □□, □□□, ... are all distinct.

Epistemic reading: □A as "knows A"; T is the factivity axiom KA → A. T is the minimal logic of knowledge — no introspection assumed.

Symbols.

Metatheory. Sound and complete with respect to the class of reflexive Kripke frames; the canonical model for KT is reflexive, so completeness follows by the canonical model construction, and canonicity is automatic since T is Sahlqvist. Reflexivity is elementary — definable by ∀w. wRw — so T is a complete, canonical, elementary logic. It has the finite model property: filtration through the subformulas of φ yields a model of size at most 2^|sub(φ)|, so satisfiability is decidable. Ladner (1977) settled the complexity: satisfiability for K, T, and S4 is PSPACE-complete, in contrast to S5, which is only NP-complete because its models collapse to a single equivalence class. T enjoys Craig interpolation and the Beth definability property. It is a proper sublogic of S4, of KTB, and hence of S5, and a proper extension of KD.

Applies to. Alethic necessity where what must be, is. Epistemic logic as the minimal factive base, before positive or negative introspection is added. Deontic settings only by contrast — T is precisely the axiom deontic logic must reject. Verification conditions read as "holds here and everywhere reachable." Baseline system for comparing frame correspondences.

Limitations. T fixes veridicality and nothing else: it validates no introspection principle, so □A → □□A and ◇A → □◇A both fail, and it cannot express agents who know what they know. Its infinite supply of distinct modalities makes normal-form arguments unavailable — there is no reduction of iterated modalities of the kind S4 and S5 permit. It is unsound for provability: reading □ as PA's provability predicate makes □A → A the reflection schema, which by Löb's theorem PA proves only for the A it already proves, and GL + T proves every formula. As an epistemic logic it inherits the logical omniscience of all normal systems — closure under necessitation and K forces knowledge of all validities — and the choice of T over stronger systems reflects a substantive epistemological position about introspection rather than a technical convenience. Reflexivity is also not reflected by bounded morphisms: tree unravelling produces an irreflexive frame mapping onto a reflexive one, so some standard frame constructions leave the class.

© 2026 Lingenic LLC