Tarski's undefinability theorem
Tarski's undefinability theorem is a fundamental result in mathematical logic, established by Alfred Tarski in 1933, which demonstrates that no consistent formal theory capable of expressing basic arithmetic can contain a definable truth predicate for its own sentences.[1] In precise terms, if a consistent theory T extends the arithmetic of natural numbers (such as Robinson arithmetic), there exists no formula Tr(x) in the language of T such that T proves A ↔ Tr(⌜A⌝) for every sentence A in the language, where ⌜A⌝ denotes the Gödel numeral of A.[1] This theorem formalizes the intuitive idea that truth for a language cannot be captured adequately from within that language itself, requiring instead a richer metalanguage to avoid paradoxes like the liar paradox.[2] The theorem emerged from Tarski's efforts in the early 1930s to provide a rigorous, mathematically precise definition of truth amid the logical positivism movement and concerns over semantical antinomies.[3] It was first articulated in Tarski's Polish-language monograph Pojęcie prawdy w językach nauk dedukcyjnych (1933), with subsequent publications in German as "Der Wahrheitsbegriff in den formalisierten Sprachen" (1935) and an English translation appearing in Logic, Semantics, Metamathematics (1956, revised 1983).[3] Building on Kurt Gödel's incompleteness theorems and diagonalization technique, Tarski's work shifted focus from purely syntactic notions to semantical ones, emphasizing the distinction between object languages and metalanguages.[2] The proof of the theorem employs a fixed-point construction, akin to Gödel's self-reference lemma: assuming a candidate truth predicate Tr(x) exists in the language, one can derive a sentence S such that S ↔ ¬Tr(⌜S⌝) holds by theorem, leading to a contradiction since S cannot be both true and false.[1] This diagonal argument reveals the inherent limitations of sufficiently expressive formal systems, ensuring that truth remains "undefinable" without ascending to a higher-level language.[2] Tarski's undefinability theorem has far-reaching implications for philosophy of language, model theory, and the foundations of mathematics, underscoring the hierarchical nature of semantic definitions and influencing developments in axiomatic truth theories, such as those by Saul Kripke and others seeking to extend Tarski's framework.[3] It also connects to broader limitative results, including Gödel's second incompleteness theorem, by highlighting why consistent theories cannot prove their own consistency without external resources.[1]Background Concepts
Formal Languages and Semantics
A formal language in mathematical logic consists of a finite alphabet of symbols, including logical connectives (such as ¬ for negation, ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for equivalence), quantifiers (∀ for universal quantification and ∃ for existential quantification), variables (e.g., x, y, z), parentheses for grouping, and non-logical symbols specific to the domain, such as constants, function symbols, and predicate symbols.[4] Well-formed formulas (wffs) are defined recursively from these symbols: atomic formulas are predicates applied to terms (where terms are built from constants, functions, and variables), and complex formulas are formed by applying connectives and quantifiers to simpler wffs. Axioms are selected wffs serving as premises, and rules of inference (like modus ponens or generalization) specify how to derive new wffs as theorems from existing ones, forming a deductive system.[1] The distinction between syntax and semantics is fundamental: syntax concerns the formal structure and manipulation of symbols according to rules, independent of meaning, while semantics provides an interpretation that assigns significance to syntactic objects through models.[4] A model, or structure, for a formal language is a domain (a non-empty set) together with interpretations for the non-logical symbols—e.g., constants map to elements of the domain, functions to operations on the domain, and predicates to relations on the domain—allowing the language to describe properties and relations within that domain.[1] Semantics is captured via the notion of satisfaction, where a structure assigns truth values to formulas relative to assignments of values to free variables. Tarski's inductive definition of satisfaction proceeds recursively over the complexity of formulas: an assignment satisfies an atomic formula if it makes the corresponding relation hold in the structure; it satisfies ¬φ if it does not satisfy φ, φ ∧ ψ if it satisfies both φ and ψ, and similarly for other connectives; for ∀x φ, it satisfies ∀x φ if every possible assignment differing only in the value for x satisfies φ.[4] Truth for closed sentences (wffs with no free variables) follows as satisfaction in the structure, yielding Tarski's Convention T: a sentence is true if and only if what it says holds in the model.[1] A canonical example is the first-order language of arithmetic, used in theories like Peano arithmetic, with constant symbol 0 (denoting zero), unary function symbol S (the successor function), binary function symbols + (addition) and × (multiplication), and the equality predicate =.[5] Logical symbols include the connectives and quantifiers mentioned above, enabling expressions like ∀x (S(x) ≠ 0) to axiomatize basic arithmetic properties. Gödel numbering encodes these syntactic elements as natural numbers for metatheoretic analysis.[4]Arithmetic Theories and Satisfaction
Peano arithmetic, often denoted PA, is a first-order theory that formalizes the properties of the natural numbers using a language with symbols for zero (0), successor (S), addition (+), and multiplication (×).[6] Its axioms include: every number has a successor; successor is injective; no number succeeds 0; induction schema, which states that if a property holds for 0 and is preserved under successor, it holds for all numbers; and axioms defining addition and multiplication recursively, such as a + [0](/page/0) = a and a + S(b) = S(a + b).[7] The standard model of PA is the structure \mathbb{N}, consisting of the natural numbers \{[0](/page/0), 1, 2, \dots\} under the usual interpretations of the symbols, where successor maps n to n+1, and operations align with standard arithmetic.[8] A model of PA is any structure \mathcal{M} = (M, 0^\mathcal{M}, S^\mathcal{M}, +^\mathcal{M}, \times^\mathcal{M}) that satisfies all the axioms of PA, with M as its universe, which must be an infinite discrete ordered semiring.[9] While \mathbb{N} is the intended standard model, PA admits non-standard models due to the compactness theorem, which guarantees the existence of models extending any consistent finite subset of axioms.[10] These non-standard models contain "non-standard" elements larger than any standard natural number, yet they satisfy the induction schema internally; for instance, their order type is \mathbb{N} + \mathbb{Z} \cdot Q, embedding \mathbb{N} as an initial segment followed by clusters of non-standard integers dense like the rationals.[11] Countable non-standard models of PA are not necessarily elementarily equivalent to \mathbb{N}. Elementary extensions of \mathbb{N} are elementarily equivalent and non-isomorphic to it, satisfying Th(\mathbb{N}), while other models of PA satisfy only the theorems of PA and may falsify true arithmetic sentences like Con(PA). All such models differ from \mathbb{N} in higher-order properties.[12] Tarski's T-schema provides a foundational condition for defining truth in a model \mathcal{M}: for any sentence \phi, the sentence \ulcorner \phi \urcorner is true in \mathcal{M} if and only if \phi holds in \mathcal{M}, where \ulcorner \phi \urcorner denotes a name for \phi.[4] This schema ensures material adequacy for a truth predicate and is realized through an inductive definition over the complexity of formulas: atomic formulas are true based on the model's interpretation of predicates; truth for negation, conjunction, and other connectives follows recursively; and for quantifiers, \forall x \psi(x) is true if \psi(a) holds for every a \in M.[13] In the context of arithmetic models, this construction yields a robust notion of truth external to the theory itself. The satisfaction relation formalizes how open formulas are evaluated in a model under variable assignments. For a model \mathcal{M}, the relation \mathrm{Sat}_\mathcal{M}(x, v_1, \dots, v_n) holds if the formula encoded by the Gödel number x (with free variables assigned values v_1, \dots, v_n \in M) is satisfied in \mathcal{M} under that assignment.[14] Satisfaction for atomic formulas depends on the model's relations and functions; for compound formulas, it is defined recursively—for example, \mathcal{M} \models \neg \psi[\vec{v}] if not \mathcal{M} \models \psi[\vec{v}], and \mathcal{M} \models \forall y \psi(y, \vec{z})[\vec{v}] if \mathcal{M} \models \psi(a, \vec{v})[v_1, \dots, v_n, a] for all a \in M.[15] Truth for sentences in \mathcal{M} is then satisfaction with no free variables: \mathcal{M} \models \phi if \mathrm{Sat}_\mathcal{M}(\ulcorner \phi \urcorner).[4]Historical Context
Gödel's Incompleteness Theorems
In 1931, Kurt Gödel published two groundbreaking theorems that revealed fundamental limitations of formal axiomatic systems capable of expressing elementary arithmetic. The first incompleteness theorem states that any consistent formal system strong enough to describe basic properties of natural numbers—such as Peano arithmetic—must be incomplete, meaning there exist statements in the system's language that are true but cannot be proved or disproved within the system.[16] This result shattered the hope, inspired by David Hilbert's program, that mathematics could be fully axiomatized in a complete and consistent manner.[16] The second incompleteness theorem extends this limitation by showing that such a formal system cannot prove its own consistency, assuming it is indeed consistent. In other words, if the system is consistent, any proof of its consistency would have to rely on stronger assumptions external to the system itself.[16] This theorem implies that Hilbert's dream of a finitary proof of consistency for arithmetic is unattainable within the arithmetic framework.[16] Gödel's ingenious method relied on arithmetization, or Gödel numbering, which assigns unique natural numbers to syntactic objects like formulas, proofs, and statements within the formal system, thereby encoding metamathematical notions as arithmetic predicates. This encoding allows the system to make statements about its own syntax and provability, enabling the construction of self-referential sentences that mirror informal paradoxes like the liar paradox.[16] A quintessential example is the self-referential Gödel sentence, which asserts its own unprovability, leading to undecidable propositions when the system's consistency is assumed.[16] The logical form of the Gödel sentence G can be expressed through a fixed-point construction asG \equiv \neg \text{Prov}(\ulcorner G \urcorner),
where \text{Prov}(x) is the arithmetic predicate representing provability in the system, and \ulcorner G \urcorner denotes the Gödel number of G.[16] If G is provable, it leads to a contradiction under the assumption of consistency; if unprovable, then G is true, demonstrating incompleteness.[16] These theorems highlighted the intrinsic syntactic limitations of formal systems and paved the way for subsequent investigations into semantic concepts.[16]