Proof Theory 2018: Contents
Contents of the course
- Intuitionistic and classical logic
- Hilbert-style proof systems, natural deduction, sequent calculus
- Kripke semantics for intuitionistic logic
- Negative translation
- Cut elimination
- Goedel's T
- Arithmetic in finite types
- Modified realizability
- Provably total functions in Heyting and Peano arithmetic
- Existence and disjunction property for Heyting arithmetic
Contents of the individual lectures
- 6 February: General introduction to proof theory and practicalities
- 8 February: Kripke models for intuitionistic logic handout
- 13 February: Natural deduction handout
- 15 February: Negative translation and Hilbert-style proof calculi handout
- 20 February: Classical sequent calculus handout
- 22 February: Cut elimination and intuitionistic sequent calculus handout
- 27 February: Normalisation for natural deduction handout
- 1 March: Strong normalisation for natural deduction and the typed lambda calculus handout
- 6 March: Predicate logic: Kripke models and natural deduction handout
- 8 March: Predicate logic: sequent calculus handout
- 13 March: Goedel's T and arithmetic in finite types handout
- 15 March: Modified realizability handout
- 20 March: Term extraction handout
Exercise sheets
To main page.