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

  • $\begingroup$ ... what's HA ? $\endgroup$ – mercio Sep 3 '13 at 8:40
  • $\begingroup$ Heyting arithmetic $\endgroup$ – Andrea Condoluci Sep 3 '13 at 8:42
  • 1
    $\begingroup$ What makes you think that not all HA-decidable quantifier-free formulas of HA are recursive? $\endgroup$ – Carl Mummert Sep 3 '13 at 12:23

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.

  • $\begingroup$ Okay so in HA recursive and decidable predicates coincide? About the stronger result: to say that $f$ is computable requires the Church thesis, doesn't it? $\endgroup$ – Andrea Condoluci Sep 3 '13 at 14:41
  • $\begingroup$ Nothing here requires (the constructive form of) Church's thesis. That would only be relevant if we were trying to formalize results such as this within HA, but the claim that "every formula $A(x)$ that is decidable in HA defines a computable set" is not phrased as a result within HA, it is a result about HA that we can prove like any other mathematical result. Church's thesis is not relevant to the quoted result. $\endgroup$ – Carl Mummert Sep 3 '13 at 14:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.