Gentzen sequent calculus + cut-elimination

Layer 0 — Mathematicsin the proof-theory subtree

Gentzen 1934 LK / LJ sequent calculi for classical / intuitionistic logic. Hauptsatz: cut-elimination → consistency-proofs + decidable propositional fragments. Foundation of structural proof-theory.