Tarski 1936 Undefinability Proof Simplified

How the “x” variable referenced in Tarski’s proof is defined:
Tarski Undefinability Proof (pages 247-248)

Tarski’s Undefinability Theorem proof:
Tarski Undefinability Proof (pages 275-276)

Direct quotes from page 275-276       // indicates paraphrase
the symbol ‘Pr’ which denotes the class of all provable sentences of the theory under consideration

We can construct a sentence x … which satisfies the following condition:
It is not true that x ∈ Pr if and only if p

(1) x ∉ Pr ↔ p                   // p ↔ ~Provable(x)
Where the symbol ‘p’ represents the whole sentence x.

We shall now show that the sentence x is actually undecidable and at the same time true.

If we denote the class of all true sentences by the symbol ‘Tr’ then – in accordance with convention T – the sentence x which we have constructed will satisfy the following condition:
(2) x ∈ Tr ↔ p                   // p ↔ True(x)
From (1) and (2) we obtain immediately:
(3) x ∉ Pr ↔ x ∈ Tr          // ~Provable(x) ↔ True(x)

We can derive the following theorems from the definition of truth
(4) either x ∉ Tr or ~x ∉ Tr       // ~True(x) ∨ ~True(~x)
(5) if x ∈ Pr, then x ∈ Tr             // Provable(x) → True(x)
(6) if ~x ∈ Pr, then ~x ∈ Tr       // Provable(~x) → True(~x)

From (3) and (5) we infer without difficulty that
(7) x ∈ Tr                      // True(x)
and that
(8) x ∉ Pr                     // ~Provable(x)
In view of (4) and (7) we have
(8a) ~x ∉ Tr,              // ~True(~x)
which together with (6) gives us the formula:
(9) ~x ∉ Pr                 // ~Provable(~x)
The formulas (8) and (9) together express the fact that x is an undecidable sentence; moreover from (7) it follows that x is a true sentence.

Copyright 1936 Alfred Tarski
Paraphrase Simplifications Copyright 2018 Pete Olcott

The Concept of Truth in Formalized Languages, Alfred Tarski 1936