# Tarski's original proof of the undefinability of truth

I'm trying to understand Tarski's proof of the undefinability of truth as given in his paper The Concept of Truth in Formalized Languages (English translation in Logic, Semantics, Metamathematics, 1983, pp. 152-278).

I understand modern presentations of the theorem and its proof, but they use the Diagonal Lemma while Tarski doesn't (at least not explicitly).

Are there any such explications of the original proof?

See page 247-48 (and footnote page 247):

The idea of the proof of this theorem can be expressed in the following words: (1) a particular interpretation of the metalanguage is established in the language itself and in this way with every sentence of the metalanguage there is correlated, in one-many fashion, a sentence of the language which is equivalent to it (with reference to the axiom system adopted in the metatheory); in this way the metalanguage contains as well as every particular sentence, an individual name, if not for that sentence at least for the sentence which is correlated with it and equivalent to it.

This is what in the proof of Gödel's Incompleteness Theorems has been called: the arithmetization of syntax.

The original Gödel's proof "diagonalize" without using an explicit "general purpose" Diagonal Lemma.

(2) Should we succeed in constructing in the metalanguage a correct definition of truth, then the metalanguage — with reference to the above interpretation — would acquire that universal character which was the primary source of the semantical antinomies in colloquial language. It would then be possible to reconstruct the antinomy of the liar in the metalanguage, by forming in the language itself a sentence x such that the sentence of the metalanguage which is correlated with x asserts that x is not a true sentence. In doing this it would be possible, by applying the diagonal procedure [emphasis added] from the theory of sets, to avoid all terms which do not belong to the metalanguage, as well as all premises of an empirical nature which have played a part in the previous formulations of the antinomy of the liar.

You can find the "diagonal argument" referred to by Tarski in e.g.:

Diagonal Lemma (Cantor). Let P be a binary predicate. For each number b, we define a unary predicate P_b by P_b(a) ↔ P(a,b). Let P be a binary predicate, and let Q be the unary predicate defined by Q(a) ↔ ¬ P(a,a). Then Q is distinct from all the P_b.

A simple proof of Tarski's Theorem in "old style" can be found in: