Sequent Calculus

In 1935, a 22-year-old named Gerhard Gentzen published a proof system so clean that it still powers every modern theorem prover, proof assistant and type-checker. He called it the Sequent Calculus.

The central object is a sequent: a statement of the form $\Gamma \vdash \Delta$, read "assuming everything in $\Gamma$, at least one thing in $\Delta$ holds." Think of $\Gamma$ as a bag of hypotheses on the left and $\Delta$ as a bag of conclusions on the right. A proof is a tree: you start with the goal sequent at the bottom and work upward, applying rules that break it into simpler sub-goals, until every leaf is an axiom (a trivially true sequent like $A \vdash A$).

What made Gentzen's system revolutionary is that every step is local and mechanical. Unlike the informal proofs mathematicians write by hand, a sequent-calculus proof can be checked by a computer in linear time — just walk the tree and verify each rule application. That mundane fact is the secret ingredient behind the halting problem boundary: we can reliably check proofs even when we cannot reliably find them.

The demo below shows a goal sequent at the bottom. Click Apply rule to break it into sub-goals using the matching left or right rule. Keep applying rules until every open goal becomes an axiom ($A \vdash A$). The full proof tree grows upward.

<!-- {{c_html_intro}} -->
<div class="sc-app">
  <div class="goal-label">{{label_goal}}</div>
  <div id="goal-display" class="sequent goal-sequent"></div>
  <div id="proof-tree" class="proof-tree"></div>
  <div id="status" class="status"></div>
  <div class="btns">
    <button id="btn-apply" type="button">{{btn_apply}}</button>
    <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
  </div>
  <details class="rules-ref">
    <summary>{{label_rules_ref}}</summary>
    <ul class="rule-list">
      <li><code>Ax</code> — {{rule_ax}}</li>
      <li><code>&amp;R</code> — {{rule_and_r}}</li>
      <li><code>&amp;L</code> — {{rule_and_l}}</li>
      <li><code>→R</code> — {{rule_imp_r}}</li>
      <li><code>→L</code> — {{rule_imp_l}}</li>
      <li><code>∨R</code> — {{rule_or_r}}</li>
    </ul>
  </details>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; font-size: 14px; }
.sc-app { padding: .5rem; }
.goal-label { font-size: .8rem; font-weight: 700; text-transform: uppercase;
              letter-spacing: .06em; color: #666; margin-bottom: .3rem; }
.sequent { font-family: ui-monospace, monospace; font-size: 1rem; padding: .35rem .6rem;
           background: #eef2f7; border: 1px solid #c8d4e0; border-radius: 6px;
           display: inline-block; margin-bottom: .5rem; }
.goal-sequent { background: #d4e8ff; border-color: #6aabf0; font-weight: 700; }
.proof-tree { margin: .5rem 0; min-height: 1.5rem; }
.node { margin-bottom: .4rem; }
.node-seq { font-family: ui-monospace, monospace; font-size: .9rem;
            padding: .25rem .5rem; border-radius: 6px; display: inline-block; }
.node-seq.open { background: #fff4cc; border: 1px solid #e0c840; }
.node-seq.axiom { background: #d6f5d6; border: 1px solid #72cc72; }
.node-seq.derived { background: #eef2f7; border: 1px solid #c8d4e0; color: #666; }
.rule-tag { font-size: .75rem; color: #888; margin-left: .4rem; }
.indent { margin-left: 1.4rem; border-left: 2px solid #d0d8e4; padding-left: .6rem; }
.status { font-size: .95rem; font-weight: 600; min-height: 1.4em; margin: .4rem 0; }
.status.ok { color: #0a7d33; }
.status.hint { color: #1d3557; }
.status.done { color: #6a0dad; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .85rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .4; cursor: default; }
.rules-ref { margin-top: .8rem; font-size: .82rem; color: #444; }
.rules-ref summary { cursor: pointer; font-weight: 600; }
.rule-list { margin: .4rem 0 0 1rem; padding: 0; list-style: disc; }
.rule-list li { margin: .15rem 0; }

// Code not found

Notice what just happened: you derived a tautology without any creativity — just a fixed menu of rules applied in the right order. That is the core promise of sequent calculus. Checking the finished tree takes a single pass; finding which rules to apply and in which order is where the real work hides.

Sequent calculus splits the work of reasoning into two radically different tasks.

Checking a proof tree is trivial: walk from leaves to root and verify that each node is a valid rule application. Every step is a local pattern match, so the whole tree is verified in time linear in its size — this is why proof assistants like Coq and Lean can trust the kernel.

Finding a proof is another matter entirely:

• Propositional logic (LK without quantifiers): proof search is PSPACE-complete. The search space can be exponential in the formula size, and the problem is as hard as any in PSPACE — harder than P vs NP suggests for NP.
• First-order logic (with $\forall$ and $\exists$): proof search is undecidable — there is no algorithm that halts and finds a proof for every valid formula. This is a direct consequence of Gödel's incompleteness theorems, which Gentzen's system was partly designed to illuminate.

Cut elimination (Gentzen's Hauptsatz) is the jewel of the theory: any proof that uses a "cut" rule (a lemma) can be transformed into a cut-free proof. This guarantees the subformula property — every formula that appears in a proof is a piece of the original goal — and makes proof search more tractable in practice. The transformation can, however, blow up proof size non-elementarily (a tower of exponentials).

So sequent calculus is not a silver bullet for automation: it hands us a rigorous framework and a clear complexity landscape, but finding proofs remains hard — or outright impossible for richer logics.

Sequent calculus is not just an academic curiosity — it is the engineering blueprint for a wide range of real systems:

• Proof assistants (Coq, Lean, Agda): the kernel of every major proof assistant is essentially a sequent-calculus checker. A user builds a proof term; the kernel just verifies each rule application. The de Bruijn criterion — trust only a small verified kernel — works precisely because checking is linear.
• Type theory and programming languages: the Curry–Howard correspondence maps sequent-calculus proofs to programs and propositions to types. Logic rules become typing rules; cut elimination becomes program reduction. Languages like Haskell and ML carry Gentzen's fingerprints in their type systems.
• Automated theorem provers: systems like Prover9 and leanCoP implement proof-search strategies (tableaux, resolution) that are direct descendants of sequent-calculus proof search.
• Structural proof theory: cut elimination lets logicians prove consistency of formal systems (Gentzen proved the consistency of Peano Arithmetic this way in 1936) and derive interpolation and definability results without model-theoretic detours.

Understanding sequent calculus gives you the skeleton of program equivalence checking, the logic of types, and the reason formal verification is both possible and hard.

Gerhard Gentzen built a machine for truth. His sequent calculus turned the vague activity of "doing mathematics" into a precise game of rule applications — one whose moves can be listed, checked and, in principle, searched by a computer.

The hard boundary he uncovered is still with us: checking a proof is always fast, finding one can be impossibly slow. That asymmetry is not a failure of Gentzen's system; it is an honest map of logical space. Every proof assistant, type checker and automated theorem prover working today is navigating exactly that map.

If you have ever wondered why computers are so good at verifying software and so bad at writing it from scratch, sequent calculus is a big part of the answer — and P vs NP is waiting just around the corner.