# Main differences and relations between Sequent Calculus and Natural Deduction

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) ?

• 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. Dec 25, 2016 at 11:02
• @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. Dec 25, 2016 at 11:54
• It seems that the particular point of view of Girard is symmetry and that the classical Natural Deduction has not this "property". Dec 25, 2016 at 14:00
• Relevant : Jean-Yves Girard, The Blind Spot : Lectures on Logic (2011), Ch.3 and 4 on Sequent calculus and Natural Deduction. Dec 25, 2016 at 14:07
• @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. Dec 25, 2016 at 14:42

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.