With respect to a deductive system $\text{L}$, describes any $\text{L}$-theory $T$ that is the deductive closure of a recursive set of axioms, i.e., there is a decidable set of sentences $\text{Γ}$ such that $T$ is the deductive closure of $\text{Γ}$. As an example, in classical first-order logic, Peano Arithmetic $\text{PA}$ is recursively axiomatizable, as there exists a decision procedure to determine whether a formula $\phi$ is an instance of one of the Peano axioms. This demonstrates that in the classical case, the recursive axiomatizability of $T$ does not entail that $T$ is decidable. That the axioms of $T$ are recursive means that one may enumerate all proofs of formulae from $T$. It follows that if $\phi \in T$, then a proof will appear in the enumeration, whence $T$ is semidecidable, but this does not provide a decision procedure determining when $\phi \notin T$. However, if $T$ is both recursively axiomatizable and negation complete, then if $\phi \notin T$, $\neg \phi \in T$, whence $T$ is decidable.