Editing Tarski's undefinability theorem (section)

==Discussion==
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 invoke [[recursion#Functional recursion|recursive function]]s in any way. The proof does assume that every <math>L</math>-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 [[Gödel's incompleteness theorems|theorems of Gödel]] about the metamathematical properties of first-order arithmetic.

[[Raymond Smullyan|Smullyan]] (1991, 2001) has argued forcefully that Tarski's undefinability theorem deserves much of the attention garnered by [[Gödel's incompleteness theorem]]s. That the latter theorems have much to say about all of mathematics and more controversially, about a range of philosophical issues (e.g., [[John Lucas (philosopher)|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 [[Predicate (grammar)|predicates]] and [[function symbol]]s defining all the [[semantic]] concepts specific to the language. Hence the required functions include the "semantic valuation function" mapping a formula <math>A</math> to its [[truth value]] <math>||A||,</math> and the "semantic denotation function" mapping a term <math>t</math> 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 <math>\mathcal N</math> is definable by a formula in [[second order arithmetic]]. Similarly, the set of true formulas of the standard model of second order arithmetic (or <math>n</math>-th order arithmetic for any <math>n</math>) can be defined by a formula in first-order [[Zermelo–Fraenkel set theory|ZFC]].