Tarski Undefinability Theorem Succinctly Refuted

(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