I am reading Computability and Logic by Boolos, Burgess, and Jeffrey.
Godel's first incompleteness theorem is stated as there not being a consistent, complete, axiomatizable theory for arithmetic.
The theory being axiomatizable is defined as there being a recursive set of axioms from which all sentences in the theory can be derived.
My question: What happens if we change the definition of axiomatizability by saying that a set is axiomatizable iff there is a semi-recursive set of axioms from which all sentences in the theory can be derived?
My thoughts: If the axioms that axiomatize the theory form a semi-recursive set, then we may no longer be able to decide whether some statement is an axiom or not, but we can still recognize an axiom as an axiom. Hence, we can still create predicates that arithmetically define things like "$x$ is the Godel number of one of the axioms", and thus also "$x$ is a proof of some statement $y$, where every statement in the proof is either an axiom, or is derived from earlier statements in the proof". So, the Godel proof can proceed as normal.
Is this correct?
Best Answer
Yes, it is enough for the set of axioms to be recursively enumerable.
Such a set is always logically equivalent to a decidable set of axioms anyway: if $(\varphi_n)_n$ is a computable enumeration of your favorite axioms, we can instead consider the axioms $$ \{\, \varphi_n \land (\underbrace{x=x\lor \cdots\lor x=x}_{n\text{ copies}}) \,\mid n\in\mathbb N \} $$ (or some other way to encode the index in the axiom without changing its meaning).
But we don't even need to go as far as encoding this numbering in the logical structure of the axioms; we can also just define that in our proof objects an application of an axiom must consist of a pair of the axiom and a certificate that it is in the enumerated set. The construction in the incompleteness theorem already needs to use an unbounded quantifier to express "a proof of such-and-such exists", so we can require all kinds of additional decorations to be part of the proofs without upsetting the general structure of the argument.