Introduction

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⊢AA \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.

Try It

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⊢AA \vdash A). The full proof tree grows upward.

<!-- Sequent calculus proof builder — derive (A & B) -> A step by step -->
<div class="sc-app">
  <div class="goal-label">Goal sequent:</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">Apply rule</button>
    <button id="btn-reset" type="button" class="ghost">Reset</button>
  </div>
  <details class="rules-ref">
    <summary>LK rule reference</summary>
    <ul class="rule-list">
      <li><code>Ax</code> — if A appears on both sides: A, Γ ⊢ Δ, A</li>
      <li><code>&amp;R</code> — split conjunction right: Γ ⊢ A  and  Γ ⊢ B  gives  Γ ⊢ A ∧ B</li>
      <li><code>&amp;L</code> — use conjunction left: A, B, Γ ⊢ Δ  gives  A ∧ B, Γ ⊢ Δ</li>
      <li><code>→R</code> — introduce implication right: A, Γ ⊢ B  gives  Γ ⊢ A → B</li>
      <li><code>→L</code> — use implication left: Γ ⊢ A and B, Γ ⊢ Δ  gives  A→B, Γ ⊢ Δ</li>
      <li><code>∨R</code> — introduce disjunction right: Γ ⊢ A, B  gives  Γ ⊢ A ∨ B</li>
    </ul>
  </details>
</div>

/* Styles for the sequent calculus interactive proof builder */
* { 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; }

// Sequent calculus demo — step-by-step LK derivation of (A & B) -> A
// The goal is the tautology (A & B) -> A, proved in 3 rule steps
// Goal tautology: (A & B) -> A
// Proof tree (bottom-up, LK rules):
//   ->R: (A & B) -> A  becomes  A & B |- A
//   &L:  A & B |- A    becomes  A, B  |- A
//   Ax:  A, B  |- A    (axiom — A appears on both sides)

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));

// Ordered steps: index 0 = initial goal (not yet applied), 1..3 = rule applications
const STEPS = [
  {
    rule: null,
    seq: '⊢ (A ∧ B) → A',
    note: 'Initial goal',
    children: []
  },
  {
    rule: '→R',
    seq: 'A ∧ B ⊢ A',
    note: 'Apply →R: move antecedent to the left',
    children: []
  },
  {
    rule: '∧L',
    seq: 'A, B ⊢ A',
    note: 'Apply ∧L: split the conjunction on the left',
    children: []
  },
  {
    rule: 'Ax',
    seq: 'A, B ⊢ A',
    note: 'Axiom: A appears on both sides',
    children: [],
    isAxiom: true
  }
];

let stepIdx = 0;
// lines accumulated for the growing proof tree
let treeLines = [];

function seqClass(idx) {
  if (idx < stepIdx) {
    if (STEPS[idx].isAxiom) return 'axiom';
    return 'derived';
  }
  return 'open';
}

function renderTree() {
  const container = document.getElementById('proof-tree');
  container.innerHTML = '';
  if (stepIdx === 0) return;
  // Show the derivation chain from current top down to the original goal.
  // Show the derivation chain from current top down to the original goal.
  for (let i = stepIdx; i >= 1; i--) {
    const step = STEPS[i];
    const div = document.createElement('div');
    div.className = 'node';
    const indent = document.createElement('div');
    indent.className = 'indent';
    const seqDiv = document.createElement('div');
    const cls = step.isAxiom && i < stepIdx ? 'axiom' : (i === stepIdx ? 'open' : 'derived');
    seqDiv.className = 'node-seq ' + cls;
    seqDiv.textContent = step.seq;
    const tag = document.createElement('span');
    tag.className = 'rule-tag';
    tag.textContent = '[' + step.rule + ']';
    indent.appendChild(seqDiv);
    indent.appendChild(tag);
    div.appendChild(indent);
    container.prepend(div);
  }
}

function setStatus(msg, cls) {
  const el = document.getElementById('status');
  el.textContent = msg;
  el.className = 'status ' + cls;
}

function applyStep() {
  if (stepIdx >= STEPS.length - 1) return;
  stepIdx++;
  renderTree();
  const step = STEPS[stepIdx];
  if (step.isAxiom) {
    setStatus(i18nFmt('Axiom reached: %seq%', { seq: step.seq }), 'ok');
    document.getElementById('btn-apply').disabled = true;
    setStatus('Proof complete! Every goal reduced to an axiom.', 'done');
  } else {
    setStatus(i18nFmt('Applied [%rule%] — new goal: %seq%', { rule: step.rule, seq: step.seq }), 'hint');
  }
}

function reset() {
  stepIdx = 0;
  treeLines = [];
  renderTree();
  document.getElementById('btn-apply').disabled = false;
  setStatus('Click "Apply rule" to begin the derivation.', 'hint');
  const goalEl = document.getElementById('goal-display');
  goalEl.textContent = STEPS[0].seq;
}

document.getElementById('btn-apply').addEventListener('click', applyStep);
document.getElementById('btn-reset').addEventListener('click', reset);

// Initialize the demo
reset();
Result
Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/sequent-calculus/Content licensed under CC BY-NC 4.0.