law of excluded middle from subsets of finite sets being finite in “five stages of accepting constructive mathematics”

Question

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

Answer 1

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.

Answer 2

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$.