Constructible problems for which the solution is non-constructible?

For the sake of this question, I am using the word "constructible" in the sense of constructive mathematics: e.g. a real number is constructible if you can construct a Cauchy sequence for it in ZF (without choice), and also prove that it is Cauchy in ZF. Then a real-valued problem is constructively solvable if a Cauchy sequence for the solution exists in ZF, it can be proven constructively to be Cauchy, and it can be proven constructively to solve the problem. (Although I am also interested in the case where one or both of these requirements fail, if anybody has any examples.) Of course, I'm only interested in the sorts of problems for which such a solution does exist and is provable classically.

I've noticed that for every specific problem (constraint set?) I have seen defined constructively it always seems to be the case that all of the solution(s) are also constructible. Consider: finding the roots of a specific constructed polynomial, or finding the solution to a specific constructed ODE.

You can't necessarily find an algorithm that works over a whole class of problems (say, the general intermediate-value theorem) but given the construction of a specific continuous function $f$, and a constructed $y$-value, I've never seen anybody fail to construct a specific $x$-value which satisfies the IVT $f(x)=y$ at that point, given that $y$ does actually lie between two other points as per the assumption of the IVT.

When I say the words "constructible problem" or "constructible constraint set", I suppose one requirement I have to add is that if the constraints are of a functional or Pi-type "for all x, ..." then the type/set over which they are indexed should also consist only of constructible things (e.g. natural numbers, and not the reals as a whole).

Am I not imaginative enough, or does every constructively-definable set of constraints yield a constructible solution?

Are there any examples of a constructively-defined set of constraints provably not yielding a constructive solution, or at the very least which we reliably fail to prove constructively? Are there any results about this? (I kind of suspect this whole question is maybe a model theory thing?)

For the sake of this question, I'm primarily just interested in problems with real/complex-valued solutions (or in the case of differential equations, entire functions), but would be interested to hear about anything tangentially related. Bonus points for delineating between solutions which can merely be defined constructively and solutions which can be proven to be the solution constructively.

I don't know an awful lot about PDEs, for example, but I know that some people apparently spend their entire careers studying numerical approximations of them, so as a more concrete example of something in the ballpark of what I'm looking for:

Can you provide an example of a specific, constructed mathematical object, (say, a PDE or something) with a solution which we provably can't algorithmically approximate to arbitrary precision? Or at least which we fail to construct a Cauchy approximation for (or can construct, but fail to prove that it is Cauchy)?

Solution 1:

First observe that there are constructive real numbers $a$ such that we (working in ZF) do not (currently) know whether $a$ is zero or positive. For example, let $a$ be given by the Cauchy sequence whose $n$-th term is $2^{-k}$ if $k\leq n$ is the first counterexample to Goldbach's conjecture and $2^{-n}$ otherwise. Let $b$ be another such number, derived from some other search problem that has (as far as we know) nothing to do with Goldbach's conjecture, for example, searching for the first Gödel number of a ZFC proof that there are no supercompact cardinals.

Now define (constructively) a function $f$ on the interval $[0,3]$ by first setting $f(0)=-1$, $f(1)=-a$, $f(2)=b$, and $f(3)=1$ and then interpolating linearly between these values. The intermediate value theorem assures us that there is an $x$ with $f(x)=0$. But we can't constructively produce such an $x$ and prove (even in classical ZF) that it works, because of our ignorance about Goldbach's conjecture and the consistency of supercompact cardinals. For all we currently know, the required $x$ might be 1 or 2 or any of lots of reals between those, so we can't produce any good approximations to $x$.

Solution 2:

O. Aberth provides an example of an initial value problem given by a uniformly continuous function of two variables that does not have a computable solution:

O. Aberth.The failure in computable analysis of a classical existence theorem for differential equations. Proc. Amer. Math. Soc. 30 (1971), 151-156

We may conclude that we cannot constructively prove the existence of a solution, as we could extract the algorithmic content from a constructive proof, yielding a computable solution. Classically, the 'existence' of a solution is guaranteed by Peano's theorem.