{{Short description|Formal language used to prove statements}} {{tertiary sources|date=December 2024}} In [[mathematical logic]], a '''proof calculus''' or a '''proof system''' is built to prove [[Statement (logic)|statements]].
==Overview== A proof system includes the components:<ref>{{Cite web| url=http://www3.cs.stonybrook.edu/~cse541/chapter7.pdf| title=General proof systems |author=Anita Wasilewska}}</ref><ref name=":0">{{Cite web |title=Definition:Proof System - ProofWiki |url=https://proofwiki.org/wiki/Definition:Proof_System |access-date=2023-10-16 |website=proofwiki.org}}</ref> * [[Formal language]]: The set ''L'' 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 [[Theorem|theorems]] are derived from axioms.
A [[formal proof]] of a [[well-formed formula]] in a proof system is a set of axioms and rules of inference of the proof system that infers that the well-formed formula is a theorem of the proof system.<ref name=":0" />
Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined 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 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 class of [[Hilbert system]]s,<ref name=":0" /> of which the most famous example is the 1928 [[Hilbert-Ackermann system|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 [[syllogism]]s, carried out under the [[aegis]] of [[term logic]]. *[[Gottlob Frege]]'s two-dimensional notation of the ''[[Begriffsschrift]]'' (1879) is usually regarded as introducing the modern concept of [[Quantifier (logic)|quantifier]] to logic. *[[Charles Sanders Peirce|C.S. Peirce]]'s [[existential graph]] easily might have been seminal, had history worked out differently.
Modern research in logic teems with rival proof calculi: *Several systems have been proposed that replace the usual textual syntax with some graphical syntax. [[proof net]]s 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]], [[hypersequent]]s, the [[calculus of structures]], and [[bunched implication]].
== See also == * [[Method of analytic tableaux]] * [[Proof procedure]] * [[Propositional proof system]] * [[Resolution (logic)]]
==References== {{Reflist}}
[[Category:Proof theory]] [[Category:Logical calculi]]