Cantor’s Theorem about dense linear orders states that any two linear orders which are

• countably infinite
• dense
• do not have endpoints (i.e. unbound from above and below)

are isomorphic.

The standard proof is a quintessential application of the back-and-forth method, where one builds an isomorphism between two countable structures and by iteratively building up a finite partial isomorphism: grab the “next” point in and find some point in so that these two points extend the existing partial isomorphism; and then do the same thing starting from . Continuing in this fashion, at stage you have a full isomorphism (since both structures are countable).

While the proof may not too difficult to understand, visualizing the isomophorisms produced by this method is another story. Fortunately, Cantor’s Theorem is constructive, with a few caveats¹, so we can actually construct these isomorphisms. In order to do to this, I used Coq to formalize Cantor’s Theorem in the abstract, and then provided some examples of these orders. In particular:

• is a countable dense linear order without endpoints
• If is such an order and , then (with the induced suborder) is also
• If are two such orders, then (with the coproduct order) is also
• If are two such orders, then (with the lexicographic order) is also

The full verification effort can be found in this repo.

After extracting a couple of examples to Haskell, I was able to produce these three plots:

An order isomorphism from to :

An order isomorphism from to :

An order isomorphism from to :

---

1: To avoid using choice principles, we assume that countability is witnessed by a bijection with the natural numbers, density is witnessed by a midpoint-finding function, and lack of endpoints is witnessed by functions which find points to the left and right.