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)?


2 Answers 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?').
  • $\begingroup$ I'm aware (per Glivenko) that there's no third truth value in intuitionistic logic, and that $p$ may not be assigned a truth value yet. Still, in this proof, $0 \in S_p$ specifically if $p$ has been assigned the value 'true'. Seemingly, therefore, we still recover a weaker version of L.E.M., since $p$ either has, or has not been, assigned that truth value. I.e. $\min(S_p) = 0$ means $p$ is 'true'; $\min(S_p) = 1$ means either $p$ is 'false', or $p$ has an undefined truth value. $\endgroup$ Dec 3, 2023 at 3:09
  • $\begingroup$ Also, we know for sure (by definition) $S_p$ contains $1$, and the only other number that might conceivably be a member of $S_p$ is $0$ (also by definition). Just not sure if I'm supposed to think of $0$ as being a "fuzzy" member of $S_p$, or if it's in some Schrodinger-state of both 'in' and 'not in' for a $p$ which has no assigned truth value, or how to build intuition around this case. $\endgroup$ Dec 3, 2023 at 3:11
  • 3
    $\begingroup$ @RiversMcForge My point in turning the quote around wasn't anything to do with multivalued logic, just to highlight that you are using excluded middle when you reason 'it has to be one thing or the other so...'. Yes, we know for sure it contains $1$ and know it can't contain anything else but $0$. But to affirm 'there is a least element' in a constructive setting, we need to actually produce the least element, which we can't here unless we can affirm or refute $p$ (again, this is very similar to thinking about Brouwerian counterexamples in non-set-theory contexts). $\endgroup$ Dec 3, 2023 at 4:48
  • 2
    $\begingroup$ @RiversMcForge As to how to think of it, I don't think that $0$ being a 'fuzzy member' is far off. Per HallaSurvivor's answer you can think of what it looks like in models, where it will be 'a member in some worlds but not others'. $\endgroup$ Dec 3, 2023 at 4:52

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 ^_^

  • $\begingroup$ This is very helpful, I was not familiar with this model at all, but it clarifies things immensely. It does have something of a "rabbit-out-of-a-hat" quality to me--can you explain the motivation behind constructing this particular model, or point me to a source which does so? $\endgroup$ Dec 3, 2023 at 4:33
  • 1
    $\begingroup$ There's nothing particularly special about this model. The same idea would work for almost any sheaf topos, but I chose to work with sheaves on $\mathbb{R}$ because it's a very familiar space. If you're asking for motivation behind sheaf topoi more generally, that's a very deep question. They were originally developed in order to solve the Weil Conjectures in algebraic geometry, and later were shown to have deep and interesting ties to (higher order) intuitionistic logic. $\endgroup$ Dec 3, 2023 at 4:39
  • 1
    $\begingroup$ In fact, there's a soundness/completeness theorem saying that intuitionistic provability is the same thing as truth in all topoi, and this connection is incredibly well studied. Hopefully this makes the example feel less like a rabbit out of a hat, and more like an inevitable result of general theory (which happens to be new to you). One famous (introductory-ish) reference on topos theory is Mac Lane and Moerdijk's Sheaves in Geometry and Logic. Since you're reading Bell's book on IZF, you'll likely be excited to hear he also has a book on topoi: Toposes and Local Set Theories. $\endgroup$ Dec 3, 2023 at 4:44
  • 1
    $\begingroup$ As a quick remark, though, you should know two things going in. First, Bell's book is clearly written for set theorists, and the way he presents things comes off as slightly strange compared to how a lot of working topos theorists think about things. That's fine, just know that if you read it first and then decide to do more topos theory later you'll face some mild translation issues along the way. $\endgroup$ Dec 3, 2023 at 4:48
  • 1
    $\begingroup$ Second, topos theory is a pretty formidable subject, and you shouldn't expect to learn it quickly. Getting really familiar with even the basics can take years, rather than months (it certainly took years for me). I don't say that to discourage you, but rather to encourage you. If you decide to spend the time to learn it, remember that it's hard for everyone, and it's ok to step back for a while and come back later. It's a hard subject, but is absolutely worth learning! Especially if you're interested in models of intuitionistic logic! Good luck ^_^ $\endgroup$ Dec 3, 2023 at 4:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .