Gödel's incompleteness theorem already holds for $Q$ (Robinson's Arithmetic), by design. Is $Q$ already strong enough to support (entail) Kleene's recursion theorem, or are there some limits to recursion at this level?
$\begingroup$
$\endgroup$
12
asked Apr 22, 2017 at 23:21
-
2$\begingroup$ What do you mean by "support Kleene's recursion theorem"? Are you asking whether the recursion theorem is provable in Q? $\endgroup$– Noah SchweberCommented Apr 23, 2017 at 3:05
-
2$\begingroup$ For this question to have a definite answer, you'd need to specify the exact formalization of the recursion theorem that you have in mind. Formalizations that are trivially equivalent might not be provably equivalent in Q, because Q is so weak. For example, although Q (the version I'm accustomed to) proves $(\forall x)(x+0=x)$, it doesn't prove $(\forall x)(0+x=x)$, so if you had asked "Does Q prove that 0 is an additive identity?" the answer would depend on whether you meant left, right, or 2-sided identity. With a statement as complex as the recursion theorem, [continued in next comment] $\endgroup$– Andreas BlassCommented Apr 23, 2017 at 5:02
-
2$\begingroup$ [continuation of previous comment] the issue becomes much bigger. I'd expect that, if you were to formalize the recursion theorem explicitly, it would most probably not be provable in Q, unless you designed your formalization very cleverly in order to make it provable. $\endgroup$– Andreas BlassCommented Apr 23, 2017 at 5:04
-
1$\begingroup$ A more direct proof of Gödel's incompleteness theorem uses Gödel's diagonal lemma instead of Kleene's recursion theorem. The former does hold for Q. $\endgroup$– Emil JeřábekCommented Apr 23, 2017 at 8:19
-
1$\begingroup$ Also, you mention Nelson’s finitism. Well, for Nelson, $Q$ is the starting point, but he would not actually expect interesting things to be directly provable in $Q$ (hardly anything is). What he did was to construct a theory, IIRC denoted $Q^*$, which is interpretable in $Q$ on a cut, and prove stuff in $Q^*$. The theory includes e.g. $I\Delta_0+\Omega_1$. The recursion theorem is provable in such a theory, under a reasonable enumeration of algorithms. $\endgroup$– Emil JeřábekCommented Apr 23, 2017 at 10:47
|
Show 7 more comments