Re: All infinities are countable in ordinary mathematics

On 06/05/2025 14:10, Julio Di Egidio wrote:

On 06/05/2025 01:57, Julio Di Egidio wrote:
 

Speaking of which, what do you even think this thread is
about??  THERE IS NO SUCH THING AS THE EXTRA-ORDINARY,
in ordinary and/or concrete (foundational!) mathematics:
so in any mathematics!  That's eventually my thesis.

 The underlying presumption being that a mathematics that
cannot be instantiated is at best an exercise in futility.
 

Now try and give me a counter-example... that does not
rely on [i.e. assume] the real numbers being uncountable.

 You cannot, can you.  LOL

Here is a very interesting one [*], M. Rathjen,
"Proof Theory of Constructive Systems: Inductive Types
and Univalence" (2018), <https://arxiv.org/abs/1610.02191>
For example, among other things:
<< Martin-Löf type theory appears to capture the abstract notion
of an inductively defined type very well via its W-type. There are,
however, intuitionistic theories of inductive definitions that at
first glance appear to be just slight extensions of Feferman's
explicit mathematics (see Feferman's quote from Sect. 1) but have
turned out to be much stronger than anything considered in ML type
theory. They are obtained from `T^i_0` by the augmentation of a
monotone fixed point principle which asserts that every monotone
operation on classifications (Feferman's notion of set) possesses
a least fixed point. To be more precise, there are two versions of
this principle. `MID` merely postulates the existence of a least
solution, whereas `UMID` provides a uniform version of this axiom
by adjoining a new functional constant to the language, ensuring
that a fixed point is uniformly presentable as a function of the
monotone operation. >>
Or, as we say around here, `lim_{n->oo} n = oo`,
aka "the point at infinity".
Julio
[*] Found via this SE answer by L. Pujet which provides
more introduction: "Proof-theoretic comparison table?"
<https://proofassistants.stackexchange.com/a/1210>