Difference between Gentzen and Hilbert Calculi

Question

What is the difference between Gentzen and Hilbert Calculi?

From my understanding of Rautenberg's Concise Introduction to Mathematical Logic, Gentzen calculus is based on sequents and Hilbert calculus, on tautologies.

But isn't every Gentzen sequent a tautological modus ponens?

For instance, the sequent $X\vdash a \wedge b |X \vdash a,b$ can be written as the tautology $\forall X \forall a \forall b\:( X\vdash a \wedge b \rightarrow X \vdash a,b$), can't it?

Answer 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 .

Answer 2

Both systems are equivalent in the sense that they proof the same theorems.

A Hilbert-style deduction system uses the axiomatic approach to proof theory. In this kind of calculus, a formal proof consists of a finite sequence of formulas $\alpha_1, ..., \alpha_n$, where each $\alpha_n$ is either an axiom or is obtained from the previous formulas via an application of modus ponens.

Of course, many theorems of it look like Gentzen's natural deduction inference rules, if the the enhancement relation is to be represented in the object language through the material implication:

• $\vdash(A\land B) \rightarrow A $ $\ \ \ \ $ and $ \ \ \ $ $\displaystyle \frac{A \land B}{A} $
• $\vdash((A \rightarrow \bot) \rightarrow \neg A) $ $\ \ \ \ $ and $ \ \ \ $ $\displaystyle \frac{\frac{A}{\bot} }{\neg A} $
• $\vdash A \rightarrow (A \lor B) $ $\ \ \ \ $ and $ \ \ \ $ $\displaystyle \frac{A}{A \lor B} $

From left to right, Hilbert and Genzten-style respectively.

But this has a lot of technical drawbacks. Hilbert-style proofs are pretty artificial and harder to carry out in comparison to Gentzen-style proofs: To see this for yourself, try to provide an axiomatic proof of $A \rightarrow B,B \rightarrow C \vdash A \rightarrow C$ and then a Gentzen-style proof of it. In your axiomatic proof, consider as an exercise to prove it with and without using the deduction theorem in your proof.

Have you noticed the difference? It is partially due to the fact that in Hilbert-style calculus one are not allowed you to make hypothetical reasoning, that is, arguments like "let $P$ ... conclude $Q$, hence $P$ implies $Q$" (see the implication introduction rule) which is part of the daily practice of a mathematician. The deduction theorem kind of compensates this, but this is still a big drawback.

Answer 3

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.