Skip to content
Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

Reading Sequent calculus in wikipedia

I read this article for making the validator of proofs in LK/LJ. So I would occasionally skip the part which is irrelavant to LK or LJ.

  • Hilbert style proof calculus
    • Each line is an unconditional tautology = theorem.
  • Gentzen style proof calculus
    • Each line is a conditional tautology. Conditions are on the left.
    • Natural deduction
      • every line has exactly one assertion on the right.
    • Sequent calculus
      • every line has zero or more assertions on the right.

Hilbert style has only a few rules, but needs many axioms. Gentzen style have more rules than Hilbert style, but needs fewer axioms.

  • LK was introduced in 1934.
  • LJ was introduced in 1935.

The cut elimination theorem on LK and LJ is called Gentzen's Hauptsatz. It is later used to prove the consistency of Peano arithmetics.

  • Sequent calculi (ie LK and LJ) are also called Gentzen's systems.

(Hilbert's system seems a little different from sequent calculi)

  • Natural deduction
    • Judgement is a form, A0, ..., An |- B
  • Sequent Calculus
    • Sequent is a form, A0, ..., An |- B0, ..., Bn
You can’t perform that action at this time.