0
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book? $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 9:15
  • $\begingroup$ Ok; in Wiki's entry dedicated to sequent calculus, it is used $\vdash$ for sequents and $\to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $\text R \to$ rule is like mine below (written upside-down). $\endgroup$
    – Mauro ALLEGRANZA
    Jul 17, 2018 at 9:30
  • $\begingroup$ Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ \frac{\frac{A\vdash A}{\dots}}{A\vdash B} $$ can be completed to a deduction for the sequent $A\vdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $\forall R$ and $\exists L$. $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 12:51
  • $\begingroup$ However, the question about a reference is still relevant. $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 12:54

1 Answer 1

Reset to default
3
$\begingroup$

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)$.

$\endgroup$
7
  • $\begingroup$ Mauro, I think this is a mistake: the meaning of the symbol $\vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $\vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $\vdash A$ to $\vdash B$ implies the deducibility of $\vdash A\to B$. $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 8:32
  • $\begingroup$ Mauro, I edited the question to clarify this. $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 8:44
  • 1
    $\begingroup$ @SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $\Gamma\to\Delta, D$ where $\to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,\Gamma\to\Delta,D$, and you can apply the $\supset$R rule to get what you want. $\endgroup$
    – hmakholm left over Monica
    Jul 17, 2018 at 12:16
  • $\begingroup$ (Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping). $\endgroup$
    – hmakholm left over Monica
    Jul 17, 2018 at 12:18
  • $\begingroup$ @HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you! $\endgroup$
    – Sergei Akbarov
    Jul 17, 2018 at 12:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.