Under what conditions does an axiomatic proof system have a natural deduction equivalent?

Question

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:

1. (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.
2. (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?

Answer 1

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.

First, the reason that natural deduction systems have more rules is because they use more logical connectives ... you could make an axiomatic system for more connectives as well, and it would likewise have more axioms. In fact, the most natural way to create an axiomatic system with rules for all the usual connectives is to make those rules conditionalizations of the typical Elim and Intro rules, e.g. you might have an axiom $(P \rightarrow Q) \rightarrow ((Q \rightarrow P) \rightarrow (P \leftrightarrow Q))$ as the axiomatic conditionalization of a typical $\leftrightarrow$ Intro rule, while something like $(P \leftrightarrow Q) \rightarrow (P \rightarrow Q)$ would be a good candidate to axiomatize the $\leftrightarrow$ Elim inference rule.

I point this out because in the above paragraph you seem to make a connection between the number of rules and the fact that a natural deduction system uses assumptions ... but those are unrelated, as one can make an axiomatic system with effectively those very rules (but conditionalizations thereof). The core difference, then, between axiomatic systems and natural deduction systems, is indeed just the fact that you can make assumptions (i.e start 'subproofs') or, as you say, a sequent system with non-empty sets of support.

However, this potential connection between rules and axioms can also be used to address your very question: at least it would seem that as long as you conditionalize the Elim and Intro rules in the way I suggested above, you can ensure that the axiomatic system can do whatever a natural deduction system can do. And for going the other way around ... well, if the axioms in the axiomatic system are indeed the conditionalized versions of the Intro and Elim rules of a natural deduction system, then the Deduction Theorem would seem to suffice.

Of course, if there is no such systematic connection between axioms and inference rules, then all bets are off, and you'd have to prove the equivalence between the different systems on a more ad hoc basis,... in other words, I couldn't tell you any 'general requirements for equivalence' ... other than being able to prove both system are complete by themselves of course.