Natural Deduction and Sequent Calculus

Natural deduction and the sequent calculus are the two Gentzen-style formal systems that represent proofs through introduction and elimination rules for the logical connectives, forming the basic machinery of structural proof theory.

Definition

Natural deduction derives formulas from assumptions using introduction and elimination rules that mirror informal reasoning, while the sequent calculus manipulates sequents, assertions that a list of formulas entails another, through rules acting on the left and right of an entailment.

Scope

This topic covers the rules of natural deduction with their introduction and elimination pairs, the structure of the sequent calculus with its left and right rules and structural rules, normalization for natural deduction, the relationship between the two systems, and their intuitionistic and classical variants.

Core questions

• How do introduction and elimination rules confer meaning on the logical connectives?
• What is a sequent and how do its rules differ from those of natural deduction?
• How does normalization simplify natural deduction proofs?
• How are the classical and intuitionistic versions of these calculi related?

Key theories

Introduction and elimination rules

Each connective is governed by rules that introduce it and rules that exploit it, and their harmony, that elimination recovers exactly what introduction puts in, expresses the meaning of the connective.

Normalization theorem

Prawitz showed natural deduction proofs can be reduced to a normal form free of detours where an introduction is immediately undone by an elimination, the natural deduction analogue of cut-elimination.

Correspondence of the two calculi

Natural deduction and the sequent calculus prove the same theorems and can be translated into one another, with sequent left rules corresponding to natural deduction elimination rules.

Clinical relevance

These calculi are the standard formats for studying proofs structurally: natural deduction underlies type theory and proof assistants through the proofs-as-programs correspondence, while the sequent calculus, with its subformula property after cut-elimination, is the basis of automated proof search and analytic tableaux.

History

Gentzen introduced both natural deduction and the sequent calculus in 1934 and 1935, devising the sequent calculus to obtain his cut-elimination theorem after finding natural deduction harder to analyze. Prawitz revived natural deduction in 1965 with a thorough normalization study, and the systems became central to the later proofs-as-programs developments.

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

What is the difference between natural deduction and the sequent calculus?

Natural deduction works with formulas under a context of assumptions and uses elimination rules, closely matching informal proof. The sequent calculus works with explicit entailments and replaces elimination rules with left-introduction rules, a format that makes cut-elimination and the subformula property transparent.

Why is normalization important?

A normal proof contains no detours and has the subformula property, so every formula in it is a subformula of the conclusion or premises. This constrains the shape of proofs, yields consistency results, and, via the proofs-as-programs correspondence, corresponds to evaluating a program to a value.