Tarski's undefinability theorem

Tarski's undefinability theorem. In mathematical logic, Tarski's undefinability theorem, formulated and proven by Alfred Tarski in the 1930s, is a fundamental limitative result about the expressibility of truth. It states, informally, that the concept of truth for the sentences of a given formal language cannot be consistently defined within that same language. More precisely, for a sufficiently strong formal system like Peano arithmetic, there is no formula in the language of the system that can correctly express "is a true sentence." This theorem is deeply connected to Gödel's incompleteness theorems and has profound consequences for the philosophy of language and the foundations of mathematics.

Statement of the theorem

The formal statement of Tarski's theorem requires a precise setting. Let \( \mathcal{L} \) be a formal language capable of expressing a certain amount of arithmetic, such as the language of Peano arithmetic or Zermelo–Fraenkel set theory. Let \( \mathbf{N} \) be a structure, typically the standard model of the natural numbers, that interprets \( \mathcal{L} \). Tarski proved that there is no formula \( \text{True}(x) \) in \( \mathcal{L} \) such that for every sentence \( \phi \) in \( \mathcal{L} \), \( \mathbf{N} \models \phi \) if and only if \( \mathbf{N} \models \text{True}(\ulcorner \phi \urcorner) \). Here, \( \ulcorner \phi \urcorner \) denotes the Gödel numbering of the sentence \( \phi \). This result is often summarized by saying that a consistent formal system of sufficient strength cannot contain its own truth predicate. The theorem relies on techniques similar to those used in the liar paradox and shares a formal structure with the proof of Gödel's first incompleteness theorem.

Historical context and significance

Tarski developed his theorem during a period of intense investigation into the foundations of mathematics, following the discoveries of Kurt Gödel and the work of David Hilbert on Hilbert's program. Gödel's 1931 results demonstrated inherent limitations in formal axiomatic systems, showing that any consistent system containing basic arithmetic is incomplete. Tarski, working at the University of Warsaw and later at the University of California, Berkeley, sought to clarify the nature of semantic concepts like truth and definability. His theorem, presented in his 1933 work "The Concept of Truth in Formalized Languages" and more formally in 1936, established a rigorous, formal barrier to defining truth, separating object language and metalanguage. This work was foundational for the development of model theory and influenced later thinkers like Willard Van Orman Quine and Saul Kripke.

Sketch of the proof

The proof employs a diagonal lemma (or a fixed-point lemma) analogous to that used by Gödel. Assume, for a contradiction, that a formula \( \text{True}(x) \) exists in the language \( \mathcal{L} \) that correctly defines truth for sentences of \( \mathcal{L} \) in the standard model \( \mathbf{N} \). By the diagonal lemma, there exists a sentence \( \lambda \) (a formal version of the liar sentence) such that \( \mathbf{N} \models \lambda \leftrightarrow \neg \text{True}(\ulcorner \lambda \urcorner) \). This sentence \( \lambda \) essentially says "This sentence is not true." Now, if \( \lambda \) is true in \( \mathbf{N} \), then by the property of the truth predicate, \( \text{True}(\ulcorner \lambda \urcorner) \) holds, but the biconditional from the diagonal lemma then implies \( \lambda \) is false—a contradiction. Conversely, if \( \lambda \) is false, then \( \neg \text{True}(\ulcorner \lambda \urcorner) \) holds, making the right side of the biconditional true, which by the lemma means \( \lambda \) is true—again a contradiction. Therefore, the initial assumption that such a truth predicate exists is false.

Consequences and related results

A direct corollary of Tarski's theorem is the undefinability of other semantic notions, such as validity or logical consequence, within the object language itself. It provides a semantic counterpart to Gödel's syntactic incompleteness results; indeed, one can derive a version of Gödel's first incompleteness theorem from Tarski's theorem. The theorem also implies the impossibility of a universal decision procedure for truth in arithmetic, reinforcing the findings of Alonzo Church and Alan Turing on the Entscheidungsproblem. Related limitative results include the Church–Turing thesis on computability and Tarski's theorem on the undefinability of truth in certain non-classical logics. The framework established by Tarski led to the development of hierarchical theories of truth, such as those in the Tarski–Kuratowski algorithm and the work of Solomon Feferman.

Philosophical implications

Tarski's theorem has had a substantial impact on the philosophy of language and analytic philosophy. It is central to discussions about the nature of truth, leading to Tarski's own semantic theory of truth, which employs a metalanguage to define truth for an object language, circumventing the paradox. This approach influenced logical positivists of the Vienna Circle and later philosophers like Donald Davidson, who used it in his theory of meaning. The theorem also raises deep questions about self-reference, the limits of formalization, and the relationship between language and the world. It challenges any simplistic correspondence theory of truth that seeks to be fully formalized within a single linguistic system and remains a key topic in debates on deflationism about truth and the structure of semantic paradoxes. Category:Mathematical logic Category:Theorems in the foundations of mathematics Category:Alfred Tarski