Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics.
In 1931, Kurt Gödel published the incompleteness theorems, which he proved in part by showing how to represent the syntax of formal logic within first-order arithmetic.
Each expression of the formal language of arithmetic is assigned a distinct number.
This procedure is known variously as Gödel numbering, coding and, more generally, as arithmetization.
The undefinability theorem shows that this encoding cannot be done for semantic concepts such as truth.
It shows that no sufficiently rich interpreted language can represent its own semantics.
A corollary is that any metalanguage capable of expressing the semantics of some object language (e.g. a predicate is definable in Zermelo-Fraenkel set theory for whether formulae in the language of Peano 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.
While Gödel never published anything bearing on his independent discovery of undefinability, he did describe it in a 1931 letter to John von Neumann.
Tarski had obtained almost all results of his 1933 monograph "The 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.
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.
This is the theory of the natural numbers, including their addition and multiplication, axiomatized by the first-order Peano axioms.
The theory is strong enough to describe recursively defined integer functions such as exponentiation, factorials or the Fibonacci sequence.
consists of the ordinary set of natural numbers and their addition and multiplication.
To define a truth predicate for the metalanguage would require a still higher metametalanguage, and so on.
Tarski proved a stronger theorem than the one stated above, using an entirely syntactical method.
The resulting theorem applies to any formal language with negation, and with sufficient capability for self-reference that the diagonal lemma holds.
First-order arithmetic satisfies these preconditions, but the theorem applies to much more general formal systems, such as ZFC.
be any interpreted formal language which includes negation and has a Gödel numbering
The proof of Tarski's undefinability theorem in this form is again by reductio ad absurdum.
But the diagonal lemma yields a counterexample to this equivalence, by giving a "liar" formula
The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invoke recursive functions in any way.
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 enough self-reference for the diagonal lemma to apply to them.
The broader philosophical import of Tarski's theorem is more strikingly evident.
Tarski's theorem then generalizes as follows: No sufficiently powerful language is strongly-semantically-self-representational.
For example, the set of (codes for) formulas of first-order Peano arithmetic that are true in
Similarly, the set of true formulas of the standard model of second order arithmetic (or