Re: Ross Finlayson what about the Prolog Liar Paradox ?

On 7/7/2026 4:35 PM, Ross Finlayson wrote:
> On 07/07/2026 12:48 PM, olcott wrote:
>> On 7/7/2026 2:17 PM, Ross Finlayson wrote:
>>> On 07/07/2026 11:07 AM, olcott wrote:
>>>> On 7/7/2026 12:53 PM, Ross Finlayson wrote:
>>>>> 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.
>>>>>
>>>>
>>>> I have a name for this: The finite set of "atomic facts" of
>>>> empirical general knowledge and the finite set of relations
>>>> between them is named:
>>>> "the body of general knowledge expressed in language"
>>>>
>>>>> 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."
>>>>>
>>>>
>>>> You are simply ignoring that expressions with cycles
>>>> in their evaluation sequence are rejected as meaningless.
>>>> Kripke would say that they are "undefined"
>>>>
>>>>> 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.
>>>>>
>>>>
>>>> So maybe this is too much into the field of philosophy of
>>>> logic and thus outside the field or carefully memorizing
>>>> exiting conventions for you to understand.
>>>>
>>>> The bottom line is the my Prolog tossed the Liar Paradox
>>>> out on its ass and Gemini agrees. You didn't seem to get
>>>> this most crucial point.
>>>>
>>>
>>>
>>>
>>> Russell would call you a fool.
>>
>> Not at all he himself had the vicious circle principle.
>> https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/ 
>> volume-40/issue-1/Russell-Presupposition-and-the-Vicious-Circle- 
>> Principle/10.1305/ndjfl/1039096305.full
>>
>>
>> Have you every heard of ZFC?
>>
> 
> Since Chrysippus for modal, temporal, relevance logic,
> there's the like of "Hume's connexions", where something
> like John Stuart Mill would be so familiar to quasi-modal
> repeteurs.
> 
> The model-theory and the proof-theory are equi-interpretable.
> 

Not really. Model theory does not have enough info
to reject bad inputs.

> Then, "theories-of-one-relation" like set-theory or class-theory
> or part-theory or partition-theory, or order-theory or ordering-theory,
> like set theory, for example ZFC with:
> 
> an ordinary vacuity, the empty set,
> an ordinary infinity, the inductive set,
> 
> those being both expansion-of-comprehension and
> restriction-of-comprehension, since axioms are of at least two kinds,
> then for various rulialities/regularities that compete:
> 
> well-foundedness, sets having e-minimal elements,
> well-ordering, orderings having e-minimal elements,
> 
> then besides the usually not included alike Martin's axiom:
> 
> well-dispersion, both e-minimal and e-maximal, the illative or univalent,
> 
> then the rest of the axioms of ZFC being expansion of comprehension
> or composing sets, quite naively, then at least one of those,
> doesn't matter much, being called a schema instead of an axiom
> for first-order-izibility,
> 
> that's ZFC, the set theory, then for its accounts modeling the
> descriptive set theory's account of geometry and for the objects
> of real analysis, usually also axiomatizing
> 

ZFC does not allow sets containing themselves to be
defined. Most of the rest of math is not this insightful.
Bad input is thought of as a limitation of the formal system.

> least-upper-bound existence of the rational field,
> measure 1.0 of the unit in the real field,
> 
> since those aren't derived in the usual way, with line-reals first
> providing least-upper-bound and measure 1.0, then yes,
> I've heard of ZFC, and NBG and GBN, and ZFC with classes.
> 
> 
> It's good to know these things and be thorough and conscientious,
> instead of being a vacuous moron of the ordinary sort.
> 
> 
> 
> In school when were shown that an error in reasoning could result
> seemingly correct answers that were wrong, it was in the setting
> of a calculus course, where one of the expressions was a quotient
> with the divisor being an expression in the difference of a constant
> and a variable, thusly, if the variable was equal the constant,
> then that would be dividing by zero, which is undefined, then a
> resulting evaluation resulted 0 = 1, which was wrong. Then there
> was addressed limits from the left and limits from the right and
> discontinuities and removable discontinuities, about the thorough sort
> of account.
> 
> The point here is that the gap in definition about the objects of
> mathematics is different than ex falso quodlibet, since singularities in
> a singularity theory are branches in a multiplicity theory,
> and it's simply erroneous to break the definition, and erroneous to have
> carried the derivation, ex falso quodlibet is erroneous.
> 
> 

This is the whole kit-and-kaboodle of the essence
of my system. Currently PTS understands these things
the best.

P ⊢ Q means syntactic derivation implements semantic
entailment encoded in syntactically the language.
This is the only inference steps allowed. The entailment
rules depend on the represented domain.



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