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

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




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