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:

1. The Hilbert calculus, of which the most famous example is the 1928 Hilbert-Ackermann system of first-order logic;
2. 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;
3. 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:

1. 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;
2. Gottlob Frege's two-dimensional notation of the Begriffsschrift that is usually regarded as introducing the modern concept of quantifier to logic;
3. 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.