Liar Paradox formalized as Prolog
(error now unequivocally shown)

“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.
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