Re: Ross Finlayson what about the Prolog Liar Paradox ?

On 07/07/2026 09:10 AM, olcott wrote:
> % 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
>

Imagine a language and its utterance of all the truisms in the universe.

This isn't saying necessarily what it says, only that it's said.
So, this account of a "Comenius language" of all the truisms is
more than less inscrutable yet as empty tautologies and truisms,
while yet each unique, for example as by natural numbers.

"This sentence 1 is true.
This sentence 2 is true.
This sentence 3 is true.
..."


So, quantify over those, like Russell might as
"sets-of-all-sets-that-don't-contain-themselves".

"This sentence (...) is not true."

Now, the idea here is that there's only one example of a truism
about contradiction, that the alternation of inversion of the
consideration that results quantification, brings along the
"sputnik of quantification", that reads in its form as
"The Liar", yet instead of being a "paradox", its form is
construed as being a "Confessing Liar".


So, this account of univocity since Duns Scotus or as alike
accounts of the kabalah and gematria or since acconts of the
universal grammar since Panini like Leibnitz, this "Comenius
language" its consideration, like Quine's Nietzsche's "eternal
basic text", includes in itself a prototype of contradiction,
in otherwise all its affirmations.


Then, in natural language, there is a ready example or prototype
of contradiction, that in alike the natural "Coleridge language",
where that metaphor eventually fails yet there is a structural
account of the strong metonymy that fulfills true metaphor about
truth, then "the Liar" is simply an indicator of contradiction,
and results instead of explosion to contradiction its unconscious
digestion, results implosion to detection in any account of language.


So, "thinking" instead of "being thought" is the usual idea.
That's all then that the cycle-detection routine claims to do.


This way there are no paradoxes at all in Comenius language,
including that Confessing Comenius has an example to compare
against, what would be false.



The eternal basic text or underlying univocal universal word
might be negations instead of affirmations.

"This sentence 1 accounts and excludes 0.
This sentence 2 accounts and excludes 1.
This sentence 3 accounts and excludes 2.
..."


Then a similar account gives alike:

"This sentence infinity accounts and includes infinity."



Then simple accounts of error-detection then error _correction_,
including accounts of "not enough information" or "conflicting
information" are mostly usual and trite, in fact there's an
entire enterprise called "science" which makes for an inter-subjective
formal account with regards to strengthened logicist positivism
and ontologists, which though is always a _science_, yet though
that there are ideals like "truth" and "infinity" for that
"geometry" and "continuity" are real, and more than the blahs.