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

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.

-- 
Mikko