Proof calculus
1250665
206258342
2008-04-17T15:15:12Z
128.194.146.134
In [[mathematical logic]], a '''proof calculus''' corresponds to a family of [[formal system]]s 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 (mathematical logic)|theory]] of a logic.
Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi can be used for radically different logics. For example, a paradigmatic case is the sequent calculus, which can be used to express the [[consequence relation]]s 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 [[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, or might have been, 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, 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.
*[[Charles Peirce|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]].
[[Category:Proof theory]]
[[Category:Logical calculi]]