Re: Within Proof Theoretic Semantics Gödel's G h as no meaning in PA

On 7/6/2026 11:16 AM, Ross Finlayson wrote:
> On 07/05/2026 03:55 PM, olcott wrote:
>> On 7/5/2026 5:15 PM, Ross Finlayson wrote:
>>> On 07/05/2026 02:45 PM, olcott wrote:
>>>> On 7/5/2026 4:30 PM, Ross Finlayson wrote:
>>>>> On 07/05/2026 01:25 PM, olcott wrote:
>>>>>> On 7/5/2026 2:56 PM, Ross Finlayson wrote:
>>>>>>> On 07/05/2026 09:33 AM, olcott wrote:
>>>>>>>> On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
>>>>>>>>> On 04/07/2026 16:31, Tristan Wibberley wrote:
>>>>>>>>>> On 06/05/2026 20:37, Julio Di Egidio wrote:
>>>>>>>>>>> On 02/05/2026 20:47, Scott Hoge wrote:
>>>>>>>>>>>
>>>>>>>>>>>> In Cantor's theorem, we do not actually construct a diagonal.
>>>>>>>>>>>> Rather, we presuppose that we can enumerate a set, and then,
>>>>>>>>>>>> /purely on the grounds of possibility/, conceive a diagonalized
>>>>>>>>>>>> non-element.
>>>>>>>>>>>
>>>>>>>>>>> Nope, as explained and re-explained ad nauseam around here:
>>>>>>>>>>> just the resident trolls won't get it.
>>>>>>>>>>>
>>>>>>>>>>> Cantor's diagonal argument, the one with the binary sequences,
>>>>>>>>>>> is indeed constructive: a definition of anti-diagonal of *any*
>>>>>>>>>>> (infinite) list is provided, and the proof that the anti- 
>>>>>>>>>>> diagonal
>>>>>>>>>>> cannot be in the list is quite constructive.
>>>>>>>>>>
>>>>>>>>>> "quite" but not "completely".
>>>>>>>>>>
>>>>>>>>>> A constructive operation is defined, but a diagonal number is
>>>>>>>>>> constructed just when that constructive operation is applied to a
>>>>>>>>>> constructible list.
>>>>>>>>>
>>>>>>>>> I should note for the less knowledgable readers of course it's 
>>>>>>>>> less
>>>>>>>>> often than that, it is only that often for systems such as the one
>>>>>>>>> Julio
>>>>>>>>> and Phoenix are using which allows dequantification of universally
>>>>>>>>> quantified statements into the system proper which then have
>>>>>>>>> derivable
>>>>>>>>> statements containing actual constructions of the constructible
>>>>>>>>> objects
>>>>>>>>> they apply to by virtue of their original quantification. Of
>>>>>>>>> course,
>>>>>>>>> dequantification of fantastically quantified statements doesn't
>>>>>>>>> make a
>>>>>>>>> statement about nonconstructible objects because there aren't any
>>>>>>>>> outside of the fantastical quantification.
>>>>>>>>>
>>>>>>>>> By which I don't mean to argue the countability of the set of
>>>>>>>>> reals as
>>>>>>>>> defined in what we call Cantor's Proof of the Uncountability of 
>>>>>>>>> the
>>>>>>>>> Reals to include objects quantified over by fantatstical
>>>>>>>>> quantification
>>>>>>>>> but not by universal quantification, but it does make some meaning
>>>>>>>>> clearer.
>>>>>>>>>
>>>>>>>>> While some of the sets might have objects in the system proper,
>>>>>>>>> some of
>>>>>>>>> the members of some of the sets clearly do not.
>>>>>>>>>
>>>>>>>>
>>>>>>>> % This sentence is not true.
>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>> LP = not(true(LP)).
>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>> false.
>>>>>>>>
>>
>>>
>>> Gemini agrees with not-you.
>>>
>>>
>>
>> OK then the point that I was trying to make is
>> exactly what Gemini said right here:
>> https://share.gemini.google/1dJnMwOZ2k5F
>>
>>
>>
>>
> 
> I tend not to follow links like that, post the transcript.
> 
> 

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

All the rest is irrelevant.
The point is that the LP have been finally totally
resolved.

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