Prolog already refutes the Tarski Undefinability Theorem

Prolog queries return “Yes” when-so-ever an expression is provable on the basis of the Facts and Rules in its database and returns “No” otherwise. Facts correspond to axioms, Rules correspond to rules-of-inference and the Prolog database corresponds to a formal system.

The above inference model directly refutes the third line of Tarski’s proof:
(3) x ∉ Pr if and only if x ∈ Tr

~Provable(x) ↔ True(x)
Because of the way that the Prolog inference model works the above expression would be false, and its negation: Provable(x) ↔ True(x) would be true. So the Prolog inference model already refutes Tarski’s line (3) which in turn causes the whole rest of Tarski’s proof to fail.