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)



Relationship between provable in $RCA_0$ and effectively true
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](https://arxiv.org/pdf/2003.13331.pdf), correcting [Kuyper](https://arxiv.org/abs/1511.05189)).


