Relationship between provable in $RCA_0$ and effectively true

Question

Question: What is the relationship between provability in $RCA_0$ and effectively true?

In other words: Given a problem, if a statement asserting the existence of a solution of the problem is provable in $RCA_0$, does it follow that given a computable instance of the problem we can compute a solution to the problem?

Motivation: I'm getting into Reverse Mathematics and Hirchfeldt gives an exercise in his book Slicing the Truth to prove that $RCA_0$ proves the Ramsey theory for singletons $RT^1_k$ for each $k \geq 2$. This together with $REC$ being the intended model for $RCA_0$ implies to me that the homogenous set should be computable.

However, $RT^1_k$ seems to be effectively true only in the trivial case of $k=1$. My thinking so far got me the following observations:

1. If the colour in the infinite pigeonhole principle is effectively true, then so is $RT^1_k$, but this doesn't seem to help, since the two are equivalent.
2. Trying to define the property that the homogenous set is infinite leaves me with the solution being $\emptyset''$-computable.

To my limited knowledge the most probable solution to this, unless I'm missing some trick that would make $RT^1_k$ effectively true, is that while homogenous sets are computable, we cannot effectively decide which homogenous set is infinite, hence cannot effectively compute the solution to the instance.

My naive leap from this is that provable in $RCA_0$ implies effectively true only with finite and trivial instances. But this seems quite a long stretch and the use of trivial is rather vague(to incorporate the $RT^1_k$ case, something along the lines of Rice's theorem) hence the question.

(Apologies if this is not a research-level question, my competence to evaluate these is lacking)

Answer 1

Provability in $\mathsf{RCA_0}$ (or even truth in all $\omega$-models of $\mathsf{RCA_0}$) guarantees a version of computable truth of a $\Pi^1_2$ sentence, namely that for every instance of the corresponding problem $X$ there is a solution $Y$ which is computable from $X$ (note that this applies even when $X$ is non-computable). However, this does not mean that we can find such a $Y$ given $X$ in any nice way.

For example, let $\varphi(x)$ be any arithmetic formula at all and consider the $\Pi^1_2$ sentence "For all $X$ there is some $Y$ such that the first bit of $Y$ codes whether $\varphi$ holds of the first bit of $X$." This is trivially provable in $\mathsf{RCA_0}$, but of course we can't have a simple process for finding $Y$ given $X$ in general since that would compute $\{x:\varphi(x)\}$.

Note, however, that the above toy counterexample crucially uses classical logic. One natural question at this point is whether provability in some constructive version of $\mathsf{RCA_0}$ might be connected with genuine computable truth. It turns out that there are indeed connections here, but they are rather subtle (see Uftring, correcting Kuyper).

Answer 2

Three (related) approaches that have not been mentioned are as follows:

1. the meta-theorems from proof-mining (see U. Kohlenbach's "Applied Proof Theory") provide the kind of results you are looking for in a (much more) general setting. These meta-theorems are restricted to specific classes of formulas, but there exist counter-examples to most purported generalisations. In other words, one cannot do better in general, esp. when classical logic is used.

2. Makoto Fujiwara has obtained a number of results connecting "provability in constructive math" and "provability in classical mathematics with witnesses". This is a list of some of his papers. The results are perhaps more concrete than proof mining, so not as general, but a better starting point for the novice.

3. In the case of Ramsey's theorem, there is even a constructive version based on the notion of 'almost full' (Veldman and Bezem). This formulation is quite elegant and even has applications in CS, as shown here. Formulated with almost-fullness, there is a computable interpretation 'by default'.

Answer 3

While provabilty of $\forall x \in X \ \exists y \in Y \ \phi(x,y)$ in $\mathrm{RCA}_0$ is often related to being able to compute the witnesses $y$ from the instances $x$, there is no general implication in either way. A proof in $\mathrm{RCA}_0$ can make use of non-uniform case distinctions (as you have observed). Conversely, we may have a computable algorithm to find the $y$'s from the $x$'s, but to prove correctness of the algorithm we may need more than $\mathrm{RCA}_0$.

What a proof in $\mathrm{RCA}_0$ tells you is that for any computable instance there is a computable solution - so it's just uniformity which is an issue here.

Slicing the Truth may very well get to that (I have to admit not having read it yet), but if you want a detailed picture of how difficult obtaining the solutions from the instances is in an algorithmic sense, the go-to formalism is Weihrauch reducibility. For the full answer to your question, you'll probably want to understand to what extent the Weihrauch degree picture of theorems agrees with the reverse math picture - and that is definitely research-level (and an area of active work at the moment).

The most up-to-date survey on Weihrauch reducibility is found here: https://arxiv.org/abs/1707.03202