**“This sentence is not true”.**

Formalized mathematically as this predicate logic statement:

**LP ↔ ~True(LP)**

not_true(X) :- X -> false; true.

materially_equivalent(X, Y) :- (X, Y); (not(X), not(Y)).

**Liar Paradox formalized as Prolog:**

materially_equivalent(not_true(LP), LP).

**This fails indicating an infinitely recursive structure:**

?- unify_with_occurs_check(not_true(LP), LP).

**Therefore this predicate cannot be evaluated:**

?- materially_equivalent(not_true(LP), LP).

Thus showing the precise nature of the unequivocal error of the Liar Paradox and related self-referential undecidable decision problems.

http://mathworld.wolfram.com/Undecidable.html

Not decidable as a result of being neither formally provable nor unprovable.

**Pinnacle of my work (over 12,675 USENET messages) since 1998:
Tarski’s formal correctness formula: ∀x True(x) ↔ φ(x)
is completed by this RHS: ∀x True(x) ↔ ⊢x**

**That tiny little formula provides the basis for correctly refuting:**

(1) The Liar Paradox

(2) The essence of the 1931 Incompleteness Theorem

(3) The 1936 Tarski Undefinability Theorem

(4) The 1936 Alan Turing Halting Problem

**All four have (previously undiscovered) infinitely recursive structure.**

Copyright 2018 (and many other years since 1998) Pete Olcott