Introduction to Proof Theory

This is the home page for a short course to be taught by Jeremy Avigad and Henry Towsner at Notre Dame, during the weeks of June 6 and June 13, 2005. This course is funded by NSF's Division of Mathematical Sciences and the Notre Dame Philosophy Department.

The course is still in the planning phase, so all the information below is tentative and subject to change. If you are registered, please contact Jeremy Avigad (avigad@cmu.edu) at some point with answers to the questionnaire below.

Tentative schedule

Morning lecture: 10:00-11:30 (Monday - Friday)
Afternoon lecture: 2:00-3:30 (Monday - Thursday)

We will meet Monday through Friday each week, though we will only hold the morning lecture on Friday. In lieu of homework, we will assign optional problems and hold an informal "problem session" for anyone interested in working on them.

Problem session: 5:00-6:30 (Monday - Thursday)

Tentative syllabus

It is hard to gauge what can be done in such a short time frame. Here is the current, rough, plan.

Week 1 will introduce some of the basics of proof theory, including:

• deductive systems for classical and intuitionistic logic
• translations between logics
• the cut elimination theorem
• properties of first-order logic (Herbrand's theorem, explicit definability for intuitionistic logic, the interpolation theorem)
• primitive recursion, coding, and the language of arithmetic.

Week 2 will survey some more advanced topics, including, as time allows:

• the conservativity of Sigma-1 induction over Primitive Recursive Arithmetic
• the ordinal analysis of first-order arithmetic
• the Paris-Harrington theorem
• the elimination of weak König's lemma

Resource page

We have set up a resource page and begun populating it with handouts, references, and draft chapters of a textbook. Because the textbook is still in a preliminary form, the resource page is generally inaccessible to the public. Simply e-mail Jeremy Avigad for the login and password.

Drafts of the textbook chapters and other items posted on the resource page should provide sufficient material to support the lectures. But a good secondary reference for much of the material treated the first week is:

• Troelstra and Schwichtenberg, Basic Proof Theory, second edition. Cambridge University Press, Cambridge, 2000.

It is available on Amazon for about $35, and the emphasis is on structural proof theory. The treatment is terse and encyclopedic, which can make it hard to read as an introductory text. There is an online review here.

Questionnaire

1. What is your background in logic (field of interest, current instutition, courses taken, etc.)?
2. What would you like to get out of this course?
3. Some specifics: have you ever worked with a natural deduction proof system? seen a cut elimination theorem? convinced yourself that any reasonable computable function is primitive recursive? convinced yourself that assertions about "finitary" mathematical objects can be expressed in the language of arithmetic?