Editing Tarski's undefinability theorem (section)

==General form==
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]].

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

The proof of Tarski's undefinability theorem in this form is again by [[reductio ad absurdum]]. Suppose that an <math>L</math>-formula <math>\mathrm{True}(n)</math> as above existed, i.e., if <math>A</math> is a sentence of arithmetic, then <math>\mathrm{True}(g(A))</math> holds in <math>\mathcal N</math> if and only if <math>A</math> holds in <math>\mathcal N</math>. Hence for all <math>A</math>, the formula <math>\mathrm{True}(g(A)) \iff A</math> holds in <math>\mathcal N</math>. But the diagonal lemma yields a counterexample to this equivalence, by giving a "liar" formula <math>S</math> such that <math>S \iff \lnot \mathrm{True}(g(S))</math> holds in <math>\mathcal N</math>. This is a contradiction. QED.