Does Peano's existence theorem admits a constructive proof?

$$y(t)=y_0+\int_0^t b(y(s))ds$$ $b\in C(R^d)\cap L^\infty(R^d)$

The classical proof for Peano's existence theorem in ODE need use the Ascoli's theorem, so it's not constructive. When $d=1$, in the paper of Walter "There is an Elementary Proof of Peano's Existence Theorem" the author showed there is an constructive proof for Peano's theorem. But the method can't transformed to $d>1$. I found some literature say there is no constructive proof for this theorem.

I am not a logician and really confused about this. Can one give a rigorous meaning to "there is no constructive proof to the Peano's theorem"?

• This is similar to reverse mathematics. There one shows that theorems are equivalent to certain axioms/axiom systems. – David Roberts Jun 2 '15 at 22:42
• Peano's existence theorem is nonconstructive, as it is equivalent to weak König's lemma. Details are in §IV.8 of Simpson's Subsystems of Second Order Arithmetic. From that result we can also see that Ascoli's theorem is not required, since that is equivalent to the stronger axiom of arithmetical comprehension. – Benedict Eastaugh Jun 2 '15 at 23:00
• @BenedictEastaugh: (a) can you make that an answer instead of a comment (b) if yes, can you also briefly comment on the issue of the $d$ (why $d=1$ there is a constructive proof [according to the OP] and $d >1$ there isn't)? Thanks in advance. – Willie Wong Jun 3 '15 at 7:12
• It is not clear to me that Walter's paper is really about constructive mathematics; I think it is about something weaker, in the way that classical mathematicians sometimes use the word "constructive", which is a much broader sense of the term than is used in constructive mathematics. – Carl Mummert Jun 3 '15 at 15:41

I think that the heart of the question is "Can one give a rigorous meaning to 'there is no constructive proof to the Peano's theorem'?" The answer to this is yes, but the answer is not as simple as one might naively hope.

The way that one would give an affirmative answer is to first choose a constructive framework. The proof will not show that there is no constructive proof in any possible sense, only that there is no constructive proof within that framework. However, if the framework is sufficiently natural, then the negative answer in that framework will often be viewed as somewhat definitive.

Once a particular framework has been chosen, if one can show that the theorem implies, within the framework, some principle that is known to be unprovable in the framework, then the theorem itself is certainly unprovable by any means that can be formalized within the framework. One such principle might be the law of the excluded middle, but there are many weaker but still nonconstructive principles that are also used in practice.

There are several frameworks for constructive mathematics; an old but excellent introduction is Varieties of Constructive Mathematics by Bridges and Richman (1987).

Two particular frameworks worth mentioning are:

• Bishop's framework, which is presented in Bishop and Bridges, Constructive Analysis, 1985. Briefly put, this framework was intended to resemble ordinary informal mathematics (but with special care to avoid nonconstructive methods, and other issues of classical mathematics that Bishop felt obstructed constructive proofs).

• The "Markov-type" framework, developed by many constructivists but particularly associated with Russian constructivism. Briefly put, this framework focuses on algorithms, rather than more abstract mathematical objects. To have an object is to have an algorithm for it.

It appears that the answer in both of these frameworks is that there is no constructive proof of Peano's theorem.

• Aberth (1971) showed that Peano's theorem fails in a Markov-type setting (full text available from the journal page). Reference: Oliver Aberth, The failure in computable analysis of a classical existence theorem for differential equations, Proc. Amer. Math. Soc. 30 (1971), 151-156. MR 302982

• Bridges (2012) showed that, in a Bishop-type setting, Peano's theorem implies the principle LLPO, which is a well-known non-constructive principle used to gauge the non-constructivity of theorems. Reference: Bridges, Douglas S., Constructive solutions of ordinary differential equations. Logic, construction, computation, 67–77, Ontos Math. Log., 3, Ontos Verlag, Heusenstamm, 2012. MR 3204972

It was pointed out in the comments that, in the context of classical Reverse Mathematics, Peano's theorem is known to imply the system $\mathsf{WKL}_0$. That is a clue that the theorem may not be constructive, but there are two issues that prevent it from being definitive. First, the implication proof may require non-constructive methods. Second, the system $\mathsf{WKL}_0$ is tightly tied to Bishop's program for constructive analysis, and some theorems that are equivalent to $\mathsf{WKL}_0$ in the context of Reverse Mathematics are nonetheless considered constructive by Bishop, due to the difference between the Reverse Mathematics framework and Bishop's framework. However, the two references above are both written in constructive frameworks, and I would view them as definitive.