Philosophy 149

The course will cover in detail the basic results of structural and ordinal proof theory. Both branches of proof theory go back to the work of Gerhard Gentzen who, working in the tradition of Hilbert’s program, established the foundational results of the discipline in the 1930s. In structural proof theory, they include the formulation of natural deduction systems and sequent calculi and the major metatheorems about them (normalization and sub-formula property for natural deduction; cut elimination and sub-formula property for sequent calculi). In ordinal proof theory, Gentzen gave a constructive proof of the consistency of Peano Arithmetic by means of ordinal notations and a principle of induction for such notations (up to an ordinal called epsilon-zero). The lectures will be based on a forthcoming book on proof theory by Prof. Mancosu. The course will be of interest to philosophers, logicians, mathematicians, computer scientists, and linguists. 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, i.e., normalization, harmony etc.). Prerequisites: Phil 12A or equivalent.