What does it mean to say that a formal theory is recursive The wikipedia article on Formal Theories states that
"A formal system is said to be recursive (i.e. effective) or recursively enumerable if the set of axioms and the set of inference rules are decidable sets or semidecidable sets, respectively."
Does this mean that that the set of theorems of a formal theory is recursive (i.e. decidable) if the sets of its axioms and inference rules are decidable? That doesn't seem right---the sets of axioms and inference rules of FOL are decidable, but theoremhood isn't.
 A: It appears that you are confounding two distinct yet related notions of decidability here. The first has to do with computability and the second with completeness. If the set of axioms and rules of inference for a formal theory are decidable in the first sense, then there exists a finite procedure by which one can determine whether a sentence in the formal language is indeed an axiom of the theory, or whether it has been obtained via an application of one of the rules of inference. Hence one can effectively decide (i.e., compute) whether a finite list of sentences is a valid derivation of a theorem.
To assert that a theory is decidable in the second sense (i.e., completeness) is to say that for any given sentence $\varphi$ in the formal language, either $\varphi$ or $\neg \varphi$ can be derived in a finite number of steps from the axioms of the theory. The First Incompleteness Theorem tells us that any consistent formal theory that extends Robinson arithmetic is undecidable in the sense of completeness. That is, there exist sentences $\varphi$ in the language of arithmetic without any formal proof of either $\varphi$ or $\neg \varphi$. But these formal theories of arithmetic are nonetheless decidable in the earlier sense of having a recursive set of axioms and rules of inference.
