Axiomatic Theories of Truth

Origin. Tarski (1933) showed truth is not definable in the object language and drew the hierarchy conclusion. The axiomatic alternative — add a truth predicate and axioms for it, rather than define it — was developed by Feferman (1962, 1991), Friedman and Sheard (1987), Cantini, Halbach (Axiomatic Theories of Truth, 2011), and Horsten. The Kripke–Feferman system axiomatizes what Kripke's fixed-point construction produces semantically.

Models. A base theory, usually PA, extended by a predicate T and axioms saying what it does. The question is not what truth is but what a truth predicate may be assumed to satisfy without contradiction — and the Liar makes that a real constraint rather than a bookkeeping one. Each system is a different answer to which of the intuitive principles to keep.

Formalism.

Base: PA in the language of arithmetic plus a unary predicate T. Gödel coding gives ⌜φ⌝ for each sentence φ.

Disquotation (TB — typed): T(⌜φ⌝) ↔ φ, for φ T-free. Conservative over PA. Adds no strength and little else.

Uniform disquotation (UTB): Same, with free variables. Still conservative.

Compositional (CT — typed, Tarskian): T(⌜¬φ⌝) ↔ ¬T(⌜φ⌝) T(⌜φ ∧ ψ⌝) ↔ T(⌜φ⌝) ∧ T(⌜ψ⌝) T(⌜∀x φ(x)⌝) ↔ ∀n T(⌜φ(n̄)⌝) for T-free φ, ψ. CT with induction restricted to the base language is conservative over PA; with induction extended to the full T-language it proves Con(PA) and is proof-theoretically equivalent to ACA, ordinal ε_{ε₀}. Not ACA₀ — ACA₀ is itself conservative over PA and therefore cannot prove Con(PA); the subscript zero is precisely the restriction of induction that CT-with-full-induction lifts.

Kripke–Feferman (KF — type-free): T applies to sentences containing T. Built to axiomatize Kripke's least fixed point over Strong Kleene. T(⌜¬T(⌜φ⌝)⌝) ↔ T(⌜¬φ⌝) and companions. KF is classical, but its internal logic is not: KF ⊬ T(⌜λ⌝) and KF ⊬ ¬T(⌜λ⌝) for the Liar λ, while KF ⊢ ¬(T(⌜λ⌝) ↔ λ). So KF proves its own truth predicate is not disquotational. Proof-theoretic ordinal: φ_{ε₀}(0), the strength of ramified analysis up to ε₀.

Friedman–Sheard (FS): Keeps full compositionality and both truth rules (from φ infer T⌜φ⌝, and back). ω-inconsistent (McGee): proves each ¬T(⌜φ_n⌝) and also ∃n T(⌜φ_n⌝). Consistent, and no model has the standard numbers.

The trade: No system keeps disquotation, compositionality, classical logic, and type-freedom together. Each named theory is a choice of three.

Symbols.

Metatheory. Conservativity is the philosophical battleground: TB and UTB are conservative over PA, so a deflationist can add the truth predicate without adding strength — and CT with full induction is not conservative, which is taken to show that a truth predicate doing real work is not innocent (Shapiro, Ketland; against Field). KF's ordinal is φ_{ε₀}(0); FS's is φ₂(0), the strength of ramified truth for all finite levels (Halbach), wrapped around an ω-inconsistency. The axiomatic and semantic approaches meet at KF, which stands to Kripke's fixed point as an axiomatization stands to the structure it describes.

Applies to. Deflationism and its conservativeness argument. Formal treatments of the Liar. Proof-theoretic strength of truth principles. Theories of truth in formal semantics and in type theory's universe hierarchies, where the same typed/type-free choice recurs.

Limitations. Every system is a mutilation: something intuitive about truth is given up, and no principled reason selects which. KF is classical but proves its truth predicate non-disquotational, which is close to self-defeat for the motivating intuition. FS is ω-inconsistent, which most readers treat as a refutation rather than a feature. The conservativity argument turns on which base theory and which induction schema are chosen, and the choice is not forced.

© 2026 Lingenic LLC