Proof Theory 2015/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
- 26 October: General introduction to proof theory and practicalities
- 27 October: Kripke semantics for intuitionistic propositional logic handout
- 2 November: Natural deduction for propositional logic handout
- 3 November: Hilbert-style proof calculi and negative translation handout
- 9 November: Sequent calculus for classical propositional logic handout
- 10 November: Classical consistency properties handout
- 16 November: Intuitionistic consistency properties and intuitionistic sequent calculi handout
- 17 November: Cut elimination handout
- 23 November: Semantics for classical and intuitionistic predicate logic handout
- 24 November: Proof systems and cut elimination for predicate logic handout
- 30 November: Arithmetic in all finite types handout
- 1 December: Modified realizability handout
- 7 December: Term extraction handout
- 8 December: Normalisation (not for the exam) 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.