(1) x ∉ Pr ↔ p // p ↔ ~Provable(x)

(2) x ∈ Tr ↔ p // p ↔ True(x)

(3) x ∉ Pr ↔ x ∈ Tr // ~Provable(x) ↔ True(x)

By making x and p concrete such as:

x 3 > 5

p 3 < 5

(1) ~Provable(3 > 5) ↔ {3 < 5}

(2) True(3 > 5) ↔ {3 < 5}

(3) ~Provable(3 > 5) ↔ True(3 > 5)

There is no way to concretely define x and p such that

line (3) logically follows from lines (1) and Line (2)

**The 1936 Tarski Undefinability Proof**

http://liarparadox.org/Tarski_Proof_275_276.pdf

**Tarski Undefinability Theorem Succinctly Refuted**

http://liarparadox.org/Tarski_Undefinability_Refutation.pdf

Meaning_Postulates_Rudolf_Carnap_1952.pdf

http://liarparadox.org/Haskell_Curry_45.pdf

http://liarparadox.org/247_248.pdf