## Formalized Name
Church's Thesis Schema Is Kleene-Realizable
## Formalized Statement
Work with standard Kleene realizability for first-order arithmetic, using a fixed pairing function, projections, the partial computable functions $\varphi_e$, and an arithmetized computation predicate $T(e,n,c)$ whose output is decoded by $U(c)$. For every arithmetic formula $A(n,m)$, the following Church's Thesis schema is realized:
\begin{align*}
\bigl(\forall n\,\exists m\,A(n,m)\bigr)\to
\exists e\,\forall n\,\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr).
\end{align*}
## Proof
[proofplan]
Unfold the Kleene realizability clauses for implication, universal quantification, and existential quantification. A realizer for the premise computes, uniformly in the input, a pair containing a witness and a realizer for the instance of the formula. Use the s-m-n theorem to build an index for the computable function that extracts those witnesses.
[/proofplan]
[step:Unpack a realizer for the premise]
Let $r$ realize $\forall n\,\exists m\,A(n,m)$. By the realizability clause for universal quantification, for each natural number $n$ the computation $\varphi_r(n)$ is defined and realizes $\exists m\,A(n,m)$. By the realizability clause for existential quantification, the value $\varphi_r(n)$ decodes as a pair
\begin{align*}
\langle m_n,a_n\rangle,
\end{align*}
where $a_n$ realizes $A(n,m_n)$.
[/step]
[step:Build a uniform computable index]
By the s-m-n theorem, from $r$ one effectively obtains an index $e$ for the partial computable function
\begin{align*}
n\mapsto m_n,
\end{align*}
computed by running $\varphi_r(n)$ and returning the first projection of the resulting pair. More explicitly, whenever $\varphi_r(n)=\langle m_n,a_n\rangle$, the computation of $\varphi_e(n)$ halts with output $m_n$. Let $c_n$ be a code for this halting computation, so $T(e,n,c_n)$ holds and $U(c_n)=m_n$.
[/step]
[step:Realize each instance of the universal conclusion]
Fix $n$. The previous step gives $c_n$ with $T(e,n,c_n)$ and $U(c_n)=m_n$, and the first step gives a realizer $a_n$ for $A(n,m_n)$. Since $m_n=U(c_n)$, the same realizer $a_n$ realizes $A(n,U(c_n))$. Combining the canonical realizer for the true computation fact $T(e,n,c_n)$ with $a_n$ gives a realizer for
\begin{align*}
T(e,n,c_n)\land A(n,U(c_n)).
\end{align*}
Pairing $c_n$ with that conjunction realizer realizes
\begin{align*}
\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr).
\end{align*}
Because this construction is uniform in $n$, it realizes the universal formula over $n$.
[/step]
[step:Realize the outer existential and implication]
The existential realizer for the conclusion is the pair consisting of the index $e$ and the realizer for the universal statement constructed above. Thus, from any realizer $r$ of the premise, there is an effective procedure producing a realizer of the conclusion. This procedure is exactly a realizer of the implication in the Church's Thesis schema.
[/step]
[step:Summarize the computation extraction]
The proof converts a realizer for a total existential statement into an index for the function that extracts its witnesses. The remaining realizability clauses package the computation trace and the original instance realizer into the required existential conclusion.
[guided]
The proof converts a realizer for a total existential statement into an index for the function that extracts its witnesses. The remaining realizability clauses package the computation trace and the original instance realizer into the required existential conclusion.
[/guided]
[/step]
