Counting infinities

As I have mentioned in my previous post, recently I stepped upon the path leading to infinity. But what is “infinity?” The question demands deep thinking.

This post starts the new series.

Prolog

We usually meet the ideas of finite and infinite when we talk about sets: collections of objects that we can, at least in principle, list or describe. A set can be a small, concrete collection, such as the set of books on your desk or the set of planets in the Solar System. Other sets are already infinite, like the set of all even numbers \{0,2,4,6,\dots\}, the set of all odd numbers \{1,3,5,7,\dots\}, or the set of all prime numbers \{2,3,5,7,11,\dots\}. All of these are infinite in the sense that there is no last element, yet they are made from familiar things and we have an intuitive picture of what they are. In the early days of set theory, however, mathematicians began to consider more daring constructions such as the “set of all sets”. This led to paradoxes (for example, versions of Russell’s paradox) showing that if we allow absolutely any collection to count as a set, we run into contradictions. In response, various axiomatic systems for set theory were developed, each carefully limiting which collections are allowed to be sets.  Today there are competing foundations (such as Zermelo–Fraenkel set theory (ZF) and its extension with the Axiom of Choice (ZFC), von Neumann–Bernays–Gödel class theory, elementary topos theory (topos-theoretic foundations), and other alternative systems), reflecting the fact that our naive picture of “the set of all sets” was philosophically appealing but mathematically too generous. The foundational framework we choose is not neutral for “cardinal numbers” and the different kinds of infinity they describe: it can change their ontology, some of their provable properties, and their usefulness for different styles of mathematics (classical analysis vs.\ constructive or computational vs.\ categorical). In this introductory “sandbox” we quietly work within the usual ZF/ZFC picture, but the basic ideas about comparing sizes of sets can be appreciated without going deeply into these foundational debates.

Counting sizes of sets

We usually think of a “number” as something we use for counting: three books, five students, ten fingers, and so on. Mathematically, this idea is captured by cardinal numbers, which measure the size (or cardinality) of a set, ignoring order and other structure.\footnote{For a more systematic treatment, see e.g.\ the article Cardinal number on Wikipedia.}

Two sets A and B are said to have the same \emph{cardinality} if there exists a bijection between them, that is, a one-to-one and onto map f\colon A\to B. Intuitively, you can match each element of A with exactly one element of B, with nothing left over on either side.

A first picture

Suppose your bookshelf has four books, and your desk has four pencils. You can pair them: \begin{center}

Rendered by QuickLaTeX.com

\end{center}

The exact pairing does not matter; what matters is that such a perfect matching exists. That is what it means for two sets to have the same cardinality.

Finite and infinite

A set is \emph{finite} if its elements can be counted as 1,2,\dots,n for some natural number n; in this case we write |A| = n. Otherwise the set is \emph{infinite}.

The set of natural numbers

    \[ \mathbb{N} = \{0,1,2,3,\dots\} \]

is the basic example of an infinite set. A set is called \emph{countable} if it has the same cardinality as \mathbb{N}, that is, if its elements can be listed in a sequence.

Examples

  • The set of integers \mathbb{Z} = \{\dots,-2,-1,0,1,2,\dots\} is countable. One possible listing is

        \[ 0,1,-1,2,-2,3,-3,\dots \]

    which gives a bijection with \mathbb{N}.

  • The set of rational numbers \mathbb{Q} is also countable, although the construction of a listing is more involved.
  • The set of real numbers \mathbb{R} is uncountable: there is no way to list all real numbers in a sequence so that each appears exactly once.

A sketchy picture of uncountability

To explain what goes wrong with trying to “count” all real numbers, it is helpful to recall how we write real numbers in decimal form. A decimal expansion is a way of writing a number using digits 0,1,\dots,9 after a decimal point, such as

    \[ 3.14159\quad\text{or}\quad 0.50000\quad\text{or}\quad 2.71828\ldots \]

Some decimals eventually stop (like 8.75 = 8.75000\ldots); others go on forever but repeat a pattern of digits (like 1/3 = 0.3333\ldots). Numbers that can be written as a fraction of two integers, such as 5/2 or 37/99, are called rational numbers. Exactly these numbers have decimal expansions that either terminate or eventually repeat. By contrast, an irrational number cannot be written as a ratio of integers. Its decimal expansion goes on forever without ever settling into a repeating pattern. One of the simplest examples is \sqrt{2}, the length of the diagonal of a unit square. The ancient Greeks already knew that \sqrt{2} is not rational: assuming \sqrt{2} = a/b with integers a,b leads to a contradiction after a short number-theoretic argument. In decimal form,

    \[ \sqrt{2} \approx 1.4142135623\ldots \]

and the digits continue indefinitely with no repeating block. Cantor’s idea was to imagine that, somehow, we have managed to list all real numbers between 0 and 1 in a sequence:

    \[ x_1, x_2, x_3, x_4,\dots \]

and that each x_n is written in decimal form:

    \[ \begin{array}{rcl} x_1 &=& 0.\,d_{11}d_{12}d_{13}d_{14}\dots \\ x_2 &=& 0.\,d_{21}d_{22}d_{23}d_{24}\dots \\ x_3 &=& 0.\,d_{31}d_{32}d_{33}d_{34}\dots \\ x_4 &=& 0.\,d_{41}d_{42}d_{43}d_{44}\dots \\ \vdots && \vdots \end{array} \]

Here d_{nk} is the kth digit of the nth number in the list.

Cantor’s diagonal trick

Added as a reply to Bjab’s objections in the comment 2026/05/05 at 09:39

I hope it addresses adequately his criticism and clarifies the issue at hand.

We start with identifying all real numbers x between 0 and 1 with infinite sequences c_n of integers form the set {0,1,2,3,4,5,6,7,8,9}, omitting the sequence of all zeros, and omitting sequences in which only 9 appears starting from some point. Each such sequence defines a decimal expansion of some x, and each x\in (0,1) can be uniquely represented by such a sequence

    \[ x=\sum_{n=1}^{\infty} d_n 10^{-n}.\]

Here we take it as proven fact , though we will not present a proof, as the proof would require  a precise definition of a real number, and some more. Thus we assume a bijection between real numbers in (0,1) and infinite sequences described above. Cantor’s reasoning deals with the sequences. But since these are in bijection with reals in (0,1), the two sets, by definition, have the same cardinal number.

Now we construct a new number y by looking at the diagonal digits d_{11},d_{22},d_{33},\dots and changing each one. For example, define the decimal digits c_k of y by

    \[ c_k = \begin{cases} 5,&\text{if } d_{kk} \neq 5,\\[4pt] 6,&\text{if } d_{kk} = 5, \end{cases} \]

and set

    \[ y = 0.\,c_1c_2c_3c_4\ldots \]

By construction, y is a real number between 0 and 1 (we have built a perfectly good decimal expansion), but it disagrees with each x_n in at least one digit: for the nth number, they differ at the nth digit after the decimal point, since c_n was chosen to be different from d_{nn}. In particular,

    \[ y \neq x_1\quad\text{because they differ in the first digit,} \]

    \[ y \neq x_2\quad\text{because they differ in the second digit,} \]

and so on for every n. Therefore y is not in the list x_1,x_2,x_3,\dots, even though that list was supposed to contain all real numbers in (0,1). This contradiction shows that no such complete list can exist: the real numbers in (0,1) cannot be put into a one-to-one correspondence with the natural numbers. In other words, the set of real numbers is uncountable.

A small diagram.

It may help to picture the situation schematically as a grid of digits:

Rendered by QuickLaTeX.com

The red line marks the diagonal digits d_{11},d_{22},d_{33},\dots; changing each of them produces the digits of the new number y, which by design avoids every line in the table.

We will not go into details here, but the conclusion is clear: there are more real numbers than natural numbers.

Alephs and the continuum

Infinite cardinalities are usually denoted by Hebrew letters.

  •  \aleph_0 (“aleph-null”) is the cardinality of \mathbb{N}; it is the smallest infinite cardinal.
  • \aleph_1, \aleph_2, \dots denote larger and larger infinite cardinals, defined using the theory of well-ordered sets.

The cardinality of the set of real numbers is called the \emph{continuum} and is denoted by

    \[ \mathfrak{c} = |\mathbb{R}|. \]

One can show that \mathfrak{c} = 2^{\aleph_0}, the cardinality of the power set of \mathbb{N}.

Power set

Before going further, we need one more basic construction on sets. Given a set A, its \emph{power set}, denoted \mathcal{P}(A) or 2^A, is the set of all subsets of A. For example, if X = \{a,b\}, then

    \[ \mathcal{P}(X) = \{\varnothing,\{a\},\{b\},\{a,b\}\}, \]

and if Y = \{1,2,3\}, then

    \[ \mathcal{P}(Y) = \{\varnothing,\{1\},\{2\},\{3\},\{1,2\},\{1,3\},\{2,3\},\{1,2,3\}\}. \]

The empty set \varnothing and the whole set A itself both count as subsets. In general, a finite set with n elements has 2^n subsets, which explains the notation 2^A: for each element, there are two choices (in or out) when forming a subset. Power sets will be crucial for us, because they produce new sets whose cardinalities are strictly larger than those of the original sets, and in particular they appear in the expression 2^{\aleph_0} for the cardinality of the continuum.

Diagram: different “sizes” of infinity

Here is a schematic picture (the arrows indicate “strictly smaller than”):

Rendered by QuickLaTeX.com

There is no surjective map from a set onto its power set, so |A| < |\mathcal{P}(A)| for any set A.

Some basic properties

Let A and B be sets.

  • If A \subseteq B, then |A| \le |B|.
  • For infinite sets, adding or removing finitely many elements does not change the cardinality.
  • The Cartesian product \mathbb{N}\times\mathbb{N} is countable (pairs can be listed in a grid and read diagonally).
  • The power set \mathcal{P}(A) always has strictly larger cardinality than A.

A bit of history

Georg Cantor (1845–1918) developed the modern theory of sets and cardinal numbers in the late 19th century. He showed that infinite sets can have different sizes, that \mathbb{R} is uncountable, and that the cardinality of \mathbb{R} is 2^{\aleph_0}.

Cantor’s ideas were initially controversial, but they eventually became a central part of modern mathematics and influenced logic, topology, analysis, and many other fields.

A light interlude: Pikabu the Cat

To keep things a bit more personal, imagine the set

    \[ C = \{\text{your Pikabu cat}\}, \]

a set with exactly one element. Its cardinality is 1. Contrast this with the set of all photos you have ever taken of your Maine Coon — that set might be finite or (practically) “infinite,” depending on how attached you are to your camera.

The Continuum Hypothesis

A natural question is whether there is a cardinal strictly between \aleph_0 (the size of \mathbb{N}) and \mathfrak{c} (the size of \mathbb{R}). The Continuum Hypothesis (CH) says that there is no such intermediate size; in symbols,

    \[ \mathfrak{c} = \aleph_1. \]

\medskip

In the 20th century, Kurt G\”odel (1940) showed that CH cannot be disproved from the usual axioms of set theory (ZFC), and Paul Cohen (1963) showed that CH cannot be proved from them either, assuming those axioms are consistent. In technical terms, CH is independent of ZFC.

This result has deep philosophical consequences: even with a very widely accepted system of axioms, some natural questions about sets (and about the continuum of real numbers) cannot be settled one way or the other.

Closing remarks

Cardinal numbers give a precise way to compare the sizes of sets, going far beyond finite counting. They reveal that infinities themselves come in different sizes and lead naturally to questions, such as the Continuum Hypothesis, that touch the foundations of mathematics.

The discussion with Bjab prompted me to add these two appendices.

Appendix 1.

Let \mathbb{N} denote the set of all natural numbers. We prove that the set 2^{\mathbb{N}} is uncountable. The reasoning is by contradiction as with the Cantor’s diagonal proof. Suppose that it is countable. That is suppose that there exists a sequence  of subsets of \mathbb{N} such that every subset of \mathbb{N} coincides with some  element of this sequence. Call the elements of this sequence S_1,S_2,.... Once we have this sequence we construct a new subset S as follows:

    \[ S=\{n\in\mathbb{N}: n\notin S_n\}.\]

We show that this new set is not being one of these S_n. Indeed, take any n, and the corresponding S_n.  Then either n is in S_n or is not in S_n. If n is in S_n, then n is not in S, so S_n and S are different. If, on the other hand n is not in S_n, then n is in S. Again S_n and S are different. As this holds for any n, we deduce that S is not in the collection {S_n\}, contrary to our assumption.

 

Appendix 2.

  • Norman J. Wildberger, a contemporary mathematician (formerly at UNSW Sydney, with expertise in algebra, geometry, and rational trigonometry), is one of the most vocal modern critics. In his “Math Foundations” series and writings (e.g., “Uncomputable decimals and measure theory: is it nonsense?”), he rejects actual infinities, questions the coherence of infinite decimal expansions as “myths,” and argues that Cantor’s proof (and the uncountability of the reals) relies on ill-defined objects. He claims this invalidates the diagonal argument and broader transfinite set theory.
  • L.E.J. Brouwer (founder of intuitionism) and associated intuitionists/constructivists questioned the meaning of the proof, even if some variants of the diagonal argument can be made intuitionistically valid. They reject non-constructive existence proofs and the idea of a “completed” set of all reals as a finished totality. The reals are handled differently in intuitionistic logic (often via choice sequences or spreads), so uncountability holds in a weaker sense but without the full classical implications.
  • R.T. Brady and P.A. Rush (logicians working in relevant and paraconsistent logics) published a 2008 paper titled “What is Wrong with Cantor’s Diagonal Argument?” in Logique et Analyse. They use an entailment logic based on “meaning containment” (which avoids the full law of excluded middle and disjunctive syllogism) to argue that the diagonal reasoning fails or leads to different conclusions in their framework. They contrast this with intuitionism and explore impacts on naive set theory.
  • Historical figures like Henri Poincaré dismissed transfinite set theory as a “grave illness” of mathematical reasoning, and Ludwig Wittgenstein (in a finitist/philosophical vein) analyzed the diagonal argument as invalid due to confusions between intensional laws and extensional sets. 
  • Hermann Weyl (1885–1955), one of the 20th century’s most influential mathematicians (known for work in analysis, geometry, and quantum mechanics), strongly criticized Cantor’s set theory. He argued that classical logic was abstracted only from finite sets and mistakenly applied to infinities, calling this the “Fall and original sin” of set theory. Weyl sought more constructive foundations for the continuum and viewed Cantor’s approach as permeated by contradictions
This entry was posted in Philosophy, set theory and tagged , , , . Bookmark the permalink.

33 Responses to Counting infinities

  1. SasaM says:

    “One can show that \mathfrak{c} = 2^{\aleph_0}, the cardinality of the power set of \mathbb{N}.”

    Does the above quoted statement mean that set of all subsets of the set of natural numbers is uncountable infinite, same as set of real numbers?

    Been a bit confused by the CH, does it essentialy say that there are only two types of infinities, countable and uncountable?
    Because, intuitevely, there is cca two times more integers than natural numbers.

  2. SasaM says:

    Sort of an interesting conjecture from the post, if understand it right, would be in relation to geometry, dimensions of spaces and fields, and describing consciousness and densities.

    It was said before that dimension of Clifford algebra Cl(n) is 2^n, which for finite n is finite number.
    If n is countable infinity, then 2^n is uncountable infinity, which ‘contradicts’ what the C’s said about dimensions of geometric algebra to describe consciousness and densities. IOW, according to them, Cl(infinity) would not be the right algebra for the job even if n would be countable infinity.
    Also, countable infinite tensor product of Clifford algebras for finite n, like Cl(4)×Cl(4)×…. would result in some finite 2^n, like 2^4=16, to the power of countable infinity, which is again uncountable infinity according to what the post here said. IOW, infinite tensor product of finite (and infinite) dimensional Clifford algebras would also have uncountable infinite number of dimensions.

    On the other hand, a product of finite number of countable infinities would still be countable, as well as countable infinite iterations of such a product, like N×(N×N×…×N) = N×N^n = N^(n+1) where n is finite number. IOW, a product of finite number of countable infinite sets, like integers, rationals and algebraic numbers, as well as infinite iterations of such a geometric ‘space’ or ‘field’, would have countable infinite number of ‘dimensions’.

    FWIW.

  3. John G says:

    The Cs said countable infinity for the geometric algebra and back in 2018 they said uncountable infinity in relation to branes. They also in 2018 said the relation between infinity and the finite number of spacetime dimensions is to think of the spacetime dimensions infinitely repeating (which sounds countable). I suspect the idea is that one brane universe is a Cl(n,C) for each of the countable infinite number of spacetime vertices in a single brane universe state and all the interactions for all the brane universe states becomes a 2^n uncountable infinity via the n being a countable infinity. In other words you would have a Fock space of countable infinite dimensions but all the operators connecting all Fock spaces would be uncountable. The n of Cl(n) w0uld be the Fock space dimension and the 2^n would be operators getting you to all the other Fock spaces.

    • SasaM says:

      That seems like an interesting possibility, thanks.

      I’ve been thinking in sort of relatively simpler terms; kind of infinite, but discrete (quantized) or grid-like, and thus with countable number of ‘points’, space or field (perhaps something in line with 6-dim space like presented in Ark’s recent paper) of information (possibly thoughts?), over which there would be an ‘algebra’ in the sense of possible ‘geometric connections’ or relationships between/among the ‘points’ of such a grid.
      Relationships in the form of configurations within the field based on algebra ‘rules’ (truth) would lead to consciousness, and ‘number’ of actualized configurations and/or awareness of possible configurations that could be actualized within the field or given field segment would speak about densities. Or something along those lines.

      • John G says:

        Thinking discrete countable infinity even if that gets a little weird for something like a degenerate metric seems good to me. 6-dim conformal would seem important too. I also liked Anna last year bringing up phase space in relation to a question you asked. Like from Ark’s previous post, an orthogonal and symplectic geometric algebra within the field.

        • DMcBride says:

          IMO there is the set theoretic foundation, that is, is your algebra over the field of real numbers?

          If someone, you’re in an uncountable infinity with regards to the purely number theoretic ‘sets’ and ‘subsets’. Going out into spaces and subspaces is going to vectors, extensions, matrices, subspaces, creating your geometries from your algebras… I don’t know if you get to the higher constructions without explicit field basis initially.

  4. Bjab says:

    Hi,
    there’s a logical error somewhere in this diagonal reasoning.
    But where? – I explain.
    To be able to replace the twelfth digit (after the decimal point) in the twelfth number, one would have to KNOW that twelfth number (or at least KNOW its expansion to the twelfth digit). Therefore, one must KNOW all (each individual) numbers in the sequence. What does it mean to KNOW a number? It means having access (a finite independent description of access) to each of its digits in the expansion. Only countably many descriptions of such accesses are possible. A diagonally constructed number has no independent description, so it is no surprise that it doesn’t appear in a sequence of numbers that allow for its construction.
    To summarize – in the sequence, we are dealing with, we have all real numbers (in the range 0, 1) that do not allow for construction, or we only have, in the sequence, numbers with a finite independent description.

  5. arkajad says:

    Thanks! I have added a paragraph (in bold) at the beginning of Cantor’s diagonal trick section.

    • Bjab says:

      To make it consistent – in the formula, below the words “uniquely represented by such a sequence”, there should be d_n instead of c_n

    • Bjab says:

      Ark, however, your new paragraph doesn’t change much. We’d still need to know the nth term of each sequence (the equivalent of a number) to construct the new number. So my earlier comment remains valid. The diagonal proof stinks.

      • arkajad says:

        The proof is by contradiction So we assume that all our sequences can be numbered. We take the seqeunce x_1. It starts with some number d11. We take it and change it. Then we take sequence x_2. We take its second element. We proceed doing it for each n. From the sequence x_1,x_2,…, assuming we are given this sequence, we have construct new sequence. This is a construction algorithm build upon what we assume we have been given.

        I personally, see no problem.

        Perhaps I will add another proof of a related statement. This will widen a little bit our discussion, and it should be educative.

        • Bjab says:

          “Then we take sequence x_2. We take its second element.”

          To take second element of sequence x_2 we have to KNOW this second element.

          To take 2026th element of sequence x_2026 we have to KNOW this 2026th element.

          To KNOW the elements of the sequence, we must have a finite, independent description of this sequence.

          The newly created number (sequence) has no independent description – its description depends on an infinite number of sequences.

      • DMcBride says:

        The need to enumerate an irrational number endlessly doesn’t contradict the notion that that is precisely what is making the mathfrak{c} of a different cardinality to that of the natural numbers.

        We would simply have you accede to the notion that access is needed, and the numbers can be enumerated when questioned by the mathatician to tease out more and more numbers–call it a querying function to continue expanding the infinite decimal.

        It appears to me now to illustrate the inordinate amount of information in the uncountable compared to the countable.

  6. arkajad says:

    No, no, no. Let us phrase it differently to make it clear.
    We reason by contradiction. Assume that our set of sequences countable. What does it mean? It means there EXISTS a sequence x_1,x2_,… of sequences. What does it mean that the sequence of sequences EXISTS? It means that each of its members EXISTS, But a member is again sequence. What does it mean that it EXISTS? It means that each of its members exists. But now it is a number. This number exists, we give it a name (d_{nk}.

    Where do you have a problem with this reasoning? Perhaps you will say that a set can well exist without requiring its all elements to exist? For instance empty set? But all elements of the empty set exist!

    • Bjab says:

      Let x be a real number (or a sequence or subset of natural numbers). There are two possibilities: either there exists a finite independent description of this number that would allow its identification, or there does not. If a number x that does not have a finite independent description were to appear in the sequence of numbers under consideration (say, at position n), the algorithm for constructing the “auxiliary number” would fail on this number (because the nth digit of this number would be unrecognizable).

      There are only countably many finite independent descriptions of numbers (e.g. sqrt(2) is such finite indepedent descrpition identifying that number – we may KNOW every digit of it).

      • arkajad says:

        For me it does not matter whether the digit is recognizable or not. I do not even know what “recognizable” is? By whom? It does not matter. For me it is enough that it EXISTS, so, in principle, can be used to construct other existing objects.
        But I understand that you may think that gives us too much freedom, and too much freedom may lead to contradictions and paradoxes. Well, sometimes it may create a paradox, but often it creates something useful.

        • Bjab says:

          Ark: “By whom?”

          By algorithm.

          Therefore, two approaches to the problem are possible.
          One approach (yours) assumes that the algorithm that constructs the successive digits of the desired number can work because it has paranormal access to the required digits of numbers from a countable sequence. The second approach (let’s call it mine) assumes that such access is only possible if the successive numbers in the sequence have a description that allows determining the required digits.

        • Bjab says:

          A similar dichotomy also holds in the case described in Appendix 1. Here the problem comes down to whether it is possible to state whether n is in S_n without a defining description of S_n.

          • arkajad says:

            The problem is that I am using the classical set theory, as described for instance in Kuratowski, Mostowski “Set Theory”, or in Bourbaki “Set Theory”. Cantor’s reasoning can, in fact, be adapted to be valid also within other versions of set theory (by constructivists, intuitionists). You are trying to use some other set theory, and some other philosophy of mathematics. It would help if you could expand your ideas about what kind of this new mathematics is supposed to be? How far your mathematics can go? Do real numbers exists at all in your mathematics? Do the set of integers exist? And what does it mean that something “exists”? Perhaps you can write a post on this subject?

          • Bjab says:

            “Do real numbers exists at all in your mathematics? Do the set of integers exist?”

            I make mistakes when I am irritated that something does not fit with the ideas I have established in my beliefs.

          • arkajad says:

            I think that there is no reason to believe that everything that exists must necessarily be described by finite means (or algorithms). At least I do not see any reason for such a belief. Of course one may be curious to see how far we can go restricted ourselves in this way. But that is a personal taste and preferences.

          • Bjab says:

            What exists that is not described? 🙂

  7. arkajad says:

    “What exists that is not described? ”

    Every element of every infinite sequence of of the elements of {0,1,2,3,4,5,6,7,8,9} . It exists and it is one of these 10 numbers.

    • Bjab says:

      “Every element of every infinite sequence of of the elements of {0,1,2,3,4,5,6,7,8,9} . It exists and it is one of these 10 numbers.”

      There are two possibilities.
      Either some element of a given sequence is described (determined) by the description (recipe (my be not full)) for this sequence (and this contradicts what you wrote (that: Every element of …))
      or
      this element can not be determined (described) due to the lack of any description (representation) of the said sequence and then it is not possible (without the God’s knowledge) to carry out the algorithm of diagonal proof.

    • arkajad says:

      I asked Perplexity: about machine proofs of Cantor’s theorem. Here is the answer:

      Yes, Cantor’s uncountability proof (and many variants) have been fully formalized and machine‑checked in several proof assistants, and the libraries are publicly available.

      Projects and sites you may have in mind
      There isn’t just one site, but several long‑running “formalization of mathematics from the axioms” projects:

      Isabelle/HOL: A large library of real analysis and set theory, developed over decades by Paulson and others.

      HOL Light: John Harrison’s system, used in the Flyspeck project and containing a detailed formalization of the reals and basic measure theory.

      Coq, Lean, and others: Each has a math library with reals and cardinal theory (e.g. mathcomp, Coq’s standard library; mathlib for Lean).

      In all of these, the fact that R is uncountable is proved formally, typically via a version of Cantor’s diagonal argument or an equivalent characterization.

      Where Cantor’s uncountability appears
      Concretely:

      In HOL Light, the standard library includes a construction of the real numbers and a theorem that there is no bijection between
      N and R; the development is used as a basis for later real analysis and is part of the libraries that have been ported or translated into Coq and Isabelle.

      In Isabelle/HOL, the “HOL-Complex” and related libraries include the usual result that the reals are uncountable, needed for standard topology and measure theory.

      In Coq, the real numbers (in the standard library or in CoRN/MathComp-Analysis) come with the theorem that there is no enumeration of all reals; the proof is again a mechanized version of Cantor’s style argument.

      These are machine‑checked proofs starting from the foundational axioms of each system (HOL or something close to ZF/ZFC) and standard constructions of R.

  8. arkajad says:

    “There are two possibilities. ”

    There is a third possibility: we do not know (it may well be undecidable), and we do not care, since it is, for us, irrelevant. So asking these additional questions that you are asking is permissible, but not obligatory. Question of personal taste.

    BTW On my Substack blog I replied to one comment, and it may be relevant to our discussion. Here is what I replied there:

    Thanks a lot for your thoughtful comment and for taking the time to raise this point.

    You’re right that in ZFC the existence of an infinite set is taken as a separate axiom – the axiom of infinity – and is not derivable from the rest of the axioms of ZF. In that precise sense, classical set theory does not “prove” that infinite sets exist; it assumes at least one infinite set (typically modeled by the natural numbers).

    What set theorists then study is what follows if you accept that assumption, together with the other axioms. One could certainly choose a different foundational system that does not postulate infinity; it would just be a different mathematics, with a correspondingly more limited universe of sets.

    So I agree with your underlying point: the existence of actual infinities is not something forced on us by pure logic alone, but a substantive mathematical choice. In this article I’m working inside the usual ZFC framework, where that choice has been made explicitly.

  9. Bjab says:

    For me, however, the diagonal proof has a certain flaw. People don’t see that it involves calculating a new (computable) number from a sequence of numbers, not all of which are computable. Doesn’t this make you bother?

  10. arkajad says:

    You’re pointing to a genuinely interesting tension, and it’s useful to separate two levels.

    Cantor’s classical proof lives in a very generous universe of sets: it allows arbitrary infinite sequences of digits, without any requirement that they be computable or definable in a finite way. In that setting, the diagonal step is simply a pointwise definition of a new sequence; the proof does not claim this sequence is computable, only that it exists as a set of positions where digits are flipped.

    If, however, we restrict attention to computable real numbers, then we are working in a much smaller universe. There, diagonal arguments are still valid, but their conclusion is different: they show that no single algorithm can list “all” computable reals in a way that is stable under its own diagonalization. This is the kind of reasoning used in computability theory and in Turing’s analysis of the limits of algorithms.

    So the diagonal method itself is sound; what changes is the background notion of “number” we allow. Classical set theory assumes arbitrary, possibly non‑computable reals and gets uncountability; computability theory assumes only algorithmically generated reals and gets instead strong limitations on effective procedures. Your concern is exactly where these two perspectives rub against each other.

    • Bjab says:

      Inspired by your use of AI I asked AI about: “cantor’s diagonal proof restricted to the set of computable real numbers”

      3. The key issue: the list of computable reals is not computably enumerable in digit form

      There is an enumeration of all computable reals (because they are countable), but:
      there is no effective procedure that, given n,k, always computes the k-th digit of the n-th computable real in a total uniform way.

      Why not?

      Because determining whether a program correctly computes a real, halts properly, etc., runs into undecidability phenomena related to the Halting Problem.
      So the diagonal real constructed from an arbitrary enumeration need not itself be computable.

      4. What diagonalization actually proves here

      If you had a computable enumeration of computable reals:
      r1, r2,…

      where digits can be effectively accessed, then the diagonal real would also be computable.

      But then it would differ from every rn, contradicting completeness of the list.

      Therefore:

      There is no computable enumeration of all computable reals.

      This is a stronger and more precise statement.

      5. Summary
      The full set of reals is uncountable by Cantor diagonalization.
      The computable reals are countable.
      However, they are not computably enumerable in a uniformly effective way that allows diagonalization to stay inside the computable reals.
      Diagonalization over an effective list of computable reals produces a computable real outside the list, proving no such effective list exists.

      So the “failure” of diagonalization here is not about countability; it is about effectiveness/computability of the enumeration.

      Powyższe jest bardzo interesujące ale na pierwsze spojrzenie jest tam trochę machania łapkami (tonący łapie się brzytwy)

      • arkajad says:

        My experience with AI suggests the following:
        AI is not like a human being. It is not getting upset when we are not satisfied with its answers and demand more and better. So, one should never hesitate for a second to express your unsatisfaction with logic and clarity, or with incomplete answers. AI can always to do more and better. It is programmed to give you first a cheap answer, with least effort. It is even “happy”, in a sense, when its first or second answer does not satisfy you and you openly express your dissatisfaction.

  11. arkajad says:

    My AI (Perplexity) makes also this comment:

    ZFC easily defines and proves “computable reals are countable”. The countability follows because computable reals are parametrized by codes (programs), and the set of codes is countable; this is standard recursion‑theoretic material formalizable in ZFC.

    ZFC does not have a general notion of “definable real” as a set. The phrase “the set of all definable reals” is not first‑order definable in ZFC, and there are well‑known subtleties around the Myhill–Scott work on definability from ordinals etc., precisely because “definable” is a meta‑notion. For “computable”, by contrast, we can fix a particular formal model (Turing machines) and write down the corresponding formula

Leave a Reply