What exactly is necessary for the deduction theorem to hold?

Question

Suppose we have some set of sentences S that we call axioms and a theory T that specifies our rules of inference. Then we write $$S\vdash_TD$$ to mean that the sentence D is deducible from the axioms S using the rules of inference of T.

Let's assume that each rule of inference in T requires at least one premiss, for otherwise we can simply include its conclusion in S instead. (Question #1: Is this assumption reasonable?)

Now I am interested in exactly what conditions we can prove that

$$S\cup\{B\} \vdash_T C\quad\textrm{ if and only if }\quad S\vdash_T B\rightarrow C.\tag{1}$$ Clearly the "if" direction can be proved if we have the rule of modus ponens. The "only if" direction, or the "deduction theorem," (I believe it's called) is more problematic for me. Clearly if all the rules of inference of T are finitary, (i.e., each rule requires only a finite number of premisses,) then every sentence that can be deduced from S in the theory T can be deduced in a finite number of steps from a finite subset of S. Taken to the extreme we might say for some sentence D, that if $S\vdash_T D$, then $S'\vdash_TD$ for some finite subset $S'\subseteq S$ and so $$\emptyset\cup\{\Pi S'\} \vdash_T D\quad\textrm{ if and only if }\quad \emptyset\vdash_T \Pi S'\rightarrow D,\tag{2}$$ where $\Pi S'$ is the conjunction of all the sentences in S'. But this is absurd, because clearly nothing can be derived from the empty set if every rule of inference requires at least one premiss.

Question #2: Under my assumption, what kind of axioms must S contain in order for (1) to hold? Alternatively, (discarding my assumption,) what rules of inference are needed for (2) to also hold?

Answer 1

It is true to that you can separate all rules with zero premisses out from $T$ and insist that they appear in $S$ instead. However, there are various pragmatic reasons not to want to do that.

One of those reasons is, as you correctly argue, a $T$ that satisfies the Deduction Theorem in its full generality (that is, for an aribitrary $S$) must have at least one rule without premises.

A different reason is that requiring all of the logical axioms to be in $S$ rather than $T$ makes it very difficult to do with a finite $S$ -- or at least to keep single finite $S$ that you do all of your reasoning in. For example $T$ would commonly contain a single rule saying

Everything of the form $\Phi\to\Psi\to\Phi$ is a theorem, for all wffs $\Phi$ and $\Psi$.

but moving that into $S$ would generally require you to put all of the rules infinitely many instances into $S$ -- or to select a new $S$ containing finitely many of those instances each time you want to prove something new. Effectively, this choice would make it very difficult to speak about a first-order theory being finitely axiomatizable, for example.

(One could still cheat one's way around that by adding a dummy premise -- so we could have a rule in $T$ stating

Whenever $\Theta$ is a theorem, $\Phi\to\Psi\to\Phi$ is a theorem too, for all wffs $\Theta$, $\Phi$, and $\Psi$.

Then as long as $S$ is non-empty you still get the pragmatic benefits of a premise-less rule in $T$. But if you're planning to do that, it's much easier just to allow premise-less rules in the first place).

---

Question 2:

As far as I know, there's no simple characterization of those combinations of rules and logical axioms that satisfy the Deduction Theorem. Not, at least, one that is any simpler than simply saying "those logics that satisfy the Deduction Theorem".

One can give various sufficient conditions, of course -- for example, if the only premiseful rule in $T$ is modus ponens and $\Phi\to\Psi\to\Phi$ and $(\Phi\to\Psi\to\Theta)\to(\Phi\to\Psi)\to(\Phi\to\Theta)$ are both logical axioms, then you get the Deduction Theorem. But such conditions are far from being necessary.

By the way, another way of looking at your property (1) is that it is not so much about a property of the logic in itself, but about whether the connective on the right-hand side deserves to be called "implication" or not.

Answer 2

But this is absurd, because clearly nothing can be derived from the empty set if every rule of inference requires at least one premiss.

In sequent calculus, "nothing proves a tautology" (an empty set of statements to the left of the turnstyle) means that the statement to the right is a tautological conclusion of the rules of inference alone. $$\vdash_T S\to C$$