By "axiomatic system", I have in mind a Hilbert-style proof system with axioms and (typically few) basic inference rules, where every theorem is provable from the axioms and these few rules. For sake of easy comparison, a Gentzen-style sequent system where every theorem can given a proof with only unconditional lines (sequents where nothing occurs on the left of the turnstile).
By "natural deduction system" I mean a proof system that relies on introduction and elimination rules, providing a relatively large set of inferences. For example, a Gentzen-style sequent calculus with some proofs necessarily containing lines with a non-empty set of premises to the left of the turnstile.
My question concerns the requirements for equivalence, in the sense of proving the same theorems. I'm particularly interested in what can be said at some level of generality, not restricting to a particular logic like propositional or first-order logic. What I know about some particular cases:
- (Classical) Propositional Logic: in order to secure equivalence to a natural deduction system with a $\rightarrow$-intro rule, the deduction theorem must hold in the axiomatic system.
- (Classical) First-Order Logic: in order to secure equivalence to a natural deduction system with a $\forall$-intro rule, universal generalization must hold in the axiomatic system.
But can anything interesting and more general be said about the conditions for equivalence, especially extending to other logics (e.g., modal logics and higher-order logics) and axiomatic theories in mathematics? (Especially those logics and mathematical theories that are incomplete?) What conditions are required to ensure that there will be a natural deduction equivalent for an axiomatic proof system (and vice versa)? Are there properties of an axiomatic or natural deduction system that definitively block equivalence?