Proof calculus

From Wikipedia, the free encyclopedia

Informally, we may say that a proof calculus determines a family of formal systems which specify inference rules that characterize a logical system. As opposed to the application of the term calculus in such contexts as lambda calculus, it is usually inappropriate to identify a calculus with a particular formal system, since such paradigmatic cases as the sequent calculus are used to express such radically different consequence relations as intuitionistic logic and relevance logic. A better model, perhaps, is to say that a calculus is a template or design pattern that may be applied to produce formal systems, but there is no consensus among logicians on how best to define the term.

[edit] Examples of proof calculi

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

The Hilbert calculus, 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 seminal, but are not widely used today:

Aristotle's system of syllogistic presented in the Organon readily admits formalisation. There is still some modern interest in syllogistic that is carried out under the aegis of term logic;
Gottlob Frege's two-dimensional notation of the Begriffsschrift that is usually regarded as introducing the modern concept of quantifier to logic;
C.S. Pierce'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.