Editing Tarski's undefinability theorem (section)

==Statement==
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 <math>L</math> be the language of [[first-order arithmetic]]. This is the theory of the [[Natural number|natural numbers]], including their addition and multiplication, axiomatized by the [[Peano axioms#First-order theory of arithmetic|first-order Peano axioms]]. This is a "[[First-order logic|first-order]]" theory: the [[Quantifier (logic)|quantifiers]] extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describe [[Recursion|recursively defined]] integer functions such as exponentiation, [[Factorial|factorials]] or the [[Fibonacci number|Fibonacci sequence]].

Let <math>\mathbb N</math> be the standard [[structure (mathematical logic)|structure]] for <math>L,</math> i.e. <math>\mathbb N</math> consists of the ordinary set of natural numbers and their addition and multiplication. Each sentence in <math>L</math> can be interpreted in <math>\mathbb N</math> and then becomes either true or false. Thus <math>(L, \mathbb N)</math> is the "interpreted first-order language of arithmetic".

Each formula <math>\varphi</math> in <math>L</math> has a [[Gödel number]] <math>g(\varphi).</math> This is a natural number that "encodes" <math>\varphi.</math> In that way, the language <math>L</math> can talk about formulas in <math>L,</math> not just about numbers. Let <math>T</math> denote the set of  <math>L</math>-sentences true in <math>\mathbb N</math>, and <math>T^*</math> the set of Gödel numbers of the sentences in <math>T.</math> The following theorem answers the question: Can <math>T^*</math> be defined by a formula of first-order arithmetic?

''Tarski's undefinability theorem'':  There is no <math>L</math>-formula <math>\mathrm{True}(n)</math> that defines <math>T^*.</math>
That is, there is no <math>L</math>-formula <math>\mathrm{True}(n)</math> such that for every <math>L</math>-sentence <math>A,</math> <math>\mathrm{True}(g(A)) \iff A</math> holds in <math>\mathbb N</math>.

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 <math>\mathbb N</math> as in [[second-order arithmetic]])   It ''is'' possible to define a formula <math>\mathrm{True}(n)</math> which holds on exactly the set <math>T^*,</math> but that doesn't define truth for the stronger system. However, this formula only defines a truth predicate for formulas in the original language <math>L</math> (e.g., because  <math>T^*,</math> doesn't contain codes for sentences quantifying over subsets of <math>\mathbb N</math>). To define truth in this stronger system would require ascending to an even stronger system and so on.

To prove the theorem, we proceed by contradiction and assume that an <math>L</math>-formula <math>\mathrm{True}(n)</math> exists which is true for the natural number <math>n</math> in <math>\mathcal N</math> if and only if <math>n</math> is the Gödel number of a sentence in <math>L</math> that is true in <math>\mathbb N</math>. We could then use <math>\mathrm{True}(n)</math> to define a new <math>L</math>-formula <math>S(m)</math> which is true for the natural number <math>m</math> if and only if <math>m</math> is the Gödel number of a formula <math>\varphi(x)</math> (with a free variable <math>x</math>) such that <math>\varphi(m)</math> is false when interpreted in <math>\mathbb N</math> (i.e. the formula <math>\varphi(x),</math> when applied to its own Gödel number, yields a false statement). If we now consider the Gödel number <math>g</math> of the formula <math>S(m)</math>, and ask whether the sentence <math>S(g)</math> is true in <math>\mathbb N</math>, we obtain a contradiction. (This is known as a [[Diagonal lemma|diagonal argument]].)

The theorem is a corollary of [[Post's theorem]] about the [[arithmetical hierarchy]], proved some years after Tarski (1933). A semantic proof of Tarski's theorem from Post's theorem is obtained by [[reductio ad absurdum]] as follows. Assuming <math>T^*</math> is arithmetically definable, there is a natural number <math>n</math> such that <math>T^*</math> is definable by a formula at level <math>\Sigma^0_n</math> of the [[arithmetical hierarchy]]. However, <math>T^*</math> is <math>\Sigma^0_k</math>-hard for all <math>k.</math> Thus the arithmetical hierarchy collapses at level <math>n</math>, contradicting Post's theorem.