Proof Calculus - Examples of Proof Calculi

Examples of Proof Calculi

The most widely known proof calculi are those classical calculi that are still in widespread use:

• The class of Hilbert systems, of which the most famous example is the 1928 Hilbert-Ackermann system of first-order logic;
• Gerhard Gentzen's calculus of natural deduction, which is the first formalism of structural proof theory, and which is the cornerstone of the formulae-as-types correspondence relating logic to functional programming;
• Gentzen's sequent calculus, which is the most studied formalism of structural proof theory.

Many other proof calculi were, or might have been, seminal, but are not widely used today.

• Aristotle's syllogistic calculus, presented in the Organon, readily admits formalisation. There is still some modern interest in syllogistic, carried out under the aegis of term logic.
• Gottlob Frege's two-dimensional notation of the Begriffsschrift is usually regarded as introducing the modern concept of quantifier to logic.
• C.S. Peirce's existential graph might easily have been seminal, had history worked out differently.

Modern research in logic teems with rival proof calculi:

• Several systems have been proposed which replace the usual textual syntax with some graphical syntax.
• Recently, many logicians interested in structural proof theory have proposed calculi with deep inference, for instance display logic, hypersequents, the calculus of structures, and bunched implication.