Proof Theory II (Winter 2026, TU Wien)

Time: Tuesdays, 10am (academic time, i.e., really 10:15).
Place: TU Wien, Freihaus. Seminar Room Green 06A.

October 6th. Introduction. History of Proof Theory. Peano Arithmetic and subsystems (PRA, I\Sigma_n, B\Sigma_n).
October 13th. Some open problems. Wellorders. \Pi^1_1-completeness of wellorders. Spector's boundedness theorem. Definition of the \Pi^1_1-norm of a theory and proof that it is well-defined. Kreisel's counterexample.
October 20th. Definition of Q, PA, ACA0. Proof that ACA0 is \Pi^1_1-conservative over PA. The Tait-style sequent calculus for first-order logic. Proof of soundness and completeness and (semantic) cut-elimination.
October 27th.
November 2nd.
November 9th.
November 16th. No lecture.
November 24th.
December 1st.
December 8th. No lecture.
December 15th.
January 12th.
January 19th.
January 26th.

[1] W. Pohlers. Proof Theory: The First Step into Impredicativity (2009). Springer.