Proof Theory 2016: 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
- 31 October: General introduction to proof theory and practicalities
- 3 November: Kripke semantics for intuitionistic logic handout
- 7 November: Hilbert-style proof calculi and natural deduction handout
- 10 November: Negative translation handout
- 14 November: Sequent calculus for classical propositional logic handout
- 17 November: Cut elimination and sequent calculus for intuitionistic propositional logic handout
- 21 November: Normalisation for natural deduction handout
- 24 November: Strong normalisation for natural deduction handout
- 28 November: Semantics and natural deduction for predicate logic handout
- 1 December: Cut elimination for predicate logic handout
- 5 December: Goedel's T and arithmetic in finite types handout
- 8 December: Modified realizability handout
- 12 December: Term extraction handout
Exercise sheets
First Exercise Sheet
Second Exercise Sheet
Third Exercise Sheet
Fourth Exercise Sheet
Fifth Exercise Sheet
Sixth Exercise Sheet
Seventh Exercise Sheet
To main page.