Well-Ordering Principle From Recursion Theorem

Question

As far as I understand, in intuitionistic logic we have neither (i) the well-ordering principle nor (ii) the recursion theorem. But can one deduce one from the other? I believe we cannot deduce (ii) from (i), but assume (ii) holds and $P:\mathbf{N}\to\Omega$ is a subset of $\mathbf{N}$. If $P(0)$ then $0$ is the smallest element in $P$ and we are done. Else we can define $f:\mathbf{N}\to\mathbf{N}$ via $f(0)=0$ and $$f(n+1)=\begin{cases}f(n)>0&f(n)\\P(n+1)&n+1\\0&\text{else}\end{cases}$$ If $P$ is non-empty, we get $p\in P$ (by constructive definition of non-empty) and can define the smallest element of $P$ as $f(p)$. Would this work out?

My second question would be, what do intuitionists think about the recursion theorem? To me it feels a bit more constructive than proofs by contradiction, although you prove it by contradiction (as far as I remember) in classical set theory.

Answer 1

If $P : \mathbf{N} \to \mathbf{2}$ is a decidable subset of $\mathbf{N}$, and you are given $m : \mathbf{N}$ such that $P(m) = 1$, then yes, you can use $P$ to calculate a lowest value of $n : \mathbf{N}$ such that $P(n) = 1$. On the other hand, the well-ordering principle for arbitrary subsets of $\mathbf{N}$ would in fact imply excluded middle. To see this, suppose $p : \Omega$ is a proposition, and define the subset $$P := \{ n : \mathbf{N} \mid n=1 \lor (n=0 \land p) \}.$$ Then $1 \in P$, so $P$ is nonempty and the minimum element of $P$ must be either 0 or 1. However, if the minimum element is 0, then we conclude $p$, while if the minimum element is 1, then we conclude $\lnot p$. (This does make use of the fact that $\{ n : \mathbf{N} \mid n \le 1 \} = \{ 0, 1 \}$, which is straightforward to prove assuming the validity of definitions by recursion.)

For your second question: yes, defining functions on $\mathbf{N}$ by recursion is widely considered to be intuitionistically valid. For instance, the definition of a natural numbers object in a topos essentially says exactly that this is valid. Also, related to the computability interpretation of intuitionism, computer programmers define functions by recursion all the time.

Answer 2

The recursion theorem is perfectly constructively valid. In fact, in some versions of constructive mathematics, the recursion theorem is actually an axiom.

The well-ordering principle, as it’s classically stated, is equivalent to the law of excluded middle. For consider a proposition $Q$. Define $S = \{x \in \{0, 1\} \mid x = 1 \lor Q\}$. Then $S$ has a least element if and only if $Q \lor \neg Q$. For if $S$’s least element is $0$, then $Q$. And if $S$’s least element is 1, then $\neg Q$.

Your proof doesn’t work because you assume either $P(0)$ or $\neg P(0)$.