Proof calculus

Overview

• Language: The set of formulas admitted by the system, for example, propositional logic or first-order logic.
• Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems.
• Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms.

Examples of proof calculi

• 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.

• 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 easily might have been seminal, had history worked out differently.

• Several systems have been proposed which replace the usual textual syntax with some graphical syntax. Proof nets and cirquent calculus are among such systems.
• 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.