| Description: |
We will study the proof theory of Gentzen-type sequent
calculi. Our first major result will be Gentzen's Hauptsatz -- the
eliminability of the cut rule in a sequent calculus adequate for
first-order logic with equality. As corollaries, we will provide purely
syntactic proofs of, among other things, the interpolation theorem,
Beth's implicit definability theorem, and Herbrand's theorem. The
course will culminate in a discussion of a Gentzen-Schütte style
proof of the consistency of Peano arithmetic using transfinite
induction up to the ordinal epsilon-nought. |