The effects of requiring a recursive vs. a recursively enumerable axiomatization in the incompleteness theorem

Question

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?

Answer 1

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.