Let $C$ be a decidable predicate in the language of arithmetic HA, that is $$ \vdash (\forall \underline x)\: C(x) \vee \neg C(x).$$
$C$ is recursive if there exists a computable characteristic function, a $\chi_C$ such that
$$ \chi_C(\underline x):=\begin{cases} 1 & \mbox{ if $C(x)$ holds,}\\ 0 & \mbox{otherwise.}\end{cases}$$
I can't understand why not all decidable (quantifier free) propositions of HA are recursive. (They are of course if we accept Church thesis...)
Could someone give me some example (if there exists?) or some explanation?
Thank you
If $HA \vdash (\forall n) [ A(n) \lor \lnot A(n)]$ then, in particular, for each natural number $m$ we have that $$ HA \vdash A(\ulcorner m\urcorner) \lor \lnot A(\ulcorner m \urcorner)$$ Here $\ulcorner m\urcorner$ is the closed term $S(S(S(S(\cdots S(0)\cdots)$ with $m$ occurrences of $S$.
HA has the disjunction property: if $\phi,\psi$ are sentences and $HA \vdash \phi \lor \psi$ then $HA \vdash \phi$ or $HA \vdash \psi$. Thus, if $HA \vdash (\forall n) [ A(n) \lor \lnot A(n)]$ then, for each $m$, $$ HA \vdash A(\ulcorner m\urcorner) $$ or $$ HA \vdash \lnot A(\ulcorner m\urcorner) $$ The axioms of HA are all true statements about natural numbers, so HA only proves one of those two formulas, and the one it proves is true about the natural numbers.
Because HA is an effective theory, given $m$ we can enumerate derivations in HA until we find a derivation of $A(\ulcorner m\urcorner)$ or a derivation of $\lnot A(\ulcorner m\urcorner)$, and that will tell us whether $A(\ulcorner m\urcorner)$ holds. Therefore, the set $\{m : A(m) \}$ must be recursive.
There is no need in this proof to assume $A$ is quantifier free. The formula $A$ can be an arbitrarily complicated formula in the language of HA. The only assumption is that $HA \vdash (\forall n)[A(n)\lor \lnot A(n)]$.
In fact, a stronger result is known. If $B(n,m)$ has two free variables, and $HA \vdash (\forall n)(\exists m) B(n,m)$ then there is a computable function $f$ such that $B(n,f(n))$ holds for each natural number $n$. As above, $B$ can be an arbitrarily complicated formula. This stronger result requires more than just the basic techniques above, and it is usually proved with the method of realizability.