4
$\begingroup$

I believe that the (paraphrased) original statement of Gödels first incompleteness theorem (including Rosser's trick) is

If T is a sufficiently strong recursive axiomatization of the natural numbers (e.g. the peano axioms), $T$ is either incomplete or inconsistent.

and I'm pretty sure this is the version we proved in a course on the incompleteness theorem (which was years ago, though). Some sources (e.g. Wikipedia), however, relax that and require only a recursively enumerable axiomatization.

The effect of that relaxation is that $\textrm{Proves}(p,s)$, meaning that $p$ is the Gödel code of a proof of the statement with Gödel code $s$, is no longer deciable, but only semi-decidable. Or so I think, at least - with a recursive set of axioms, it's easy to validate whether a sequence of statements constitutes a proof, but if the axioms are only recursively enumberable, verifying that some sequence is not a proof is not generally possible.

However, it seems that this doesn't matter much, since $\textrm{Provable}(s) = \exists p \, \textrm{Proves}(p,s)$ is semi-decidable by PA in both cases, which is sufficient for the rest of the proof I guess.

My question is two-fold. First, is the reasoning above about why this relaxation is valid correct? And second, what are the consequences of this relaxation?

$\endgroup$
7
$\begingroup$
  1. Just for the record, the original version of Gödel's incompleteness theorem was about theories where the class of axioms and the rules of inference are rekursiv, which for Gödel at the time meant, as we would now put it, primitive recursive. [Recall, Gödel was initially writing in 1930/1931, a few years before the notion a general recursive function has been stably nailed down.]
  2. If a theory's theorems are recursively enumerable, then by Craig's theorem it is primitively recursively re-axiomatizable -- see Wikipedia. So there seems to be no real "relaxation" can be involved in re-stating Gödel's result in terms of recursively enumerable theories.
$\endgroup$
2
  • $\begingroup$ Thanks! BTW, I'm a native german speaker, and modern meaning of rekursiv in this context is the same as that of recursive in english, i.e. strictly weaker than primitiv recursive (which, ursurpringly, in german is called "primitiv rekursiv"). So even in german, the word changed its meaning over time. Interesting! $\endgroup$ – fgp Mar 19 '14 at 15:28
  • 2
    $\begingroup$ A key point is that, although the incompleteness theorems include an assumption about the effectiveness of the theory, the conclusion is about the theory itself, not about the axiomatization. So there is a certain extensionality to the conclusion of the theory. Because of Craig's theorem, it makes no difference whether we state the effectiveness condition in terms of r.e. axiomatizations, recursive ones, or primitive recursive ones - in any case we include exactly the same class of countable theories. $\endgroup$ – Carl Mummert Mar 24 '14 at 17:26

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.