i’m reading andrej bauer’s five stages of accepting constructive mathematics (after watching his excellent talk of the same name).

here i stumbled upon a curiosity. on page 6 of the document, he proves that the law of excluded middle follows from the assumption that subsets of finite sets are again finite. let me quote his proof:

To prove the converse, assume that a subset of a finite set is always finite, and consider any proposition $P$. The set $A = \{0\}$ is finite, and $B = \{x ∈ A \mid P\}$ is a subset of it, and therefore finite. Let $b_0,...,b_m$ be an enumeration of $B$. Either $m = 0$ or $m ≠ 0$. In the first case $B = ∅$ and hence $¬P$, while in the second case $0 ∈ B$, therefore $P$. We have decided $P$.

… wait, what?

[…] Either $m = 0$ or $m ≠ 0$. […]

isn’t the entire point here to not use excluded middle? how is this instance of it justified? what is the remedy here and what notion of finite is being used here anyway? as i see it, given an explicit bijection $B → [m]$ for some set $[m] = \{1, …, m\}$, we have $$¬P \iff m = 0 \quad\text{and}\quad P \iff m ≠ 0.$$ in my mind, we have yet to constructively prove that each finite cardinality is either zero or nonzero or that a finite set that isn’t nonempty must be empty or something.

(as a minor remark, i’m pretty sure, he meant to start his enumeration with $b_1$, not $b_0$, as else $m = 0$ doesn’t imply $B = ∅$. oh, and sorry for the lengthy title. i try to be descriptive, maybe excessively so.)

  • 6
    $\begingroup$ Dropping LEM as a general rule doesn't mean dropping it in all situations - equality of natural numbers is (generally) taken to be constructively decidable, and so subject to LEM. $\endgroup$ Jun 6, 2022 at 17:52
  • $\begingroup$ @NoahSchweber is this taken as an axiom or is there a proof of it from first principles? $\endgroup$
    – windfish
    Jun 6, 2022 at 17:54
  • 5
    $\begingroup$ there is a proof that equality is decidable on $\mathbb{N}$. Try inducting on $n$ to see why. If you get stuck, reach out and I can help with the proof! $\endgroup$ Jun 6, 2022 at 18:00

2 Answers 2


I think whats going on is this: rejecting LEM does not require rejecting every proposition of the form $P \lor \neg P$. Rather, rejecting LEM just means we cannot assume $P \lor \neg P$ for arbitrary $P$.

So, what makes certain instances of $P\lor\neg P$ valid? Namely if we have a proof of $P$ or if we have a proof of $\neg P$. For certain nice structures, such as the natural numbers, this is possible without using LEM and so we call equality on this structure "decidable". This means that, for example, given any $n\in\mathbb{N}$, we can decide (i.e., prove) whether or not $n$ is $0$. So, we can prove that, for all $n\in\mathbb{N}$, $n=0\lor n\not= 0$. This can be shown without too much trouble via induction, without using LEM. Basically, case on $n$ and in each case you can show either $n$ is $0$ or is not $0$. This is a fun exercise to try out.

I have not read that paper in a little while so I forget if the $0$ in question is a natural number or a boolean. But, equality is decidable on the booleans as well. I think the notion of finiteness in question is having an injective map into $\mathbb{N}$ or something like this. I expect the author mentions which notion they are using.

  • $\begingroup$ i get it, from $1 > 0$ we can prove by induction that $n = 0 ∨ n > 0$ for $n ∈ ℕ_0$, which implies $n = 0 ∨ n ≠ 0$. $\endgroup$
    – windfish
    Jun 6, 2022 at 18:12

One of my favorite examples of proofs by induction (in arithmetic) is the proof from the Peano axioms that every natural number $n$ satisfies $$ n=0\ \lor\ \exists k\,(n=S(k)), $$ where $S$ denotes "successor". The basis of the induction (i.e., the case $n=0$) is trivial, and the induction step is also trivial: If $n$ satisfies the claim then so does $S(n)$, since we can take $n$ as the value of $k$.

(What I like about this proof is that, although it makes essential use of the induction principle, the induction step never uses the induction hypothesis.)

Once you have this result, you can combine it with the Peano axiom that $S(x)\neq0$ to conclude that every natural number $n$ satisfies $$ n=0\ \lor\ n\neq0. $$ So this particular case of the law of the excluded middle is constructively provable from the axioms for the natural numbers.

EDIT: As pointed out in the comments, the following is wrong; if there is a $b_0$ then it equals $0$.

There is, however, a typo in the material you quoted. $0\in B$ should be $b_0\in B$.

  • $\begingroup$ i quoted bauer correctly, he himself writes "$0 ∈ B$”. i think $0 ∈ B$ is fine, since $B$ is a subset of $A$, so elements of $B$ are as well elements of $A$, of which $0$ is the only one. thus, if $B$ is inhabited by an element $x$, we can say $x = 0$. $\endgroup$
    – windfish
    Jun 7, 2022 at 4:48
  • $\begingroup$ @windfish You're right. If there is a $b_0$, it has to be $0$. $\endgroup$ Jun 7, 2022 at 13:18

You must log in to answer this question.

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