Please confirm that all of this is true.
Non-programmers and non-Prolog programmers only
understand Occurs‑check failure as “Prolog doesn’t like it”.
When you write LP = not(true(LP)) you are defining LP
in terms of itself with no base case. If you try to
expand the structure, you get:
not(true(not(true(not(true(not(true(…))))))))
The expansion never bottoms out. It is an infinite
regress. Most Prolog systems will show a cyclic term
if you run:?- LP = not(true(LP)).
But this is only a compact representation. It is not
a well‑founded term in the ISO sense.
If you enforce the ISO occurs check:
?- unify_with_occurs_check(LP, not(true(LP))).
you get: false.
Occurs‑check failure has a precise meaning:
the unification would create a non‑well‑founded term
whose structure expands forever. ISO Prolog requires
all terms to be finite and well‑founded, so the
unification must fail.
For non‑Prolog programmers: occurs‑check failure means
the system was about to build a data structure that
expands forever. No finite machine can represent that
safely. If Prolog actually tried to expand it, it would
recurse until it ran out of memory. So Prolog correctly
rejects it.
Conclusion: LP = not(true(LP)) is formally ill‑founded
in Prolog’s term model. Its structural expansion is
infinite, it violates the well‑foundedness requirement for
terms, and unify_with_occurs_check/2 correctly detects
this. Because the term cannot be well‑founded, it cannot
be assigned a truth value in any well‑founded interpretation.