Tarski's undefinability theorem

Tarski's undefinability theorem
Name	Tarski's undefinability theorem
Field	Mathematical logic
Proposer	Alfred Tarski
Year	1936
Status	proven

Tarski's undefinability theorem states that truth in sufficiently rich formal languages cannot be defined within those languages. Originating in the 1930s, it complements results by Kurt Gödel and Emil Post and clarifies limits on self-reference for theories like Peano arithmetic, Zermelo–Fraenkel set theory, and systems used in the foundations of Hilbert's program. The theorem has deep connections to the work of Gödel, Church, Kleene, Turing, and von Neumann.

Statement

Tarski proved that for any formal system strong enough to represent basic arithmetic—examples include Peano arithmetic, Zermelo–Fraenkel set theory, and extensions by primitive recursive functions—there is no formula in the language of that system that defines the semantic predicate "truth" for the sentences of that same language. The theorem is commonly formulated: no arithmetical formula of the language of Peano arithmetic can capture the class of Gödel numbers of sentences true in the standard model of arithmetic. This result complements Gödel's incompleteness theorems and interacts with Church's thesis, Turing's halting problem, and Kleene's recursion theory.

Historical background

Tarski announced the result in the 1930s while working at the University of Warsaw and later at University of California, Berkeley; its development is tied to his work on the concept of truth in formalized languages. The theorem was motivated by earlier paradoxes such as the Liar paradox and by foundational investigations led by Hilbert and the collaboration of logicians including Gödel, Church, and Turing. Subsequent exposition and formal refinement were influenced by logicians like Kleene, Skolem, Hermann Weyl, and Alonzo Church.

Proofs and techniques

Proofs of the theorem employ diagonalization and self-reference techniques similar to those used by Gödel and Turing; they use arithmetization of syntax via Gödel numbering and primitive recursive encodings developed by Gödel, Herbrand, and Skolem. One common approach constructs, for any putative truth-defining formula, a sentence that asserts of its own Gödel number that it is not in the extension defined by that formula, producing a contradiction in the style of the Liar paradox and Gödel sentence. Technical tools include the arithmetical hierarchy from Kleene and methods from recursion theory as developed by Post and Turing. Alternative proofs use model-theoretic techniques related to Łoś's theorem, compactness, and properties of arithmetical hierarchy and Kreisel's work on definability.

Consequences and related results

Tarski's theorem implies that semantic concepts like "truth" escape internal capture in theories as expressive as Peano arithmetic or Zermelo–Fraenkel set theory, reinforcing Gödel's incompleteness theorems and relating to Church's undecidability results and Turing's halting problem. It motivates separations between syntactic provability (as in Hilbert's program) and semantic truth (as in Frege's earlier logicism), and it influences the development of model theory and proof theory pursued by logicians such as Tarski himself, Henkin, and Robinson. The theorem also interacts with classification results like the arithmetical hierarchy and with definability theorems from Beth and Lindström.

Applications and interpretations

Beyond foundational impact on theories like Peano arithmetic and Zermelo–Fraenkel set theory, Tarski's result informs contemporary fields that handle formal truth and semantics, including computer science areas influenced by Turing and Church—for instance, limits on specification languages in formal verification and constraints on truth predicates in formal ontology used by researchers at institutions like MIT and Stanford University. Philosophical interpretations by scholars influenced by Wittgenstein, Quine, and Putnam address the distinction between object language and meta-language formalized by Tarski, shaping debates in analytic philosophy and the philosophy of mathematics connected to Husserl and Carnap.

Formalizations and generalizations

Tarski's theorem has been formalized in many contexts: within Peano arithmetic and fragments like Robinson arithmetic; in set-theoretic frameworks such as Zermelo–Fraenkel set theory including variants with Choice; and in higher-order contexts using tools from model theory and category theory explored by researchers affiliated with Princeton University and Bonn. Generalizations include undefinability results for truth predicates in typed languages, extensions to modal and intuitionistic logics studied by scholars at University of Oxford and University of Cambridge, and connections to later results by Kripke on partially defined truth and by Feferman on reflective closure. These formalizations refine the boundary between truth, definability, and computability established by Tarski, Gödel, Church, and Turing.

Category:Mathematical logic