Difference between Gentzen and Hilbert Calculi

Solution 1:

You can see a very detailed overview into : Francis Pelletier & Allen Hazen, Natural Deduction :

Sequent Calculus was invented by Gerhard Gentzen (1934), who used it as a stepping-stone in his characterization of natural deduction [...]. It is a very general characterization of a proof; the basic notation being $ϕ_1,\ldots,ϕ_n ⊢ ψ_1,\ldots,ψ_m$, which means that it is a consequence of the premises $ϕ_1,\ldots,ϕ_n$ that at least one of $ψ_1,\ldots,ψ_m$ holds.

If $\Gamma$􀀀 and $\Sigma$ are sets of formulas, then $\Gamma􀀀 ⊢ \Sigma$ means that it is a consequence of all the formulas of $\Gamma$􀀀 that at least one of the formulas in $\Sigma$ holds.

Sequent systems take basic sequents such as $ϕ ⊢ ϕ$ as axiomatic, and then a set of rules that allow one to modify proofs, or combine proofs. The modification rules are normally stated in pairs, ‘$x$ on the left’ and ‘$x$ on the right’: how to do something to the premise set $\Gamma$􀀀 and how to do it to the conclusion set $\Sigma$. So we can understand the rules as saying “if there is a consequence of such-and-so form, then there is also a consequence of thus-and-so form”.

These rules can be seen as being of two types: structural rules that characterize the notion of a proof, and logical rules that characterize the behavior of connectives. For example, the rule that from $\Gamma􀀀 ⊢ \Sigma$ one can infer $\Gamma􀀀,ϕ ⊢ \Sigma$ (“thinning on left”) characterizes the notion of a proof (in classical logic), while the rule that from 􀀀$\Gamma,ϕ ⊢ \Sigma$ one can infer $\Gamma􀀀, (ϕ∧ψ) ⊢ \Sigma$ (“∧-Introduction on left”) characterizes (part of) the behavior of the logical connective ∧ when it is a premise.

In the paper you can find an historical overview and several useful discussions; relevant for Rautenberg's textbook, see :

• 3.4 From Sequent Natural Deduction to Sequent Calculus
• 3.8 Natural Deduction with Sequences .

Solution 2:

Actually, Gentzen introduced two families of calculi, of which the more important perhaps are the natural deduction calculi (which Bruno Bentzen is referring to in his answer). Sequent calculi are rather different from both natural deduction calculi and Hilbert calculi. The latter are both ways of constructing arguments from propositions (wffs in the relevant logical language) to propositions; sequent calculi instead manipulate sequents (which can be read as metalinguistic claims about what follows from what in the relevant language).

What you really need to get to understand is, first, the relation between Hilbert calculi and Gentzen natural deduction calculi: see e.g. this handout of mine on various proof styles.

And then second, you need to understand the relation between natural deduction calculi and sequent calculi: see Ch. 1 of the splendid Structural Proof Theory by Sara Negri and Jan von Plato, available here.