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

On 06/05/2026 20:48, phoenix wrote:

> I guess my question is this: If the diagonal sequence is inadequate,
> just what exactly is Cantor attempting to represent with the diagonal
> sequence at all?

The outline is that the argument involves showing that /each/ and
/every/ sequence of /all/ the reals in [0,1) (should there be any) can
be mapped by a function to a real in [0,1) - perhaps a different one for
each sequence - that could not have been in the sequence it was
generated from. Thereby one shows that there is no sequence of /all/ the
reals in [0,1) - a solution and the only solution.

It is usually taught as "write a list of all the reals and then..."
which is useless. It is usually also taught with steps missing since the
formalisation of reals and limits that we trust today wasn't available
to Cantor so his proof doesn't involve them.

If someone were to bother making what would be a valid proof today
instead of what would have been called a proof back /then/ they would
use theorems about limits and either a constructive definition of the
reals or a constructive definition of a constraint on constructions to
those that define the reals (as they are conceived rather than later
constructively explicated).

-- 
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.