Math 2.0

Mathematical logic and foundations Proof theory Concept

Sequent calculus

Builds on Proof theory

Summary

A sequent calculus is a proof system whose lines are sequents Γ⊢Δ\Gamma \vdash \Delta. Such a sequent is read as "if all formulas of Γ\Gamma hold, then some formula of Δ\Delta holds". Gentzen introduced the systems LK for classical logic and LJ for intuitionistic logic in 1934. Each connective has rules that introduce it on the left and on the right. This symmetry makes the calculus the main tool of structural proof theory.

Reading path

To understand this page from the ground up, read these 13 pages in order. The foundations come first.

Show the path as a graph
Proposition, concept, no evidence levelPropositionconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionModus ponens, concept, no evidence levelModus ponensconceptMathematical proof, concept, no evidence levelMathematical proofconceptPropositional logic, concept, no evidence levelPropositional logicconceptPredicate logic, concept, no evidence levelPredicate logicconceptProof theory, concept, no evidence levelProof theoryconceptSequent calculus, concept, no evidence levelSequent calculusconcept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Proposition concept
  2. Conjunction definition
  3. Disjunction definition
  4. Implication definition
  5. Negation definition
  6. Predicate definition
  7. Biconditional definition
  8. Modus ponens concept
  9. Mathematical proof concept
  10. Propositional logic concept
  11. Predicate logic concept
  12. Proof theory concept
  13. Sequent calculus concept

Where this leads

2 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Sequent_calculus
About this page
TagW72CA3R9MP
URIm2://W72CA3R9MP
Kindconcept
WritingW0 stub
MSC03F05, 03F03
UsesProof theory
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Results about this

Used by

Definitions