16
$\begingroup$

What are the main differences between the Sequent Calculus and the Natural Deduction (independently of if we're working with classical, intuitionistic or another logic) ?

As far as I know :

Differences :

  • The sequent calculus is more suitable for automated proof search. Why is that so ?
  • The cut rule is implicit (based on $\Rightarrow$-intro and $\Rightarrow$-elim, right ?) in the Natural Deduction and explicit in the Sequent Calculus.
  • The Natural Deduction give a more mathematical-like approach to reasoning while the Sequent calculus give more structural and symmetrical approach.
  • I read (about the Sequent Calculus) that It presents numerous analogies with natural deduction, without being limited to the intuitionistic case in Proof and Types by J-Y Girard. Why is Natural Deduction said to be limited to the intuitionistic case ? Can't we add a rule for the excluded middle to simulate classical logic ?

Relations :

  • One can be translated to the other

I can't think of others ones.

Are my claims above right ? Is there any other interresting differences and relations (or fact) ?

$\endgroup$
9
  • $\begingroup$ Last bullett : correct; it is enough to add to the intuitionistic rules of Natural Deduction the rule for Double Negation (or equivalently : LEM) to get the classical version. See e.g : Sara Negri & Jan von Plato, Structural Proof Theory (2001), Ch.8.2 and 8.4 for TRANSLATION FROM SEQUENT CALCULUS TO NATURAL DEDUCTION and vice-versa. $\endgroup$ Dec 25, 2016 at 11:02
  • $\begingroup$ @MauroALLEGRANZA So how can we explain the quote I provided from Proof and Types ? I think it's deeper than technical details like adding a rule for classical logic. $\endgroup$
    – Boris
    Dec 25, 2016 at 11:54
  • $\begingroup$ It seems that the particular point of view of Girard is symmetry and that the classical Natural Deduction has not this "property". $\endgroup$ Dec 25, 2016 at 14:00
  • $\begingroup$ Relevant : Jean-Yves Girard, The Blind Spot : Lectures on Logic (2011), Ch.3 and 4 on Sequent calculus and Natural Deduction. $\endgroup$ Dec 25, 2016 at 14:07
  • $\begingroup$ @MauroALLEGRANZA (i) Ok, but I don't see how the intuitionistic Natural Deduction (NJ) is more symmetric than the classical one (NK). (ii) I already came across The Blind Spot but it was (globally) a bit hard to read for me. I will still try to check the chapter 3 and 4. Thanks. $\endgroup$
    – Boris
    Dec 25, 2016 at 14:42

1 Answer 1

5
$\begingroup$

Probably your last comment about double negation elimination breaking the symmetry of natural deduction is the 'reason' for the cited quote, though I don't agree with the sentiment.

Basically, natural deduction has introduction and elimination rules for each one of "$\land$" and "$\lor$" and "$\to$", which correspond to their intended meanings. We also have negation introduction in the form "$A \to \bot \vdash \neg A$" and negation elimination in the form "$A , \neg A \vdash \bot$". So double negation elimination (DNE) is an 'odd one out', so to speak, being "$\neg \neg A \vdash A$" or equivalently "$( A \to \bot ) \to \bot \vdash A$". I'm excluding the principle of explosion here because it is redundant in the presence of DNE.

Also, note that you can prove each instance of LEM using DNE plus the other rules, so adding DNE suffices to recover classical logic. If you added LEM instead of DNE, you would also have to add the principle of explosion, namely "$\bot \vdash A$" for any proposition $A$. In that sense DNE can be said to be slightly stronger than LEM. Intuitively it is obviously the case, because we would need at least one rule that reduces the total number of occurrences of "$\neg$" or "$\bot$", and LEM does not do so. Both the principle of explosion and DNE reduce that number, by $1$ and $2$ respectively. But adding just the principle of explosion is not enough to get classical logic, because it only results in intuitionistic logic.

For your other points, your statement that natural deduction is less suitable than sequent calculus for automated proof systems is arguably false. Even though the LK calculus works without the cut rule, it is not useful to take that rule away because it shortens proofs drastically in the same way that allowing on-the-fly definitions makes modern mathematics possible (we can't get far if we're not allowed to define arbitrary new terminology).

And as for the cut rule being implicit in ND via implication introduction and elimination, well is that really implicit? We could modify the other rules appropriately so that none of them use the implication symbol, and then indeed those two rules would become redundant in the same manner as the cut rule. So it looks quite explicit to me. As with LK, it is not useful in practice to take away these rules.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .