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?