.. title: Everything is just so small
.. slug: everything-is-just-so-small
.. date: 2025-05-25 22:42:59 UTC+02:00
.. tags: 
.. category: 
.. link: 
.. description: 
.. type: text
.. has_math: true

Often in mathematics, we have trouble talking about the sizes of things and
understanding whether a thing is small enough to handle or too big to examine
fully. In the most basic and natural form, a collection of objects is pretty
small if it's finite because there's a *computable* way to list all of the
objects of the collection, exhaust them, and witness that there are objects you
can no longer fit into the collection. It is remarkable that, with reasonable
though controversial assumptions, 'everything' is really tiny, and you can
always count past all of its elements, and I mean *count*. 

In the following, I present my **informal** description of the process of
transfinite recursion and the astonishing implications of the axiom of choice
on the notion of size.

.. teaser_end

The ordinals and transfinite induction
======================================

The story begins with ordinals, really really gigantic 'numbers'. Ordinals start
at 0, count all of the natural numbers, and then count beyond all of them and
beyond that, and beyond that still, and then add 1, and again, and again, and
then go beyond all of that and still counting. The ordinals are so big that they
cannot even tell you how big they can get.

Let's see this more formally. Ordinals are, in fact, sets and are constructed
from the ground up using two simple operations: the successor which from a set
:math:`X` produces the set :math:`X \cup \{X\}` and the limit which from sets
:math:`\{X_i : i \in I\}` produces the set :math:`\bigcup_{i \in I} X_i` and
starting with a base ordinal 0 corresponding to the empty set. For a computer
scientist, they are generated (but not purely inductively!) by:

.. code-block:: agda

    zero : Ordinal
    succ : Ordinal -> Ordinal
    limit : Set Ordinal -> Ordinal

The ordinals are defined as sets which are transitive and well-ordered. What
that means is that any subset of an ordinal :math:`\alpha` has a smallest
element, and any element of :math:`\alpha` (which is a set since everything is a
set!) is also itself a subset of :math:`\alpha`. It turns out, the collection of
ordinals is not a set! It's too big to be a set! In fact, ``Ord`` the collection
or ordinals is transitive and well-ordered, so if it was a set, it would be an
element of itself, contradicting a basic axiom of set theory: regularity, in
particular, that :math:`\forall x,  x \not \in x`.

In a simple world (set theory without the axiom of infinity), there would be no
infinite set and all the ordinals would be finite and we would be stuck at the
union step of all the finite ordinals as we would not be able to form a set
containing all finite ordinals as there is infinitely many of them. But in such
a world, things can be boring, and I wouldn't be writing an post on how
everything is small. The surprise is that once we admit the existence of *any*
infinite set, we can get sets waaaaay bigger than the one we introduced!  Here's
one set that's bigger than :math:`ω`, the set of natural numbers, for example:
:math:`ω + 1`. It is a set containing all finite ordinals as elements **and**
the infinite ordinal :math:`ω`. You can tell that these two sets are distinct
because :math:`ω` is an element of :math:`ω + 1` but not of :math:`ω`. In
general, any ordinal :math:`α` has a strictly larger ordinal which is :math:`α +
1`, but it also has ordinals much larger than that.  Here's one: :math:`ω + ω`.
This ordinal is obtained as the limit of :math:`ω + n` over all finite ordinals
n.

The possibility to take limits whenever you feel that you're no longer
progressing with successors instills the notion of transfinite induction.
Transfinite induction is a way to construct functions out of an ordinal by
defining the function, inductively, on the different kinds of ordinals. First
you define :math:`f(0)` as some (uniquely determined) element, then you can
define, for all :math:`α`, :math:`f(α + 1)` uniquely determined up to the
knowledge of :math:`f(α)`, and similarly, you can define :math:`f(\sup_{\beta <
\alpha} \beta)` also uniquely determined up to the values of :math:`f(\beta)`
for all :math:`\beta < \alpha`.

This is an extension of induction on the natural numbers and with the axiom of
choice, it allows us to do so much!

Proofs by transfinite induction
================================

Just as transfinite induction allows us to construct functions, it also
allows us to construct proofs parameterized by ordinals. This provides an
incredibly powerful tool for finding proofs: brute-force look for them so many
times (by going through all the necessary ordinals) and you will eventually land
on what you are looking for. This is very well illustrated by the Knaster-Tarski
fixpoint theorem.

.. admonition:: Knaster-Tarski fixpoint theorem

    Any monotone function :math:`f : P(X) \to P(X)` on a complete lattice has a
    least fixpoint :math:`\mu f` given by transfinite iteration of :math:`f`
    starting with :math:`\bot`.

Let's unpack this a bit, staying somewhat informal. A *lattice* :math:`L` is a set of
elements that can be compared with one another :math:`x \leq y` and that has a
least upper bound (supremum) and a greatest lower bound (infimum) for any two
elements :math:`x` and :math:`y`. It is *complete* if these infima and suprema
exist for any subset of the lattice, in particular, there is a global smallest
element :math:`\bot` and a global largest element :math:`\top`, the infimum and
supremum of :math:`L` respectively. A *monotone function* is a function that
preserves the ordering :math:`x \leq y \implies f(x) \leq f(y)`, and a *least
fixpoint* is the smallest point :math:`x` such that :math:`f(x) = x`.

.. admonition:: Proof attempt

   Define, inductively on :math:`\mathbb N`, :math:`x_0 = \bot`, :math:`x_{n+1} = f(x_n)`.
   As :math:`x_0 = \bot` is the smallest element of the lattice, we
   have :math:`x_0 \leq x_1`. But as :math:`f` is monotone, we also have that
   :math:`x_n \leq x_{n+1} \implies x_{n+1} \leq x_{n+2}`. As such, we obtain an
   increasing *chain* of elements :math:`x_0 \leq x_1 \leq x_2 \leq \ldots` in
   the lattice, which has a least upper bound :math:`x_\omega = \bigvee x_n : n
   \in \mathbb N` which is at least as large as :math:`x_n` for all :math:`n`.
   Then, consider applying :math:`f` to :math:`x_\omega` to get

    .. math::
        
        f(x_\omega) = f(\bigvee_{n \in \mathbb N} x_n) \stackrel{?}{=} \bigvee_{n \in \mathbb N}
        f(x_n) = \bigvee_{n \in \mathbb N} x_{n+1} = x_\omega

Unfortunately, the step :math:`f(\bigvee_{n \in \mathbb N} x_n) = \bigvee_{n \in
\mathbb N} f(x_n)` is not actually correct. Functions that have this property
are known as *continuous* functions, and a version of this theorem can be given
for such functions — it's the Kleene fixpoint theorem. However, with
transfinite induction, the continuity condition is no longer necessary! As
:math:`x_n \leq f_\omega`, and :math:`f` is monotone, we have that :math:`f(x_n)
\leq f(x_\omega)` for all :math:`n`; therefore, :math:`\bigvee_{n \in \mathbb N}
f(x_n) = f_\omega \leq f(x_\omega) = x_{\omega + 1}`, meaning that the chain
continues beyond limit ordinals like :math:`\omega`. As such, we can build
chains of any length. In particular, it's impossible to build a strict chain
indefinitely as no matter the size of :math:`L`, there is an ordinal
:math:`\alpha` that is larger than it, so at :math:`x_\alpha`, it's impossible
that we are still producing new elements in the chain; i.e. :math:`x_\alpha =
x_{\alpha+1} = f(x_\alpha)`.

Let's reiterate what we've just done: since we can count for so incredibly long,
we have a strategy to generate so many elements in a lattice that, no matter the
size of the lattice, we **will** eventually run out of new elements and reach a
fixpoint. That is quite incredible if you ask me!

.. Axiom of choice
.. ===============

.. The axiom of choice, a bit controversial, states that there is a way to
.. simultaneously pick exactly one element from each non-empty set in any family
.. (set) of sets. The axiom of choice is not an axiom but is a trivial tautology
.. for finite families of sets. You can always pick some element of a set, and
.. repeating that finitely many times gives you a choice of elements from each set.
.. Once we talk about infinite collections of sets, it's no longer obvious that you
.. can do that infinitely many times, simultaneously. This is where the axiom of
.. choice comes in to tell us that, yes, we can.

.. *TO BE CONTINUED*