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

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.


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"