10
$\begingroup$

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?

$\endgroup$
  • 5
    $\begingroup$ Gentzen's calculus is a "calculus" for the derivability relation : $\vdash$. It has a strict link with the "standard" Hilbert calculus, but the main difference is that $\to$ is a connective in the language while $\vdash$ is a relation in the meta-language. $\endgroup$ – Mauro ALLEGRANZA Jun 9 '15 at 13:59
  • 1
    $\begingroup$ The post contains several confusions between object-language and metalanguage. First, $X\vdash a\land b|X\vdash a,b$ isn't a sequent, it's two sequents. (Note also that informally, $X\vdash a,b$ means "the truth of all of $X$ logically requires the truth of at least one of $a,b$.") Second, presumably by "tautology" the author Rautenberg means a formula $a$ such that $\vdash a$ is derivable in a Hilbert-system. The expression preceding the "can't it?" is not a "tautology" in that sense. It should be rewritten "If $X\vdash a\land b$ is derivable, then so is either $X\vdash a$ or $X\vdash b$." $\endgroup$ – mmw Jun 9 '15 at 14:27
7
$\begingroup$

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 .
$\endgroup$
7
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ What do you mean by hipotethical reasoning and why doesn't Hilbert Calculus allow you to conduct it? $\endgroup$ – Bruno Schiavo Jun 9 '15 at 14:05
  • $\begingroup$ Don't rules like $\frac{A\land B}{A}$ belong to natural deduction rather than to Gentzen's sequent calculus (what he called $LK$)? E.g., $LK$ doesn't contain "elimination rules" but left and right introduction rules. $\endgroup$ – mmw Jun 9 '15 at 14:35
  • $\begingroup$ @mmw Indeed I am referring to his natural deduction calculus. I've made it explicit now as an edit. $\endgroup$ – Bruno Bentzen Jun 9 '15 at 15:05
  • $\begingroup$ "To see this for yourself, try to provide an axiomatic proof of A→B,B→C⊢A→C and then a Gentzen-style proof of it. " Well, if the axiom set include CCpqCCqrCpr or CCpqCCrpCrq, then the axiomatic proof actually ends up as easier than the natural deduction proof. Also, if either of those two can get deduced easily enough, the axiomatic proof is easier. If our axiom set include CpCqp and CCpCqCrsCpCCqrCqs, we can get to CCpqCCrpCrq in a single condensed detachment. So, for that axiom set getting to the rule you've cited only takes three steps. $\endgroup$ – Doug Spoonwood Jun 9 '15 at 22:31
  • $\begingroup$ Arguably though getting to CCpqCCrpCrq from CCpCqCrsCpCCqrCqs and CpCqp qualifies as harder than the whole natural deduction proof, since it involves substitution in both CpCqp and CCpCqCrsCpCCqrCqs. But then again, arguably it's easier, since it only requires a single detachment and a single unification. $\endgroup$ – Doug Spoonwood Jun 9 '15 at 22:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.