# Generalized Deduction Theorem

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}$$

• I encountered this in a lecture on the Hilbert calculus, where it was referred to as "the conditional proof fact". I can't seem to find anything on google referring to it as this though. It may be that its un-named (outside of been referred to as a conditional proof). Commented Dec 11, 2020 at 3:03

## 1 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.

• On the one hand, I see what your saying; on the other, there is a subtle but important difference between "for all finite sets $\Delta$, we can prove $\Delta\vdash\psi\implies\vdash\bigwedge\Delta\to\psi$," and "we can prove that $\Delta\vdash\psi\implies\vdash\bigwedge\Delta\to\psi$ for all finite sets." This is the only reason to distinguish "the" deduction theorem from its generalization. Commented Dec 15, 2020 at 14:36
• Compare and contrast Goldbach's conjecture - it is a small matter to build a function that takes an even number as its argument and returns two primes whose sum is that number. It is another matter entirely to show that such a function is total (i.e. to prove Goldbach's conjecture). Commented Dec 15, 2020 at 14:37
• In this case, it all works out to be the same, since we can prove the "generalized" form by induction and/or recursion. The only reason I was looking for a name was so I could say "by the X theorem, it follows that Y." I thought that I had seen this before, but I guess I was mistaken. It seems that I have gone quite mad, indeed. Commented Dec 15, 2020 at 14:41