Lecture Course on Proof Theory
Graduate Course, January 31 - May 18, 2000
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 |
Examples