 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. == see also == * propositional proof system * proof nets
Logical_calculi Proof_theory