## Formalized Name Church's Thesis Is Not Derivable in Ordinary Intuitionistic Arithmetic ## Formalized Statement Let $\mathrm{HA}$ denote ordinary first-order Heyting arithmetic in the language of natural numbers, without adding Church's Thesis as an axiom schema. Fix a standard arithmetic computation predicate $T(e,n,m)$ meaning that the program with index $e$ halts on input $n$ with output $m$. For an arithmetic formula $A(n,m)$, let $\mathsf{CT}_A$ be the schema instance \begin{align*} \bigl(\forall n\,\exists m\,A(n,m)\bigr)\to \exists e\,\forall n\,\exists m\,(T(e,n,m)\land A(n,m)). \end{align*} The full Church's Thesis schema is the collection of all such instances $\mathsf{CT}_A$. Ordinary $\mathrm{HA}$ does not prove this full schema. ## Proof [proofplan] We prove non-derivability by the standard semantic argument. There are intuitionistic Kripke or sheaf models of $\mathrm{HA}$ in which the axioms and rules of $\mathrm{HA}$ are valid but some instance of the full Church's Thesis schema fails. If $\mathrm{HA}$ proved the full schema, soundness would make every instance true in every such model. The countermodel therefore rules out derivability in ordinary $\mathrm{HA}$. [/proofplan] [step:Use the standard countermodel theorem] We use the following standard metatheorem about intuitionistic arithmetic. There is an intuitionistic model $\mathcal{M}$ of $\mathrm{HA}$ and an arithmetic formula $A(n,m)$ with the following property. Write $\mathcal{M}\Vdash B$ to mean that the sentence $B$ is forced, or valid, in the model $\mathcal{M}$; write $\mathcal{M}\nVdash B$ to mean that $B$ is not forced in $\mathcal{M}$. Then \begin{align*} \mathcal{M}\Vdash \forall n\,\exists m\,A(n,m), \end{align*} but \begin{align*} \mathcal{M}\nVdash \exists e\,\forall n\,\exists m\,(T(e,n,m)\land A(n,m)). \end{align*} Equivalently, $\mathcal{M}$ is a model of ordinary $\mathrm{HA}$ in which the instance $\mathsf{CT}_A$ fails. One may obtain such a model by a Kripke or sheaf construction whose nodes reveal finite information about a total number-theoretic function chosen to evade every recursive index. Each finite stage is compatible with the axioms of $\mathrm{HA}$, so $\mathrm{HA}$ remains valid in the model. Internally, the relation $A(n,m)$ is total because each input eventually receives a value. However, no single recursive index is forced to compute all witnesses, since the construction can extend past any proposed index at a later stage. [guided] The countermodel theorem supplies the exact semantic obstruction. It gives a model $\mathcal{M}$ satisfying ordinary $\mathrm{HA}$ and one formula $A(n,m)$ for which the antecedent $\forall n\,\exists m\,A(n,m)$ is forced, while the consequent asserting a single recursive index $e$ for all witnesses is not forced. Thus the particular implication $\mathsf{CT}_A$ is false in $\mathcal{M}$. The construction does not contradict realizability results for Church's Thesis. Realizability is one special computational semantics. Derivability in $\mathrm{HA}$ is stronger: a theorem of $\mathrm{HA}$ must be valid in every intuitionistic model of $\mathrm{HA}$. The countermodel theorem identifies one such model where the schema fails. [/guided] [/step] [step:Apply soundness for Heyting arithmetic] Soundness says that if $\mathrm{HA}\vdash B$ for an arithmetic sentence or schema instance $B$, then every intuitionistic model of $\mathrm{HA}$ forces $B$. Applying this to the instance $\mathsf{CT}_A$ from the previous step, if $\mathrm{HA}$ proved $\mathsf{CT}_A$, then \begin{align*} \mathcal{M}\Vdash \mathsf{CT}_A. \end{align*} But the previous step gives \begin{align*} \mathcal{M}\nVdash \mathsf{CT}_A. \end{align*} This contradiction shows that $\mathrm{HA}$ does not prove that instance $\mathsf{CT}_A$. [/step] [step:Conclude non-derivability of the full schema] The full Church's Thesis schema contains every instance $\mathsf{CT}_A$. Since one particular instance is not provable in ordinary $\mathrm{HA}$, ordinary $\mathrm{HA}$ cannot prove the full schema. Equivalently, the full schema may be added to some constructive systems as an extra principle, but it is not a theorem of bare Heyting arithmetic. [guided] To prove that a whole schema is not derivable, it is enough to find one non-derivable instance. The countermodel gives a formula $A(n,m)$ such that the corresponding instance \begin{align*} \mathsf{CT}_A=\bigl(\forall n\,\exists m\,A(n,m)\bigr)\to \exists e\,\forall n\,\exists m\,(T(e,n,m)\land A(n,m)) \end{align*} fails in a model $\mathcal{M}$ of $\mathrm{HA}$. If ordinary $\mathrm{HA}$ proved the full schema, then in particular \begin{align*} \mathrm{HA}\vdash \mathsf{CT}_A. \end{align*} By soundness for intuitionistic models of $\mathrm{HA}$, this would imply \begin{align*} \mathcal{M}\Vdash \mathsf{CT}_A. \end{align*} But the countermodel was chosen so that $\mathcal{M}\nVdash\mathsf{CT}_A$. This contradiction proves that the full Church's Thesis schema is not derivable in ordinary $\mathrm{HA}$. [/guided] [/step]