In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, a proof calculus corresponds to a family of formal system

Formal system

In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...

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

Theory (mathematical logic)

In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...

 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

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

 and relevance logic

Relevance logic

Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications be relevantly related. They may be viewed as a family of substructural or modal logics...

. Thus, loosely speaking, a proof calculus is a template or design pattern

Design pattern

A design pattern in architecture and computer science is a formal way of documenting a solution to a design problem in a particular field of expertise. The idea was introduced by the architect Christopher Alexander in the field of architecture and has been adapted for various other disciplines,...

, 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
  First-order logic
  First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
  
  ;
• Gerhard Gentzen
  Gerhard Gentzen
  Gerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...
  
  's calculus of natural deduction
  Natural deduction
  In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
  
  , which is the first formalism of structural proof theory
  Structural proof theory
  In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...
  
  , and which is the cornerstone of the formulae-as-types correspondence relating logic to functional programming
  Functional programming
  In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
  
  ;
• Gentzen's sequent calculus
  Sequent calculus
  In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
  
  , 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
  Aristotle
  Aristotle was a Greek philosopher and polymath, a student of Plato and teacher of Alexander the Great. His writings cover many subjects, including physics, metaphysics, poetry, theater, music, logic, rhetoric, linguistics, politics, government, ethics, biology, and zoology...
  
  's syllogistic calculus, presented in the Organon
  Organon
  The Organon is the name given by Aristotle's followers, the Peripatetics, to the standard collection of his six works on logic:* Categories* On Interpretation* Prior Analytics* Posterior Analytics...
  
  , readily admits formalisation. There is still some modern interest in syllogistic, carried out under the aegis of term logic
  Term logic
  In philosophy, term logic, also known as traditional logic or aristotelian logic, is a loose name for the way of doing logic that began with Aristotle and that was dominant until the advent of modern predicate logic in the late nineteenth century...
  
  .
• Gottlob Frege
  Gottlob Frege
  Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
  
  's two-dimensional notation of the Begriffsschrift
  Begriffsschrift
  Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book...
  
  is usually regarded as introducing the modern concept of quantifier to logic.
• C.S. Peirce's existential graph
  Existential graph
  An existential graph is a type of diagrammatic or visual notation for logical expressions, proposed by Charles Sanders Peirce, who wrote on graphical logic as early as 1882, and continued to develop the method until his death in 1914.-The graphs:...
  
   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
  Structural proof theory
  In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...
  
   have proposed calculi with deep inference
  Deep inference
  Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity...
  
  , for instance display logic, hypersequents, the calculus of structures
  Calculus of structures
  The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these...
  
  , and bunched implication.