Proof Theory II (Winter 2026, TU Wien)

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

Exercise sessions (see below): Thursdays, 10am (academic time).

Place: TU Wien, Freihaus. Seminar Room Green 06B.
Course website on TUWEL.

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. The \omega-rule, infinitary proofs, proof of soundness and completeness for the infinitary proof system for \omega-logic.
November 3rd. Ordinal Analysis of PA, part I: embedding arithmetic into infinitary logic with cuts.
November 10th. Ordinal Analysis of PA, part II: cut elimination.
November 17th. No lecture.
November 24th. No lecture.
December 1st.
December 8th. No lecture (holiday).
December 15th.
January 12th.
January 19th.
January 26th.

See the TUWEL page for the list of exercises.

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

[2] G. Takeuti. Proof Theory (1975). North-Holland.