Lecture Course on Proof Theory

Lecturer

Anton Setzer,
Uppsala University, Dept. of Mathematics, Polacksbacken, House 2, Room 138.
Tel.: (018) 471-3284 (office), (018) 301348 (home)
email:

Announcement

The topic of proof theory is the study of axiom systems, in which mathematical proofs can be formalized, mainly subsystems of set theory and analysis. The main goal of a proof theoretic analysis is the determination of the proof theoretic ordinal of a theory, a measure for its strength. In order to determine it, the full power of an axiom system has to be used, much more than usual in mathematics, and a deep insight into these systems is obtained. Proof theoretic methods are often the only way to reduce impredicative systems to more constructive principles. Such reductions are useful for theoretical computer science, because they allow to obtain the computable content of proofs, and provide at the same time solid foundations for mathematics.

As part of the year on mathematical logic at the Institut Mittag Leffler, a research institute for mathematics located close to Stockholm, the best proof theoretists in the world will visit this place in spring 2001 for longer periods. This course is intended as well to be a preparation for these visits.

Content:

• Part 1: Peano Arithmetic. The formal system of Peano arithmetic. Ordinal notation systems. Semi-formal systems. Cut elimination for Peano arithmetic. Well-ordering proofs.
• Part 2: Inductive Definitions. The theory ID_1. Collapsing functions. Proof theoretic analysis of ID_1.
• Part 3: Inaccessibles The axiom system of Kripke Platek set theory (KP). Analysis of KP + existence of one recursive inaccessible (KPI).
• Part 4: Mahlo Analysis of KP + existence of one recursive Mahlo ordinal (KPM).
• Part 5: Pi_3-reflection Analysis of KP + existence of one Pi_3-reflecting ordinal (KP\Pi_3).

Requirements

Logik MN1. Experience with logic in the form of one advanced logic course.

Coursebook

[Po89] Wolfgang Pohlers: Proof theory. Springer Lecture Notes in Mathematics 1407, 1989.
Research Articles

Further literature

[Sch77] Kurt Schütte: Proof theory. Springer, 1977.
[Gi87] Jean-Yves Girard: Proof theory and logical complexity, Vol. 1. Bibliopolis, Naples, 1987. (Available via Elsevier).
[Ta75] G. Takeuti: Proof theory. North-Holland, Amsterdam, 1975.

Location

Uppsala University, Department of Mathematics, Polacksbacken, house 2.
(For those living in Stockholm: Train service Stockholm - Uppsala now twice per hour).

Time

January 31 - May 18, 2000.

Schedule

 Weekday Date Time house room Monday 31.i. 10-12 2 345 Tuesday 1.ii. 15-17 2 114 No lecture on Thursday, 3.ii. Monday 7.ii. 15-17 2 215 Tuesday 8.ii. 10-12 2 314 Thursday 10.ii. 10-12 1 146 Monday 14.ii. 15-17 2 215 Tuesday 15.ii. 10-12 2 314 Thursday 17.ii. 10-12 1 146 Monday 21.ii. - 10.iv. 15-17 2 214 Tuesday from 22.ii. 10-12 2 314 Thursday from 24.ii. 10-12 2 314