Question about avoiding Law of Excluded Middle

Question

I have little background in logic, so my apologies in advance if the following question is uninformed.

I was reading this blog post by Andrej Bauer, and the first Proposition claims

If every inhabited subset of NN has an infimum then the Law of Excluded middle holds.

Here I assume we are in some ambient elementary topos with NN its natural numbers object.

In the proof of the above, given a formula $\phi$ (in 0 variables) he constructs a particular subset of NN which is inhabited by 1; then by hypothesis he lets $m$ be its infimum, and he asserts $m\leq 1$.

After this we assume either $m=0$ or $m=1$; but doesn't this require using the Law of Excluded Middle? Which technique is being used to come to this conclusion at this step in the proof?

Answer 1

Every natural $m \leq 1$ is either $0$ or $1$ by induction. For instance:

• $m = 0 \leq 1$ is $0$
• if $m = \mathsf{suc}\ n \leq 1$, then also $n \leq 1$, so the inductive hypothesis yields that $n$ is either $0$ or $1$. But actually it can only be $0$, because $\mathsf{suc}\ 1 = 2 \nleq 1$. So $m = \mathsf{suc}\ 0 = 1$.