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

On 06/07/2026 20:49, olcott wrote:
> 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.

That does not contradict the fact that there is no evaluation of G
in the determination of the Gödel number of anything, nor deny that
the intent was to decieve.
-- 
Mikko