This article includes a list ofgeneral references, butit lacks sufficient correspondinginline citations. Please help toimprove this article byintroducing more precise citations.(August 2023) (Learn how and when to remove this message)

Tarski's undefinability theorem, stated and proved byAlfred Tarski in 1933, is an important limitative result inmathematical logic, thefoundations of mathematics, and in formalsemantics. Informally, the theorem states that "arithmetical truth cannot be defined in arithmetic".^[1]

The theorem applies more generally to any sufficiently strongformal system, showing that truth in the standard model of the system cannot be defined within the system.

In 1931,Kurt Gödel published theincompleteness theorems, which he proved in part by showing how to represent the syntax of formal logic withinfirst-order arithmetic. Each expression of the formal language of arithmetic is assigned a distinct number. This procedure is known variously asGödel numbering,coding and, more generally, as arithmetization. In particular, varioussets of expressions are coded as sets of numbers. For various syntactic properties (such asbeing a formula,being a sentence, etc.), these sets arecomputable. Moreover, any computable set of numbers can be defined by some arithmetical formula. For example, there are formulas in the language of arithmetic defining the set of codes for arithmetic sentences, and for provable arithmetic sentences.

The undefinability theorem shows that this encoding cannot be done forsemantic concepts such as truth. It shows that no sufficiently rich interpreted language can represent its own semantics. A corollary is that anymetalanguage capable of expressing the semantics of some object language (e.g. a predicate is definable inZermelo-Fraenkel set theory for whether formulae in the language ofPeano arithmetic are true in the standard model of arithmetic^[2]) must have expressive power exceeding that of the object language. The metalanguage includes primitive notions, axioms, and rules absent from the object language, so that there are theorems provable in the metalanguage not provable in the object language.

The undefinability theorem is conventionally attributed toAlfred Tarski. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1933 publication of Tarski's work (Murawski 1998). While Gödel never published anything bearing on his independent discovery of undefinability, he did describe it in a 1931 letter toJohn von Neumann. Tarski had obtained almost all results of his 1933 monographThe Concept of Truth in the Languages of the Deductive Sciences between 1929 and 1931, and spoke about them to Polish audiences. However, as he emphasized in the paper, the undefinability theorem was the only result he did not obtain earlier. According to the footnote to the undefinability theorem (Twierdzenie I) of the 1933 monograph, the theorem and the sketch of the proof were added to the monograph only after the manuscript had been sent to the printer in 1931. Tarski reports there that, when he presented the content of his monograph to the Warsaw Academy of Science on March 21, 1931, he expressed at this place only some conjectures, based partly on his own investigations and partly on Gödel's short report on the incompleteness theorems "Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit" [Some metamathematical results on the definiteness of decision and consistency],Austrian Academy of Sciences, Vienna, 1930.

We will first state a simplified version of Tarski's theorem, then state and prove in the next section the theorem Tarski proved in 1933.

Let${\displaystyle L}$ be the language offirst-order arithmetic. This is the theory of thenatural numbers, including their addition and multiplication, axiomatized by thefirst-order Peano axioms. This is a "first-order" theory: thequantifiers extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describerecursively defined integer functions such as exponentiation,factorials or theFibonacci sequence.

Let${\displaystyle \mathbb{N}}$ be the standardstructure for${\displaystyle L}$, i.e.${\displaystyle \mathbb{N}}$ consists of the ordinary set of natural numbers and their addition and multiplication. Each sentence in${\displaystyle L}$ can be interpreted in${\displaystyle \mathbb{N}}$ and then becomes either true or false. Thus${\displaystyle (L,\mathbb{N})}$ is the "interpreted first-order language of arithmetic".

Each formula${\displaystyle \phi }$ in${\displaystyle L}$ has aGödel number${\displaystyle g(\phi )}$. This is a natural number that "encodes"${\displaystyle \phi }$. In that way, the language${\displaystyle L}$ can talk about formulas in${\displaystyle L}$, not just about numbers. Let${\displaystyle T}$ denote the set of${\displaystyle L}$-sentences true in${\displaystyle \mathbb{N}}$, and${\displaystyle T^{\ast }}$ the set of Gödel numbers of the sentences in${\displaystyle T}$. The following theorem answers the question: Can${\displaystyle T^{\ast }}$ be defined by a formula of first-order arithmetic?

Tarski's undefinability theorem (simplified form): There is no${\displaystyle L}$-formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ that defines${\displaystyle T^{\ast }}$.That is, there is no${\displaystyle L}$-formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ such that for every${\displaystyle L}$-sentence${\displaystyle A}$,${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(g(A))⟺A}$ holds in${\displaystyle \mathbb{N}}$.

Informally, the theorem says that the concept of truth of first-order arithmetic statements cannot be defined by a formula in first-order arithmetic. This implies a major limitation on the scope of "self-representation". By working in a stronger system (e.g., by adding a sort of subsets of${\displaystyle \mathbb{N}}$ as insecond-order arithmetic) itis possible to define a formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ which holds on exactly the set${\displaystyle T^{\ast }}$, but that does not define truth for the stronger system. However, this formula only defines a truth predicate for formulas in the original language${\displaystyle L}$ (e.g., because${\displaystyle T^{\ast }}$ does not contain codes for sentences quantifying over subsets of${\displaystyle \mathbb{N}}$). To define truth in this stronger system would require ascending to an even stronger system and so on.

To prove the theorem, we proceed bycontradiction and assume that an${\displaystyle L}$-formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ exists which is true for the natural number${\displaystyle n}$ in${\displaystyle \mathcal{N}}$ if and only if${\displaystyle n}$ is the Gödel number of a sentence in${\displaystyle L}$ that is true in${\displaystyle \mathbb{N}}$. We could then use${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ to define a new${\displaystyle L}$-formula${\displaystyle S(m)}$ which is true for the natural number${\displaystyle m}$ if and only if${\displaystyle m}$ is the Gödel number of a formula${\displaystyle \phi (x)}$ (with a free variable${\displaystyle x}$) such that${\displaystyle \phi (m)}$ is false when interpreted in${\displaystyle \mathbb{N}}$ (i.e. the formula${\displaystyle \phi (x)}$, when applied to its own Gödel number, yields a false statement). If we now consider the Gödel number${\displaystyle g}$ of the formula${\displaystyle S(m)}$, and ask whether the sentence${\displaystyle S(g)}$ is true in${\displaystyle \mathbb{N}}$, we obtain a contradiction. (This is known as adiagonal argument.)

The theorem is a corollary ofPost's theorem about thearithmetical hierarchy, proved some years after Tarski (1933). A semantic proof of Tarski's theorem from Post's theorem is obtained by contradiction as follows. Assuming${\displaystyle T^{\ast }}$ is arithmetically definable, there is a natural number${\displaystyle n}$ such that${\displaystyle T^{\ast }}$ is definable by a formula at level${\displaystyle {\mathrm{\Sigma }}_n^0}$ of thearithmetical hierarchy. However,${\displaystyle T^{\ast }}$ is${\displaystyle {\mathrm{\Sigma }}_k^0}$-hard for all${\displaystyle k}$. Thus the arithmetical hierarchy collapses at level${\displaystyle n}$, contradicting Post's theorem.

Tarski proved a stronger theorem than the one stated above, using an entirely syntactical method. The resulting theorem applies to any formal language withnegation, and with sufficient capability forself-reference that thediagonal lemma holds. First-order arithmetic satisfies these preconditions, but the theorem applies to much more general formal systems, such asZFC.

Tarski's undefinability theorem (general form): Let${\displaystyle (L,\mathcal{N})}$ be any interpreted formal language which includes negation and has a Gödel numbering${\displaystyle g(\phi )}$ satisfying the diagonal lemma, i.e. for every${\displaystyle L}$-formula${\displaystyle B(x)}$ (with one free variable${\displaystyle x}$) there is a sentence${\displaystyle A}$ such that${\displaystyle A⟺B(g(A))}$ holds in${\displaystyle \mathcal{N}}$. Then there is no${\displaystyle L}$-formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ with the following property: for every${\displaystyle L}$-sentence${\displaystyle A,}$${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(g(A))⟺A}$ is true in${\displaystyle \mathcal{N}}$.

The proof of Tarski's undefinability theorem in this form is again byreductio ad absurdum. Suppose that an${\displaystyle L}$-formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(n)}$ as above existed, i.e., if${\displaystyle A}$ is a sentence of arithmetic, then${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(g(A))}$ holds in${\displaystyle \mathcal{N}}$ if and only if${\displaystyle A}$ holds in${\displaystyle \mathcal{N}}$. Hence for all${\displaystyle A}$, the formula${\displaystyle \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(g(A))⟺A}$ holds in${\displaystyle \mathcal{N}}$. But the diagonal lemma yields a counterexample to this equivalence, by giving a "liar" formula${\displaystyle S}$ such that${\displaystyle S⟺\mathrm{\neg }\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}(g(S))}$ holds in${\displaystyle \mathcal{N}}$. This is a contradiction. QED.

The formal machinery of the proof given above is wholly elementary except for the diagonalization which the diagonal lemma requires. The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invokerecursive functions in any way. The proof does assume that every${\displaystyle L}$-formula has aGödel number, but the specifics of a coding method are not required. Hence Tarski's theorem is much easier to motivate and prove than the more celebratedtheorems of Gödel about the metamathematical properties of first-order arithmetic.

Smullyan (1991, 2001) has argued forcefully that Tarski's undefinability theorem deserves much of the attention garnered byGödel's incompleteness theorems. That the latter theorems have much to say about all of mathematics and more controversially, about a range of philosophical issues (e.g.,Lucas 1961) is less than evident. Tarski's theorem, on the other hand, is not directly about mathematics but about the inherent limitations of any formal language sufficiently expressive to be of real interest. Such languages are necessarily capable of enoughself-reference for the diagonal lemma to apply to them. The broader philosophical import of Tarski's theorem is more strikingly evident.

An interpreted language isstrongly-semantically-self-representational exactly when the language containspredicates andfunction symbols defining all thesemantic concepts specific to the language. Hence the required functions include the "semantic valuation function" mapping a formula${\displaystyle A}$ to itstruth value${\displaystyle ||A||}$, and the "semantic denotation function" mapping a term${\displaystyle t}$ to the object it denotes. Tarski's theorem then generalizes as follows:No sufficiently powerful language is strongly-semantically-self-representational.

The undefinability theorem does not prevent truth in one theory from being defined in a stronger theory. For example, the set of (codes for) formulas of first-orderPeano arithmetic that are true in${\displaystyle \mathcal{N}}$ is definable by a formula insecond order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or${\displaystyle n}$-th order arithmetic for any${\displaystyle n}$) can be defined by a formula in first-orderZFC.

• Chaitin's incompleteness theorem – Measure of algorithmic complexityPages displaying short descriptions of redirect targets
• Gödel's completeness theorem – Fundamental theorem in mathematical logic
• Gödel's incompleteness theorems – Limitative results in mathematical logic

• Tarski, A. (1933).Pojęcie Prawdy w Językach Nauk Dedukcyjnych (in Polish). Nakładem Towarzystwa Naukowego Warszawskiego.
• Tarski, A. (1936)."Der Wahrheitsbegriff in den formalisierten Sprachen"(PDF).Studia Philosophica (in German).1:261–405. Archived fromthe original(PDF) on 9 January 2014. Retrieved26 June 2013.
  • Tarski, A. (1983)."The Concept of Truth in Formalized Languages"(PDF). In Corcoran, J. (ed.).Logic, Semantics, Metamathematics. Translated by J. H. Woodger. Hackett. English translation of Tarski's 1936 article.

• Bell, J. L.; Machover, M. (1977).A Course in Mathematical Logic. North-Holland.
• Boolos, G.;Burgess, J.;Jeffrey, R. (2002).Computability and Logic (4th ed.). Cambridge University Press.
• Lucas, J. R. (1961)."Mind, Machines, and Gödel".Philosophy.36 (137):112–27.doi:10.1017/S0031819100057983.S2CID 55408480. Archived fromthe original on 2007-08-19.
• Murawski, R. (1998)."Undefinability of truth. The problem of the priority: Tarski vs. Gödel".History and Philosophy of Logic.19 (3):153–160.doi:10.1080/01445349808837306. Archived fromthe original on 2011-06-08.
• Smullyan, Raymond M. (1992).Gödel's Incompleteness Theorems. Oxford: Oxford University Press, USA.ISBN 0-19-504672-2.
• Smullyan, R. (2001). "Gödel's Incompleteness Theorems". In Goble, L. (ed.).The Blackwell Guide to Philosophical Logic. Blackwell. pp. 72–89.ISBN 978-0-631-20693-4.

• Mathematical logic
• Metatheorems
• Philosophy of logic
• Theorems in the foundations of mathematics
• Theories of truth

• Articles with short description
• Short description is different from Wikidata
• Articles lacking in-text citations from August 2023
• All articles lacking in-text citations
• Articles containing Polish-language text
• Articles containing German-language text
• Pages displaying short descriptions of redirect targets via Module:Annotated link
• CS1 Polish-language sources (pl)
• CS1 German-language sources (de)