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

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. When it's applied to a list that doesn't have a
construction then the result isn't a construction of a diagonal number.

If we take a list of any infinite sequences to admit those that have no
construction then our diagonal number is not constructed.

If, instead of restricted universal quantification (∀ st.) which ranges
over the constructible objects with a restriction, we use restricted
fantastical quantification (🦄 st.) then we will range over lists that
are not constructible unless the restriction excludes them, thus we
could range over lists containing numbers that are not constructible,
then our diagonal number is not constructed in each case.

Where we are challenged to give a list, we ought to be challenged to
construct a list.

> (Namely, we don't need to say "assume ab abdsurdo that
> an enumeration is given", we can just say "for *any* list,
> we *construct* an element not in the list".)

For any constructible list.



-- 
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.