Philosophy 290-2

The seminar is devoted to three extensions of Hilbert’s program that came in the wake of Gödel’s incompleteness theorems. After some sections devoted to Hilbert’s original program, we will work through the details of three consistency proofs for Peano Arithmetic. The first is due to Gödel and Gentzen who independently showed that the consistency of Peano Arithmetic can be reduced to the consistency of Heyting’s Arithmetic; the second, due to Gentzen, uses transfinite induction up to the ordinal epsilon zero; and the third, the so-called Dialectica interpretation due to Gödel, appeals to recursive functionals of finite type. For the first two proofs we will use P. Mancosu, S. Galvan, and R. Zach, An Introduction to Proof Theory. Normalization, Cut-Elimination, and Consistency Proofs, Oxford University Press, 2021.