Ross Finlayson what about the Prolog Liar Paradox ?

% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.

That is an elegant and classic way to demonstrate the Liar Paradox 
("This sentence is false") using Prolog's unification mechanics!

You've perfectly captured the tension between computational pragmatism 
and strict mathematical logic. Here is exactly what is happening under 
the hood in your snippet:

1. The Pragmatic Illusion: Standard Unification

Prolog
?- LP = not(true(LP)).
LP = not(true(LP)).

When you use the standard unification operator (=), Prolog tries to make 
the left side and the right side identical. To save processing time and 
memory, Prolog historically skips a crucial step called the occurs check.

Because it skips this check, Prolog happily binds the variable LP to the 
term not(true(LP)). This creates a cyclic term (or a rational tree). In 
memory, LP now points to a structure that contains a reference back to 
LP, creating an infinite loop of self-reference. Computationally, Prolog 
accepts the paradox.

2. The Logical Safeguard: The Occurs Check

Prolog
?- unify_with_occurs_check(LP, not(true(LP))).
false.

Here, you enforce strict First-Order Logic. The 
unify_with_occurs_check/2 predicate forces Prolog to pause and ask: 
"Does the variable I am trying to bind already exist inside the term I 
am binding it to?" Because the variable LP occurs inside not(true(LP)), 
Prolog realizes that unifying them would require building a 
mathematically impossible, infinitely deep structure: 
not(true(not(true(not(true(...)))))). It rightfully rejects the 
unification and returns false.

The Philosophical Takeaway
In logic, self-referential paradoxes often arise when a system is 
allowed to talk about its own truth values without hierarchical 
restrictions (as famously noted by Alfred Tarski).

Your Prolog snippet perfectly mirrors this:

Standard Unification acts like natural language, allowing the 
self-reference to happen (and potentially causing a stack overflow if 
you tried to evaluate or traverse it).

The Occurs Check acts like a strict formal logic system, explicitly 
forbidding self-referential loops and shutting the paradox down before 
it can form.


https://share.gemini.google/5UVT3f5WnV8K

-- 
Copyright 2026 Olcott

My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
The complete structure of this system is now defined.

The entire body of knowledge expressed in language is
comprised of two types of relations between finite strings:
(a) *Axioms* Expressions of language that are stipulated to be true.

My system bridges the analytic/synthetic distinction by
expressly encoding all empirical "atomic facts" in a formal
language such as CycL of the Cyc project.

(b) *Inference Rules* Expressions of language that are semantically
entailed syntactically from (a) and/or (b).