Proof that LEM is equivalent to the well-ordering of $\Bbb{N}$

Question

John L. Bell's Intuitionistic Set Theory contains an exceedingly slick demonstration that the law of excluded middle is equivalent to the well-ordering of the natural numbers $\Bbb{N} := \{ 0, 1, 2, ... \}$ - a demonstration so slick, I find myself doubting it.

His logic runs as follows: let $p$ be some logical proposition, and $S_p \subset \Bbb{N}$ be a corresponding subset such that $$S_p := \{0, 1\}, \text{ if } p \text{ is true, and } S_p := \{1\}, \text{ if } p \text{ is false.}$$ (Explicitly, he defines $S_p := \{ x | x = 0 \land p \} \cup \{ 1 \}$.) Then since $\Bbb{N}$ is well-ordered, $S_p$ has a least element $n$. If $n = 0$, $p$ is true; if $n = 1$, $p$ is false. QED, Bell claims.

I'm struggling with the following aspects of this proof:

1. The $\{ x | x = 0 \land p \}$ seems circular/question begging/ill formed to me. How can I condition an element's membership in a set, on the truth or falsity of some arbitrary proposition $p$ with no relation to the element itself? (This may be a perfectly well-formed definition syntactically, but it still makes me a little wary.)

2. Without the assumption of LEM, I guess Bell is telling me $S_p$ doesn't have a least element, but how can that be? By construction, and with no assumption on the truth value of $p$, $S_p = \{0, 1\}$ or $S_p = \{1\}$; there's no secret third thing $S_p$ could be, or is there?

3. More generally, what does intuitionistic set theory claim $S_p$ "looks like", for a proposition $p$ which can neither be proven true nor false (intuitionistically)?

Answer 1

It's possible that this whole procedure will make more sense if you see what it means in a concrete model of intuitionistic set theory. Let's work with the topos of sheaves on $\mathbb{R}$. I'll quote here some basic facts about this topos which you might take on faith, or you might treat as exercises depending on your background.

• In this world, the truth values are exactly the open subsets of $\mathbb{R}$.
• The natural numbers object $\underline{\mathbb{N}}$ is the sheaf sending the open subset $U \subseteq \mathbb{R}$ to $\underline{\mathbb{N}}(U) = \{ \text{locally constant functions } U \to \mathbb{N} \}$. You might think of elements of $\underline{\mathbb{N}}(U)$ as "natural numbers defined only on $U$"
• An "element" $n \in \underline{\mathbb{N}}$ is a locally constant function $\mathbb{R} \to \mathbb{N}$ (that is, a natural number defined everywhere). Note that, since $\mathbb{R}$ is connected, an everywhere defined locally constant function must be constant!
• A "subset" of $\underline{\mathbb{N}}$ is really a subsheaf of this sheaf. That is, if $X \subseteq \underline{\mathbb{N}}$ then we must have $X(U) \subseteq \underline{\mathbb{N}}(U)$ for all $U$, in a way that's compatible with the restriction maps.
• A statement $\varphi$ is true in the topos if and only if it's true on every open set $U$.
• A proposition (read: truth value, read: open set) $p$ is true on $U$ if and only if $U \subseteq p$. Notice that the only proposition which is true in the topos (by which again I mean "true on every $U$") is the whole set $\mathbb{R}$. Every other (nonempty) proposition is "true somewhere, but not everywhere", so that it's difficult to directly examine from "inside the topos".

Now it becomes clear how a subset $X \subseteq \underline{\mathbb{N}}$ which contains an element might fail to have a least element! If we fix a proper open subset $U \subsetneq \mathbb{R}$, then we can define a subsheaf $X \subseteq \underline{\mathbb{N}}$ by

$$ X(V) = \begin{cases} \{ 0, 1 \} & V \subseteq U \\ \{ 1 \} & V \not \subseteq U \end{cases} $$

(notice here we're using LEM in "the real world" (or the metatheory, if you like) to construct this sheaf. But that has nothing to do with LEM as interpreted in the topos, which is false.)

This subsheaf is inhabited since the statement $1 \in X$ is true (since $1 \in X(V)$ for each $V$). However, the statement "$1$ is the least element" cannot be true, since there are open subsets $V$ for which it's false! Thus we see that $\underline{\mathbb{N}}$ has inhabited subsets with no least elements!

---

Now, what about that proof of LEM? Well how do we interpret $X = \{ x : \underline{\mathbb{N}} \mid x = 0 \land p \}$?

Remember that our propositions (read: our truth values) are exactly our open subsets of $\mathbb{R}$. So $p$ "is" an open subset of $\mathbb{R}$. It's not hard to see that "$p$ is true on $U$" means that $U \subseteq p$ as open sets. From here, it's easy to compute an explicit description of the subsheaf $X \subseteq \underline{\mathbb{N}}$:

$$ X(V) = \begin{cases} \{ 0 \} & V \subseteq p \\ \emptyset & V \not \subseteq p \end{cases} $$

Of course, this looks very similar to the subsheaf we constructed in the previous part of this answer, and that's no accident!

---

As a nice exercise, you can play this game with any topological space (not just $\mathbb{R}$) and the bulleted "facts to take on faith" stay true. Can you show that, on a discrete space, every inhabited subsheaf of $\underline{\mathbb{N}}$ does have a least element? Can you (separately) show that LEM is true too? It's worth thinking deeply about the differences between that example and the one worked out in this answer.

---

I hope this helps ^_^

Answer 2

1. There's no restriction in the axiom schema of separation that says we can't have something like this in the predicate... hard to say how we'd even do that. What can (and does) happen, is that we restrict the syntactic forms of predicates allowed in separation (e.g. only bounded quantifiers) and then we wouldn't be allowed anything for $p$, but we'll generally still get instances of LEM here that we aren't entitled to.
2. To slightly modify your question: "There's no secret third truth value a proposition could have, or is there?" When you reason "if $p$ holds then $S_p = \{0,1\},$ or else $S_p = \{1\},$ in either case, it has a least element," you're doing a case analysis based on excluded middle... exactly what is prohibited.
3. It only looks like things if and when we know whether $p$ is true or not... then we know what it looks like. Compare to some Brouwerian counterexample in constructive analysis and asking "what does this real number look like?", (e.g, 'is it zero?').