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