14. Sequent Calculus Perspective and Equivalence to Natural Deduction

Working System

This chapter uses reusable code from book/advanced/sequent_imp.py. We stay in implication-only intuitionistic logic and split code into proof search, extraction, and checking.

14. Sequent Calculus Perspective and Equivalence to Natural Deduction#

Goal. Give executable evidence for the equivalence between two proof presentations in the implication-only fragment:

  1. Sequent calculus derivations (\(\Gamma \vdash A\)).

  2. Natural deduction proof terms (\(\Gamma \vdash t : A\)).

You will learn

  • The core sequent rules for implication and how they drive backward proof search

  • How proof search corresponds to building lambda terms (extraction)

  • How to check an extracted term against the original goal

  • Why some classical principles (for example Peirce’s law) are not derivable intuitionistically

  • How to read the search/extract/check pipeline as a computational witness of equivalence

Roadmap#

  1. Define formulas (Atom, Imp) and the sequent rules for the implication fragment.

  2. Run proof search sq.prove on a few goals and see which are provable.

  3. Extract a natural deduction term from a sequent proof (sq.prove_and_extract).

  4. Check the extracted term against the goal (sq.check_nd).

  5. Interpret the results as operational evidence for proof-system equivalence.

Sequent Rules (Implication Fragment)#

We use three rules:

Axiom:

\[ \frac{}{\Gamma, A \vdash A}\;(\mathrm{Ax}) \]

Right implication:

\[ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}\;(R\to) \]

Left implication:

\[ \frac{\Gamma \vdash A \quad \Gamma, B \vdash C}{\Gamma, A\to B \vdash C}\;(L\to) \]

ND Correspondence#

Natural deduction terms use:

\[ \lambda x.t \quad (\to I), \qquad t\;u \quad (\to E). \]

The equivalence theorem is proved by structural induction on derivations. Here we provide executable translations and checks in the implication fragment.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "advanced").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from advanced import sequent_imp as sq

Proof Search in Sequent Calculus#

A = sq.Atom("A")
B = sq.Atom("B")

goals = [
    sq.Imp(A, A),
    sq.Imp(sq.Imp(A, B), sq.Imp(A, B)),
    sq.Imp(sq.Imp(sq.Imp(A, B), A), A),  # classical-only principle
]

for g in goals:
    pf = sq.prove((), g, depth=12)
    print("goal:", sq.show_f(g))
    print("  provable by search:", pf is not None)

goal: (A -> A)
  provable by search: True
goal: ((A -> B) -> (A -> B))
  provable by search: True
goal: (((A -> B) -> A) -> A)
  provable by search: False

Extract ND Terms From Sequent Proofs#

For each successful sequent proof, we extract a lambda term.

for g in goals:
    pf, term = sq.prove_and_extract(g, depth=12)
    print("goal:", sq.show_f(g))
    if term is None:
        print("  no extracted term")
        continue
    print("  extracted term:", sq.show_t(term))
    print("  ND check against goal:", sq.check_nd(term, g, {}))

goal: (A -> A)
  extracted term: (lambda h0. h0)
  ND check against goal: True
goal: ((A -> B) -> (A -> B))
  extracted term: (lambda h0. h0)
  ND check against goal: True
goal: (((A -> B) -> A) -> A)
  no extracted term

Reading Equivalence Computationally#

For this fragment, the pipeline

\[ \text{sequent proof} \to \text{ND term} \to \text{goal check} \]

acts as an executable witness for one direction of equivalence. The reverse direction is standard by induction on ND typing derivations.

Reuse Note

The module advanced/sequent_imp.py can be reused for:

  • custom proof search experiments,

  • extraction benchmarks,

  • adding conjunction/disjunction rules in later work.

Exercise

  1. Prove and extract a term for \(A \to (B \to A)\) (the K combinator shape). Check it with sq.check_nd.

  2. Prove and extract a term for \(((A \to (B \to C)) \to ((A \to B) \to (A \to C)))\) (the S combinator shape). Check it.

  3. Try to prove Peirce’s law \(((A \to B) \to A) \to A\) by increasing the search depth. Confirm it remains unprovable in this intuitionistic fragment.

  4. Provide a non-empty context h:A->B, a:A and prove B. Extract the ND term and check it against B under the same context. See solutions: Exercise 14 (Sequent Calculus)

Summary#

  • Sequent calculus rules can be read operationally as a goal-directed proof search procedure.

  • Successful sequent proofs can be turned into lambda terms by extraction.

  • Checking the extracted ND term against the original goal is a concrete sanity check of soundness.

  • Classical principles show up as goals that systematically fail in intuitionistic proof search.

  • Next: Chapter 15 introduces control operators, which provide computational realizations of classical principles.

Contents