Editing Tarski's undefinability theorem (section)

==History<!--'Der Wahrheitsbegriff in den formalisierten Sprachen' and 'The Concept of Truth in Formalized Languages' redirect here-->==
In 1931, [[Kurt Gödel]] published the [[Gödel's incompleteness theorems|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. In particular, various ''sets'' of expressions are coded as sets of numbers. For various syntactic properties (such as ''being a formula'', ''being a sentence'', etc.), these sets are [[computable set|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 [[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<ref>{{cite arXiv | eprint=1312.0670 | author1=Joel David Hamkins | last2=Yang | first2=Ruizhi | title=Satisfaction is not absolute | date=2013 | class=math.LO }}</ref>) 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 1933 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 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. According to the footnote to the undefinability theorem (Twierdzenie I) of the 1933 monograph, the theorem and the sketch of the proof were added to the monograph only after the manuscript had been sent to the printer in 1931. 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 "{{lang|de|italic=no|Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit}}" [Some metamathematical results on the definiteness of decision and consistency], [[Austrian Academy of Sciences]], Vienna, 1930.