In my comment on this question, I mentioned that there was a generalized form of the deduction theorem that looks something like this
For any finite set of formulae, $\Gamma$
$$\dfrac{\Gamma\vdash\psi}{\vdash\bigwedge\Gamma\to\psi}$$
The only problem is, I can't figure out where this came from! I'm almost certain that this is a named theorem that I've seen in a textbook or article somewhere and the fact that I can't find a source is extremely frustrating.
Does anyone know what this theorem is called or have a reference for it? I'm not trying to figure out the proof (which is easy) – I just need to know that I haven't gone mad.
Note:
I think that I saw this somewhere in the context of sequent calculus; the original form might have been
$$\dfrac{\Gamma,\Delta\vdash\psi}{\Gamma\vdash\bigwedge\Delta\to\psi}$$
Best Answer
In the literature on proof systems, given a finite set of formulas $\Delta$, there are no "official" names for theorems of the form
$$\tag{1}\dfrac{\Delta \vdash\psi}{\vdash\bigwedge\Delta\to\psi}$$ and its "generalization"
$$\tag{2}\dfrac{\Gamma,\Delta\vdash\psi}{\Gamma\vdash\bigwedge\Delta\to\psi}$$
other than deduction theorem, because $(1)$ and $(2)$ just are the deduction theorem, written in a slightly different syntactical form.
Indeed, since $\Delta$ is finite, in any reasonable proof system the fact that $\Gamma, \Delta \vdash \psi$ (i.e. $\psi$ is derivable from the sets of formulas $\Gamma$ and $\Delta$) is equivalent to say that $\Gamma, \bigwedge \Delta \vdash \psi$ (i.e. $\psi$ is derivable from the set of formulas $\Gamma$ and the conjunction of the formulas in $\Delta$). By deduction theorem (in its apparently restricted form), from $\Gamma, \bigwedge \Delta \vdash \psi$ it follows that $\Gamma \vdash \bigwedge \Delta \to \psi$.
According to Occam's razor, "entities should not be multiplied without necessity", which is always a good principle. Here, $(1)$ and $(2)$ are essentially the same as deduction theorem, so there is no need to give them another name such as "generalized deduction theorem" or whatever, just because of their slightly different syntactical notation. I would distrust textbooks, articles and notes that call $(1)$ or $(2)$ in a way different from deduction theorem, because they would just complicate something that is actually simpler.
The fact that $(1)$ and $(2)$ are nothing but the deduction theorem, is evident in the context of sequent calculus. Here, the rules $(1)$ and $(2)$ are derivable, which roughly means that they can be simulated by means of the (more "atomic") inference rules of sequent calculus. More precisely, the rule $(2)$ is derivable by means of the inference rules $$\dfrac{\Gamma, \varphi_1, \varphi_2 \vdash \psi}{\Gamma, \varphi_1 \land \varphi_2 \vdash \psi}\land_L \qquad\qquad \dfrac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi \to \psi}\to_R $$ Indeed, we have
$$ \dfrac {\dfrac {\dfrac{\Gamma,\Delta\vdash\psi}{\vdots}\land_L} {\Gamma, \bigwedge\Delta \vdash \psi} \land_L} {\Gamma\vdash\bigwedge\Delta \to \psi}\to_R $$
The rule $\to_R$ internalizes the (apparently "restricted" version of) deduction theorem within the proof system, and $\land_L$ is an inference rule that is valid in any reasonable logic system (as a rule or a meta-rule). Summing up, to prove that $(2)$ (and hence $(1)$, take $\Gamma = \emptyset$) is derivable in the sequent calculus, we just need a rule that is always valid and the sequent calculus version of deduction theorem. So, $(1)$ and $(2)$ do not express anything more than deduction theorem.