Currently I am reading Simpson's Subsystem of Second Order Arithmetic.
The author defined continuous function as follows:
Within $RCA_0,$ let $\hat{A}$ and $\hat{B}$ be complete separable metric spaces. A (code for a ) continuous partial function $\phi$ from $\hat{A}$ to $\hat{B}$ is a set of quintuple $\Phi\subseteq \mathbb{N}\times A\times \mathbb{Q}^+ \times B\times \mathbb{Q}^+ $ which is required to have certain properties. We write $(a,r)\Phi (b,s)$ as an abbreviation for $\exists n ((n,a,r,b,s)\in \Phi).$ The properties which we require are:
if $(a,r)\Phi (b,s)$ and $(a,r)\Phi (b',s'),$ then $d(b,b')\leq s+s';$
if $(a,r)\Phi (b,s)$ and $(a',r') < (a,r),$ then $(a',r')\Phi(b,s);$
if $(a,r)\Phi (b,s)$ and $(b,s) < (b',s'),$ then $(a',r')\Phi(b',s');$
where the notation $(a',r')<(a,r)$ means that $d(a,a')+r'<r.$
Then the authors stated the following in the next paragraph.
If $x\in dom(\phi),$ we define the value $\phi(x)$ to be the unique point $y\in \hat{B}$ such that $d(y,b)\leq s$ for all $(a,r)\Phi(b,s)$ with $d(x,)<r.$
The author continue with the following statement.
If $x\in dom(\phi),$ we can use the code $\Phi$ and minimization theorem to prove within $RCA_0$ that $\phi(x)$ exists.
I have trouble proving $\phi(x)$ exists. Any hint is appreciated.
The key point is the definition of "$x \in \text{dom}(\Phi)$."
You want to view $(a,r)\Phi(b,s)$ as saying that if $x \in (a-r, a+r)$ then $\phi(x) \in [b-s, b+s]$. By definition (not in the question), $x \in \text{dom}(\Phi)$ if for every $\epsilon > 0$ we have $(a,r)\Phi(b,s)$ for some $a, b \in \mathbb{Q}$, some $s \leq \epsilon$ and so that $d(a,x) < r$.
If we apply this with $\epsilon = 2^{-k}$ we can get a rational $b_k$ so that $d(b_k, \phi(x)) \leq 2^{-k}$. We can choose $b_k$ by searching for an $m$ so that $(m, a, r, b, s)$ is in $\Phi$ and verifies the last sentence of the previous paragraph - this is a computable search, and this process is what Simpson means by "using minimization".
The resulting sequence $(b_k)$ is $\Delta^0_1$ in $x$ and $\phi$, and $(b_k)$ will be a quickly converging Cauchy sequence that converges to $\phi(x)$.