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:**

http://liarparadox.org/Tarski_Proof_275_276.pdf

**(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.