[jrvidal]

I think the precise pre-condition is that the theory should be recursive, which means either a finite list of axioms _or_ a computable check to determine whether a given formula is an axiom.