Proof of the deduction theorem in sequent calculus

Question

Can anybody recommend me a text, where the deduction theorem for predicate logic is proved in LK? I mean the following proposition:

if $A$ is a closed formula, and $B$ is arbitrary, then the existence of a Gentzen tree $$ \frac{\frac{\vdash A}{\dots}}{\vdash B} $$ implies the deducibility of the sequent $A\vdash B$ (or, equivalently, the deducibility of the sequent $\vdash A\to B$).

More generally, I wonder if there are textbooks on logic where the exposition is presented from the point of view of sequent calculus.

Answer 1

In sequent calculus, the Deduction Theorem is simply the $(\supset \text{Right})$ rule :

\begin{align} \frac{C, \Gamma \to \Delta, D}{\Gamma \to \Delta, C \supset D} (\supset \text R) \end{align}

See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.

You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).

Note on symbolism : I've followed Takeuti in using $\supset$ for the conditional conenctive ("if..., then...") and $\to$ for the "auxiliary symbol" used in the sequents : $\Gamma \to \Delta$.

---

---

Added (following Henning's comment).

We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $\to B$.

We apply $(\text {Weakening Left})$ to get : $A \to B$ followed by $(\supset \text{Right})$ to conclude with the sequent : $\to (A \supset B)$.

Regarding the quantifiers, the $(\forall \text { Right})$ rule is [see page 10] :

\begin{align} \frac{\Gamma \to \Delta, F(a)}{\Gamma \to \Delta, \forall x F(x)} (\forall \text { R}) \end{align}

with the restriction : $a$ does not occur in the lower sequent.

This means that we cannot use the derivation :

\begin{align} \frac{F(a) \to F(a)}{\to F(a) \supset \forall x F(x)} (\forall \text { R}) \end{align}

to derive te invalid $F(a) \supset \forall x F(x)$.