| Description | You are probably aware that if you have three natural numbers x, y and k with k ≠ 0, if kx = ky, then x = y.
Combinatorially, this means that if there is a bijection f between {0, ..., k-1} × X and {0, ..., k - 1} × Y where X and Y are finite sets, then there is a bijection h between X and Y.
Interestingly, this remains true if X and Y are infinite. The easiest proof of this fact relies on the axiom of choice, which stipulates that any infinite set can be sorted (i.e. well-ordered). For a variety of reasons (philosophical and/or technical), mathematicians and logicians sometimes want to prove things without using this axiom. In this case, one such reason is that one might find it sad that the underlying algorithm, when specialized to the finite case, consists of ignoring the input f and eagerly building a bijection h from lists enumerating X and Y in a sequential manner.
A proof without the axiom of choice was only proposed rather recently; see https://arxiv.org/abs/1504.02179 for a very short exposition (that's where the banner picture is from) and https://arxiv.org/abs/1504.01402 for the paper, which contains a number of further remarks. Those write-ups convey good intuitions and some very nice illustrations, but remain rather informal, especially when it comes to the complexity-theoretic remarks. I believe there are several nice things one could do around these results (non-exhaustive list):
* Write computer programs that illustrate examples for finite cases (much like what is done in the papers with the cards, but allowing for more scenarios/visualisations)
* Write the proof up in a more formal way
* Formalizing the theorem in a proof assistant such as Lean, Rocq or Agda.
* Clarify what is the computational model that makes the complexity analysis in https://arxiv.org/abs/1504.01402 go through and compare with other models of infinite computation from the literature, such as ordinal Turing machines.
* Analyzing the logical strength of this theorem in details: the principle of excluded middle is used in the proof, but do we need its full power? |
|---|
