Tarski's indefinability theorem
Encyclopedia
Tarski's undefinability theorem, stated and proved by Alfred Tarski
in 1936, is an important limitative result in mathematical logic
, the foundations of mathematics
, and in formal semantics
. Informally, the theorem states that arithmetical truth cannot be defined in arithmetic.
The theorem applies more generally to any sufficiently strong formal system
, showing that truth in the standard model of the system cannot be defined within the system.
published his famous incompleteness theorems
, which he proved in part by showing how to represent syntax within first-order arithmetic. Each expression of the language of arithmetic is assigned a distinct number. This procedure is known variously as Gödel numbering, coding, and more generally, as arithmetization.
In particular, various sets of expressions are coded as sets of numbers. It turns out that for various syntactic properties (such as being a formula, being a sentence, etc.), these sets are computable. 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 for semantical 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
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 to Alfred Tarski
. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1936 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 to John von Neumann
. Tarski had obtained almost all results of his 1936 paper Der Wahrheitsbegriff in den formalisierten Sprachen 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 not obtained by him earlier. According to the footnote of the undefinability theorem (Satz I) of the 1936 paper, the theorem and the sketch of the proof were added to the paper only after the paper was sent to print. When he presented the paper to the Warsaw Academy of Science on March 21 1931, he wrote only some conjectures instead of the results after his own investigations and partly after Gödel's short report on the incompleteness theorems "Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit", Akd. der Wiss. in Wien, 1930.
Let L be the language of first-order arithmetic, and let N be the standard structure
for L. Thus (L, N) is the "interpreted first-order language of arithmetic." Let T denote the set of L-sentences true in N, and T* the set of code numbers of the sentences in T. The following theorem answers the question: Can T* be defined by a formula of first-order arithmetic?
Tarski's undefinability theorem: There is no L-formula True(x) which defines T*.
That is, there is no L-formula True(x) such that for every L-formula x, True(x) ↔ x is true.
Informally, the theorem says that given some formal arithmetic, the concept of truth in that arithmetic is not definable using the expressive means that arithmetic affords. This implies a major limitation on the scope of "self-representation." It is possible to define a formula True(x) whose extension is T*, but only by drawing on a metalanguage
whose expressive power goes beyond that of L, second-order arithmetic
for example.
The theorem just stated is a corollary of Post's theorem
about the arithmetical hierarchy
, proved some years after Tarski (1936). A semantic proof of Tarski's theorem from Post's theorem is obtained by reductio ad absurdum
as follows. Assuming T* is arithmetically definable, there is a natural number n such that T* is definable by a formula at level
of the arithmetical hierarchy
. However, T* is
-hard for all k. Thus the arithmetical hierarchy collapses at level n, contradicting Post's theorem.
, 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.
Proof
of Tarski's undefinability theorem in its most general form, by reductio ad absurdum
. Suppose that an L- formula True(x) defines T*. In particular, if A is a sentence of arithmetic then True("A") is true in N iff
A is true in N. Hence for all A, the Tarski T-sentence True("A") ↔ A is true in N. But the diagonal lemma yields a counterexample to this equivalence: the "Liar" sentence S such that S ↔ ¬True("S") holds. Thus no L-formula True(x) can define T*. QED.
The formal machinery of this proof is wholly elementary except for the diagonalization
that the diagonal lemma requires. The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invoke recursive function
s in any way. The proof does assume that every L-formula has a Gö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 celebrated theorems of Gödel
about the metamathematical properties of first-order arithmetic.
(1991, 2001) has argued forcefully that Tarski's undefinability theorem deserves much of the attention garnered by Gö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 enough self-reference
for the diagonal lemma to apply to them. The broader philosophical import of Tarski's theorem is more strikingly evident.
An interpreted language is strongly-semantically-self-representational exactly when the language contains predicates
and function symbols defining all the semantic concepts specific to the language. Hence the required functions include the "semantic valuation function" mapping a formula A to its truth value ||A||, and the "semantic denotation function" mapping a term 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-order Peano arithmetic that are true in N is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC.
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
in 1936, is an important limitative result in mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
, and in formal semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
. Informally, the theorem states that arithmetical truth cannot be defined in arithmetic.
The theorem applies more generally to any sufficiently strong formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
, showing that truth in the standard model of the system cannot be defined within the system.
History
In 1931, Kurt GödelKurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
published his famous incompleteness theorems
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
, which he proved in part by showing how to represent syntax within first-order arithmetic. Each expression of the language of arithmetic is assigned a distinct number. This procedure is known variously as Gödel numbering, coding, and more generally, as arithmetization.
In particular, various sets of expressions are coded as sets of numbers. It turns out that for various syntactic properties (such as being a formula, being a sentence, etc.), these sets are computable. 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 for semantical concepts such as truth. It shows that no sufficiently rich interpreted language can represent its own semantics. A corollary is that any metalanguage
Metalanguage
Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...
capable of expressing the semantics of some object language
Object language
An object language is a language which is the "object" of study in various fields including logic, linguistics, mathematics and theoretical computer science. The language being used to talk about an object language is called a metalanguage...
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 to Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1936 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 to John von Neumann
John von Neumann
John von Neumann was a Hungarian-American mathematician and polymath who made major contributions to a vast number of fields, including set theory, functional analysis, quantum mechanics, ergodic theory, geometry, fluid dynamics, economics and game theory, computer science, numerical analysis,...
. Tarski had obtained almost all results of his 1936 paper Der Wahrheitsbegriff in den formalisierten Sprachen 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 not obtained by him earlier. According to the footnote of the undefinability theorem (Satz I) of the 1936 paper, the theorem and the sketch of the proof were added to the paper only after the paper was sent to print. When he presented the paper to the Warsaw Academy of Science on March 21 1931, he wrote only some conjectures instead of the results after his own investigations and partly after Gödel's short report on the incompleteness theorems "Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit", Akd. der Wiss. in Wien, 1930.
Statement of the theorem
We will first state a simplified version of Tarski's theorem, then state and prove in the next section the theorem Tarski actually proved in 1936.Let L be the language of first-order arithmetic, and let N be the standard structure
Structure (mathematical logic)
In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations which are defined on it....
for L. Thus (L, N) is the "interpreted first-order language of arithmetic." Let T denote the set of L-sentences true in N, and T* the set of code numbers of the sentences in T. The following theorem answers the question: Can T* be defined by a formula of first-order arithmetic?
Tarski's undefinability theorem: There is no L-formula True(x) which defines T*.
That is, there is no L-formula True(x) such that for every L-formula x, True(x) ↔ x is true.
Informally, the theorem says that given some formal arithmetic, the concept of truth in that arithmetic is not definable using the expressive means that arithmetic affords. This implies a major limitation on the scope of "self-representation." It is possible to define a formula True(x) whose extension is T*, but only by drawing on a metalanguage
Metalanguage
Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...
whose expressive power goes beyond that of L, second-order arithmetic
Second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
for example.
The theorem just stated is a corollary of Post's theorem
Post's theorem
In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.- Background :The statement of Post's theorem uses several concepts relating to definability and recursion theory...
about the arithmetical hierarchy
Arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
, proved some years after Tarski (1936). A semantic proof of Tarski's theorem from Post's theorem is obtained by reductio ad absurdum
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
as follows. Assuming T* is arithmetically definable, there is a natural number n such that T* is definable by a formula at level
of the arithmetical hierarchyArithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
. However, T* is
-hard for all k. Thus the arithmetical hierarchy collapses at level n, contradicting Post's theorem.General form of the theorem
Tarski proved a stronger theorem than the one stated above, using an entirely syntactical method. The resulting theorem applies to any formal language with negationNegation
In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is true when that proposition is false, and vice versa. In classical logic negation is normally identified...
, and with sufficient capability for self-reference
Self-reference
Self-reference occurs in natural or formal languages when a sentence or formula refers to itself. The reference may be expressed either directly—through some intermediate sentence or formula—or by means of some encoding...
that the diagonal lemma
Diagonal lemma
In mathematical logic, the diagonal lemma or fixed point theorem establishes the existence of self-referential sentences in certain formal theories of the natural numbers -- specifically those theories that are strong enough to represent all computable functions...
holds. First-order arithmetic satisfies these preconditions, but the theorem applies to much more general formal systems.
Proof
Proof
Proof may refer to:* Proof , sufficient evidence or argument for the truth of a proposition* Formal proof* Mathematical proof, a convincing demonstration that some mathematical statement is necessarily true...
of Tarski's undefinability theorem in its most general form, by reductio ad absurdum
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
. Suppose that an L- formula True(x) defines T*. In particular, if A is a sentence of arithmetic then True("A") is true in N iff
IFF
IFF, Iff or iff may refer to:Technology/Science:* Identification friend or foe, an electronic radio-based identification system using transponders...
A is true in N. Hence for all A, the Tarski T-sentence True("A") ↔ A is true in N. But the diagonal lemma yields a counterexample to this equivalence: the "Liar" sentence S such that S ↔ ¬True("S") holds. Thus no L-formula True(x) can define T*. QED.
The formal machinery of this proof is wholly elementary except for the diagonalization
Diagonalization
In mathematics, diagonalization may refer to:* Diagonal matrix, which is in a form with nonzero entries only on the main diagonal* Diagonalizable matrix, which can be put into a form with nonzero entries only on the main diagonal...
that the diagonal lemma requires. The proof of the diagonal lemma is likewise surprisingly simple; for example, it does not invoke recursive function
Recursive function
Recursive function may refer to:*Recursion , a procedure or subroutine, implemented in a programming language, whose implementation references itself*A total computable function, a function which is defined for all possible inputs...
s in any way. The proof does assume that every L-formula has a Gödel number
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...
, but the specifics of a coding method are not required. Hence Tarski's theorem is much easier to motivate and prove than the more celebrated theorems of Gödel
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
about the metamathematical properties of first-order arithmetic.
Discussion
SmullyanRaymond Smullyan
Raymond Merrill Smullyan is an American mathematician, concert pianist, logician, Taoist philosopher, and magician.Born in Far Rockaway, New York, his first career was stage magic. He then earned a BSc from the University of Chicago in 1955 and his Ph.D. from Princeton University in 1959...
(1991, 2001) has argued forcefully that Tarski's undefinability theorem deserves much of the attention garnered by Gö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
John Lucas (philosopher)
- Overview :John Lucas was educated at Winchester College and Balliol College, Oxford, where he studied first mathematics, then Greats , obtaining first class honors, and proceeding to an MA in Philosophy in 1954. He spent the 1957-58 academic year at Princeton University, deepening his...
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
Self-reference
Self-reference occurs in natural or formal languages when a sentence or formula refers to itself. The reference may be expressed either directly—through some intermediate sentence or formula—or by means of some encoding...
for the diagonal lemma to apply to them. The broader philosophical import of Tarski's theorem is more strikingly evident.
An interpreted language is strongly-semantically-self-representational exactly when the language contains predicates
Predicate (grammar)
There are two competing notions of the predicate in theories of grammar. Traditional grammar tends to view a predicate as one of two main parts of a sentence, the other being the subject, which the predicate modifies. The other understanding of predicates is inspired from work in predicate calculus...
and function symbols defining all the semantic concepts specific to the language. Hence the required functions include the "semantic valuation function" mapping a formula A to its truth value ||A||, and the "semantic denotation function" mapping a term 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-order Peano arithmetic that are true in N is definable by a formula in second order arithmetic. Similarly, the set of true formulas of the standard model of second order arithmetic (or n-th order arithmetic for any n) can be defined by a formula in first-order ZFC.