I am struggling for the first time with the incompleteness theorem and similar stuff. I know that a theory is axiomatizable if it is equivalent to an axiomatized one, which means that the set of theorem of this latter one is decidable.
My question is: are there axiomatizable but not axiomatized theories? That is: can I find at least one theory in which the set of theorems is not decidable, but can be translated into a theory with a computable set of theorems?
Thank you in advance or your help!
I think the concept you refer to as "axiomatized" is what in my experience is usually called "recursively axiomatized" or "axiomatic". However, the definition of that is not that the set of theorems is decidable, but that the set of axioms is decidable.
In that case, an example of a recursively axiomatizable but not actually recursively axiomatized theory (over the language consisting of a single unary predicate $p$) could be $$ T=\{ \underbrace{p(x)\land p(x)\land\cdots\land p(x)}_{n\text{ conjuncts}} \mid n\text{ is the Gödel number of a true formula about the integers} \} $$ This theory is equivalent to the theory with a single axiom $p(x)$ (which is plainly recursively axiomatized), but it is not actually decidable whether or not a given formula is an axiom of $T$.