Proof calculus

This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (January 2009)

In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules. The specific inference rules of a member of such a family characterize the theory of a logic.

Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determining and can be used for radically different logics. For example, a paradigmatic case is the sequent calculus, which can be used to express the consequence relations of both intuitionistic logic and relevance logic. Thus, loosely speaking, a proof calculus is a template or design pattern, characterized by a certain style of formal inference, that may be specialized to produce specific formal systems, namely by specifying the actual inference rules for such a system. There is no consensus among logicians on how best to define the term.

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.