# Proof calculus > Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Proof_calculus > Markdown URL: https://mediated.wiki/source/Proof_calculus.md > Source: https://en.wikipedia.org/wiki/Proof_calculus > Source revision: 1297556806 > License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/) Formal language used to prove statements This article relies excessively on references to tertiary sources. Please improve this article by adding secondary or primary sources. Find sources: "Proof calculus" – news · newspapers · books · scholar · JSTOR (December 2024) (Learn how and when to remove this message) In [mathematical logic](/source/Mathematical_logic), a **proof calculus** or a **proof system** is built to prove [statements](/source/Statement_(logic)). ## Overview A proof system includes the components:[1][2] - [Formal language](/source/Formal_language): The set *L* of formulas admitted by the system, for example, [propositional logic](/source/Propositional_logic) or [first-order logic](/source/First-order_logic). - [Rules of inference](/source/Rules_of_inference): List of rules that can be employed to prove theorems from axioms and theorems. - [Axioms](/source/Axioms): Formulas in *L* assumed to be valid. All [theorems](/source/Theorem) are derived from axioms. A [formal proof](/source/Formal_proof) of a [well-formed formula](/source/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.[2] 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](/source/Sequent_calculus), which can be used to express the [consequence relations](/source/Consequence_relation) of both [intuitionistic logic](/source/Intuitionistic_logic) and [relevance logic](/source/Relevance_logic). Thus, loosely speaking, a proof calculus is a template or [design pattern](/source/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](/source/Hilbert_system),[2] of which the most famous example is the 1928 [Hilbert–Ackermann system](/source/Hilbert-Ackermann_system) of [first-order logic](/source/First-order_logic); - [Gerhard Gentzen](/source/Gerhard_Gentzen)'s calculus of [natural deduction](/source/Natural_deduction), which is the first formalism of [structural proof theory](/source/Structural_proof_theory), and which is the cornerstone of the [formulae-as-types correspondence](/source/Formulae-as-types_correspondence) relating logic to [functional programming](/source/Functional_programming); - Gentzen's [sequent calculus](/source/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](/source/Aristotle)'s [syllogistic](/source/Syllogistic) calculus, presented in the *[Organon](/source/Organon)*, readily admits formalisation. There is still some modern interest in [syllogisms](/source/Syllogism), carried out under the [aegis](/source/Aegis) of [term logic](/source/Term_logic). - [Gottlob Frege](/source/Gottlob_Frege)'s two-dimensional notation of the *[Begriffsschrift](/source/Begriffsschrift)* (1879) is usually regarded as introducing the modern concept of [quantifier](/source/Quantifier_(logic)) to logic. - [C.S. Peirce](/source/Charles_Sanders_Peirce)'s [existential graph](/source/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 nets](/source/Proof_net) and [cirquent calculus](/source/Cirquent_calculus) are among such systems. - Recently, many logicians interested in [structural proof theory](/source/Structural_proof_theory) have proposed calculi with [deep inference](/source/Deep_inference), for instance [display logic](/source/Display_logic), [hypersequents](/source/Hypersequent), the [calculus of structures](/source/Calculus_of_structures), and [bunched implication](/source/Bunched_implication). ## See also - [Method of analytic tableaux](/source/Method_of_analytic_tableaux) - [Proof procedure](/source/Proof_procedure) - [Propositional proof system](/source/Propositional_proof_system) - [Resolution (logic)](/source/Resolution_(logic)) ## References 1. **[^](#cite_ref-1)** Anita Wasilewska. ["General proof systems"](http://www3.cs.stonybrook.edu/~cse541/chapter7.pdf) (PDF). 1. ^ [***a***](#cite_ref-:0_2-0) [***b***](#cite_ref-:0_2-1) [***c***](#cite_ref-:0_2-2) ["Definition:Proof System - ProofWiki"](https://proofwiki.org/wiki/Definition:Proof_System). *proofwiki.org*. Retrieved 2023-10-16. --- Adapted from the Wikipedia article [Proof calculus](https://en.wikipedia.org/wiki/Proof_calculus) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Proof_calculus?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.