[soberhoff]

I don't agree with that definition of "effectively axiomatized". Granted, that's what Wikipedia says here: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... But the reference given doesn't check out. Franzén's 2005 book Gödel's Theorem doesn't say anything about effective axiomatization on page 112. He does however give the following definition in his lecture notes at: https://books.google.de/books?id=Wr51DwAAQBAJ&pg=PA138#v=one...

"If T is effectively axiomatized, in the sense that there is an algorithm for deciding whether or not a given sentence is an axiom of T,..."

In Computability: Turing, Gödel, Church and Beyond Martin Davis even makes the definition "T is axiomatizable if it has an axiom set that is computable" on page 42.

And that's also the definition Shoenfield gives on page 125 of Mathematical Logic.

Besides, "effective" has always been a synonym for "computable", "recursive", or "decidable" whenever I've encountered it in this context.

Also, I must insist that "it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive." is not what Craig's Theorem says. This is dangerously close to claiming that recursively enumerable sets are recursive which is plainly untrue. If recursively enumerable axioms (not just recursively enumerable theorems) are indeed interchangeable with recursive axioms, then I'd like to hear more about that.

[triska]

Yes, you are right: This is not what Craig's theorem says! It is enough to assume that the theorems are recursively enumerable. From this, it follows that there is an axiomatization where the axioms are recursive.

The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!