Re: Within Proof Theoretic Semantics Gödel's G has n o meaning in PA

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.
>>>>>
>>>>> 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.
>>>>>
>>>>> The absence of
>>>>> (a) finite sequence of inference steps to an atomic base,
>>>>> (b) canonical proof
>>>>> (c) well-founded justification tree
>>>>> makes the above to PTS invalid.
>>>>>
>>>>
>>>> Yeah, come up with something new, or stuff a sock in it.
>>>>
>>>>
>>>
>>> The above proves that the notion of undecidable
>>> is incorrect if you understood rather than ignored
>>> what it says.
>>>
>>> It also is the final resolution to the Liar Paradox
>>> and you would know this if you understood it.
>>>
>>
>> Like I said,
>> "understanding" is for suckers,
>> "comprehension" is for knowledge.
>>
>
> Gemini agrees with me and I only gave it the Prolog.
> https://share.gemini.google/1dJnMwOZ2k5F
>
>>
>> Your axiomatization otherwise is false.
>>
>>
>> It's like they say,
>> "It just don't mean a thing."
>>
>>
>> WM <- retro-finitist crankety-troll
>> JG <- retro-finitist crankety-troll
>> PO <- retro-finitist crankety-troll
>> "Polluter(s) of sci.math"
>>
>>
>
>

Gemini agrees with not-you.