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

On 7/6/2026 4:58 AM, Mikko wrote:
> On 05/07/2026 19:33, 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.
>>
>> Olcott's Minimal Type Theory
>> G ↔ ¬Prov_PA(⌜G⌝)
>> Directed Graph of evaluation sequence
>> 00 ↔               01 02
>> 01 G
>> 02 ¬               03
>> 03 Prov_PA         04
>> 04 Gödel_Number_of 01  // cycle indicates no well-founded 
>> justification tree exists.
> 
> That is false. There is no evaluation of G in the determination of the
> Gödel number of anything. Therefore the claim of a loop is false.
> 
> That error has already been pointed out but Olcott still hopes that
> someone might bite the bait and the hook.
> 

Every LLM agrees that I turned "undecidability"
on its head with the Prolog code final resolution
of the Liar Paradox because it <is> a verified
fact that I did do this.

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