Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Lawrence D'Oliveiro <ldo@nz.invalid>
Newsgroups: comp.theory
Subject: Re: Cantor Diagonal Proof
Date: Sun, 13 Apr 2025 21:30:09 -0000 (UTC)
Organization: A noiseless patient Spider
Lines: 14
Message-ID: <vthad1$3oh15$3@dont-email.me>
References: <vsn1fu$1p67k$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 13 Apr 2025 23:30:10 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="5a394981b73e49d36ebf2736a3771422";
	logging-data="3949605"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/HM7AV1rRKINYEz/KoT7LV"
User-Agent: Pan/0.162 (Pokrosvk)
Cancel-Lock: sha1:CXKRmmSGt5hJhC8tUPmb9BiJiAg=
Bytes: 1586

Here’s another way to look at the Cantor construction.

It is possible to construct a list of numbers, ostensibly from ℝ, where it 
is provable, by induction, that the Cantor construction cannot produce a 
number not in the list. This shows that you cannot prove, a priori, the 
validity of the Cantor construction.

But then, you cannot prove, a priori, the validity of proof by induction, 
either. Instead, it has to be added as an explicit axiom when constructing 
the integers ℤ.

In the same way, you can add “the Cantor construction works” as an axiom 
when constructing the set of reals ℝ. Otherwise, ℝ is just the set of 
computable numbers.