Difference between Gentzen and Hilbert Calculi 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?

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.
