Book article:

    Samuel R. Buss.
    "An Introduction to Proof Theory"
    in Handbook of Proof Theory, edited by S. R. Buss.
    Elsevier, Amsterdam, 1998, pp 1-78.

    Download article: postscript or PDF

    Table of contents: This is an introduction to proof complexity.

  1. Proof theory and Propositional Logic.
        Frege proof systems.
        The propositional sequent calculus.
        Proposition resolution refutations.
  2. Proof theory of first order logic.
        Syntax and semantics.
        Hilbert-style proof systems.
        The first-order sequent calculus.
        Cut elimination.
        Herbrand's theorem, interpolation and definability theorems.
        First-order logic and resolution refutations.
  3. Proof theory for other logics.
        Intuitionistic logic.
        Linear logic.


1. Theorem 2.5.3 (the generalized Herbrand Theorem) on page 52 is correct as stated, but has an error in its proof. I am grateful to Richard McKinley for discovering this, and also providing a corrected proof. A corrected proof is available in the manuscript "A sequent calculus demonstration of Herbrand's Theorem" by Richard McKinley.

 Back to Sam Buss's publications page.