Mathematics 293A: Proof Theory
(Philosophy 353A--Enroll in Math 293A)
Winter 2004-2005
Syllabus
Instructor: Solomon Feferman <sf@csli.stanford.edu>
Office hours: Wed 1:15-2:05, Th 3:45-4:30 and by arrangement, Room 380-383Z
Class hours: Tu Th 11:00-12:15, Room 380-381T
Course description: Gentzen's natural deduction and sequential calculi for first-order propositional and predicate logics. Normalization and cut-elimination procedures. Relationships with computational lambda calculi. Extensions to infinitary calculi; ordinal measures of complexity. Applications to the extraction of the constructive content of proofs in arithmetic and analysis. Extensions of Hilbert's consistency program.
Prerequisites: Phil 151, 152 (formerly 160A, B) and Math 161, or equivalents, or consent of the instructor.
NB:
Math 293B (Phil 353B) will not be offered
2004-2005.
Text: A.S. Troelstra and H. Schwichtenberg, Basic Proof
Theory, Second Edition
(Cambridge,
2000), paperback. Required.
Reserve material: Math-CS Library, 3 Day Loan Period
1. A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd Edition
2. M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen
3. G. Takeuti, Proof Theory, 2nd Edition
4. K. SchŸtte, Proof Theory
5. S. Buss (ed.), Handbook of Proof Theory
6. W. Pohlers, Proof Theory. An introduction. Lecture Notes in Mathematics 1407
7. S. Feferman, Lectures on Metamathematics
8. M. H. Lob (ed.), Proceedings of the Summer School in Logic, Lecture Notes in Mathematics 70.
Other resources:
Work for the course:
Grading: Letter, with P/NC option.
Auditors: Class and room size permitting, auditors are welcome
to attend.