Tarski Undefinability of Truth

Origin. Tarski (1933, 1936). Arithmetical truth is not arithmetically definable. The semantic counterpart of Gödel incompleteness and the formal resolution of the Liar paradox.

Models. No formula in the language of arithmetic defines the set of Gödel numbers of true sentences. A language cannot contain its own truth predicate on pain of contradiction.

Formalism.

Diagonal lemma: For any φ(x) there is a sentence ψ with ⊢ ψ ↔ φ(⌜ψ⌝). Self-reference via arithmetization.

Undefinability theorem: No formula True(x) satisfies N ⊨ True(⌜φ⌝) ↔ φ for all sentences φ.

Proof: Suppose True(x) exists. Diagonalize on ¬True(x): get ψ ↔ ¬True(⌜ψ⌝). Then ψ is true iff not true — contradiction.

Object vs metalanguage: Truth for a language is definable only in a stronger metalanguage. Tarski hierarchy of languages.

Partial truth predicates: Truth for Σ_n sentences is Σ_n-definable. Full truth is not definable at any fixed level.

T-schema: True(⌜φ⌝) ↔ φ, as a material adequacy condition.

Symbols.

Symbol	Unicode	Name	Meaning
True(x)	—	Truth predicate	Alleged definition of truth
⌜φ⌝	—	Gödel number	Code of sentence φ
N	—	Standard model	Natural numbers
↔	U+2194	Biconditional	Material equivalence
⊢	U+22A2	Derivability	Diagonal lemma is proved inside the theory
⊨	U+22A8	Satisfaction	N ⊨ True(⌜φ⌝) ↔ φ, the condition shown unsatisfiable
¬	U+00AC	Negation	Diagonalization is applied to ¬True(x)
ψ	U+03C8	Psi	The self-referential sentence produced by diagonalization
φ	U+03C6	Phi	Arbitrary sentence in the T-schema
Σ_n	—	Sigma level	Partial truth predicate exists at each fixed level

Metatheory. The proof rests on the diagonal lemma, available in any theory interpreting Robinson's Q: for every φ(x) there is a ψ with ⊢ ψ ↔ φ(⌜ψ⌝). Diagonalizing ¬True(x) shows that Th(N), the set of Gödel numbers of true arithmetical sentences, is not arithmetical — not Σ⁰ₙ or Π⁰ₙ for any n — even though for each fixed n a partial predicate correctly evaluates all Σ⁰ₙ sentences, so truth escapes the hierarchy without escaping any single level of it. Provability in a recursively axiomatized theory is by contrast Σ⁰₁-definable, and Tarski's derivation of Gödel's first incompleteness theorem turns on exactly that mismatch. The same argument runs in set theory: no formula Tr(x) satisfies ZFC ⊢ Tr(⌜φ⌝) ↔ φ for all φ, though Σₙ-satisfaction is definable for each n. Adding compositional truth axioms without extending induction to the truth predicate is conservative over PA (Kotlarski, Krajewski and Lachlan, 1981); extending induction to it proves Con(PA).

Applies to. Theory of truth. Semantic paradoxes. Foundations of model theory. Reflection principles and hierarchies.

Limitations. The theorem is conditional on resources. It needs a language in which syntax can be arithmetized and a theory interpreting Robinson's Q, and says nothing about weaker systems: Presburger arithmetic is complete and decidable and supports no diagonal construction. It is also purely negative — it shows that no formula of the object language defines the truth set, not that the set fails to exist, and not what truth is. What is proved inconsistent is the package of classical logic, the unrestricted T-schema, and self-reference, and the theorem does not adjudicate which member to give up: Kripke's fixed-point construction keeps a self-applicative predicate by abandoning bivalence, revision theories by abandoning the biconditional as a stable truth condition, paraconsistent treatments by abandoning explosion. The hierarchy of metalanguages never closes, and neither its starting point nor the length of its iteration is fixed by the result.