Is this the correct way to encode the Liar Paradox in Prolog?
Liar Paradox in English: "This sentence is not true."
?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false.
After careful review by others it seems correct to say that the above expression is isomorphic to the Liar Paradox even when we ignore the English meanings of the terms "not" and "true" and replace them with "foo" and "bar". It is the pathological self-reference of the Liar Paradox that Prolog rejects.
?- LP = foo(bar(LP)). LP = foo(bar(LP)). ?- unify_with_occurs_check(LP, foo(bar(LP))). false.
The Clock & Mellish text in my answer explains the details of why unify_with_occurs_check rejects LP.
Prolog correctly rejects any expression having the same pathological self referential structure as the Liar Paradox with its unify_with_occurs_check/2.