junk theorems

I need more of these, they're funny.

It turns out that Lean has some fantastic junk theorems. A junk theorem is a theorem which is technically valid, but only because it mixes up abstractions which it probably¹¹ According to some shouldn’t. It’s a theorem of Lean that the set

is a continuous, non-monotone surjection. This is, of course, because that set is a function R → {0, 1}, where z maps to the value of z ≠ 0 as a boolean. And of course the set of booleans naturally takes the discrete topology and the order where False < True.

Most expositions you’ll find online about “junk theorems” give examples like

and so on.

I would like to do some apologetics for these junk theorems, though. I think these theorems are in fact perfectly legitimate. Like, you have to equate the natural numbers with the finite ordinals, but I think this is in fact the correct thing to do. One simply has to accept that < is ∈, ≤ is ⊆ min is ∩, max is ∪, and 2⁰ is 𝓟(0), and actually those theorems start seeming basically correct.

(Equating subsets with indicator functions is actually pretty reasonable too, I think.)

Here are some actual junk theorems:

1⨿2 should be the same thing as 3. But actually 1⨿2 = {(0, 0), (0, 1), (1, 1)} under the most common definition. 3×3 should, perhaps more obviously, be 9, but actually it’s equal to {(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (2, 2)}. And 2² should be 4, just like 2⁰ is 1 and 2¹ is 2, but actually 2² is {∅, {0}, {0, 1}, {1}} = {0, 1, 2, {1}}.

The problem is that we need to be checking for equinumerosity²² For the first two examples, you might want to instead assert that they have the same order type, if you want to actually treat the naturals as well-ordered sets. You give 1⨿2 and 3×3 the lexicographic ordering. But this fails on 2², which most naturally takes the order given by ⊆.

…or does it? Ordinal exponentiation is of course defined, and it simply uses the lexicographic order—though in that case, you definitely want to be defining 2² as the set of functions {f: 2 → 2} = {{(0,0), (1,0)}, {(0,1), (1,0)}, {(0,0), (1,1)}, {(0,1), (1,1)}}. This is, of course, rather in line with the way the nonzero reals are defined as a function in Lean.

It shouldn’t be unsurprising that you can well-order 2², that follows from the axiom of ultrafinite choice. The question is whether you should. And—well, I do suppose it seems like a good idea for the purposes of ordinal arithmetic, including the special case of natural number arithmetic. But it’s much less natural than for the coproduct and product cases. That’s because Woset has coproducts and products that play really nice with Set, but it doesn’t have exponential objects at all. The lexicographic order is mostly only useful for ordinal arithmetic, in almost any other case you’re gonna wanna use ⊆., not set equality.

We also have:

This is because the basic set theoretic definition of an ordered pair really sucks³³ To be fair, it’s less confusing if you actually use any amount of your better judgment in determining whether to render a set as 1 or 2 instead of {0} or {0, 1}.. Ordered pairs ought to be functions 2 → X for some X, but in a context where you’re actually bothering to define an ordered pair as being a certain set is one where you probably haven’t defined functions yet⁴⁴ And really I’ve been playing a little fast and loose with the distinction between a function and its graph here.. You can also do a bunch of really dumb stuff with intersections of ordered pairs and so on.

I leave you with: “The empty topological space is the set {1, 2}”.