Philosophy 290-2

The seminar will cover in detail some basic results in proof theory. We will use the original articles by Gerhard Gentzen (1909–1945), who founded both structural proof theory and ordinal proof theory. In structural proof theory we will cover, among other things, the natural deduction calculus, the sequent calculus, cut-elimination and mid-sequent theorem for the sequent calculus, and various applications of such results. In ordinal proof theory we will study, among other things, Gentzen’s consistency proof for first-order Peano Arithmetic using ordinal induction up to epsilon-zero. In addition, we will also read some other logical and philosophical articles by Gentzen and some secondary literature, where appropriate. The seminar will be of interest to philosophers, logicians, computer scientists, linguists and mathematicians. Through this material, philosophy students will acquire the tools required for tackling further debates in philosophy of mathematics (prospects for Hilbert’s program and its relativized versions etc.) and philosophy of logic and language (meaning of the logical constants; proof-theoretic semantics; realism/anti-realism, Dummett’s program (normalization, harmony etc.)). Graduate students in philosophy may use this course for satisfying the formal philosophy course requirement (i.e. a course in the 140 series or equivalent).

The minimal requirement for taking the seminar is Philosophy 12A (Introduction to Logic), although a certain amount of logical/mathematical maturity (but no specific knowledge of advanced mathematics) will be necessary for mastering the material.