A Taste of Proof Theory (2002)
Course of the Midland Graduate School, 27.2. - 27.3.2002
The course will give a first taste of proof theory, covering
the following topics:
- Three types of proof systems and their properties:
- Hilbert style (H)
- Natural deduction (N)
- Gentzens sequent calculus (G)
- Cut elimination and its applications
- Peano arithmetic (HA) is Pi02 conservative over Heyting arithmetic (HA)
- The strength of arithmetic
- W. Buchholz, Lecture notes of a
course on proof theory, 2nd chapter is in german!
at the University of Munich, 1998
- H.Schwichtenberg, Lecture notes of
a course on proof theory at the University of
- A.S.Troelstra and H.Schwichtenberg Basic
Proof Theory, Cambridge University Press, 2000
Could students form Nottingham please refrain from
recalling that book but come directly to me if you need
- coursework, put on the web 27.2.02,
- coursework, put on the web 6.3.02,
- 1st note contains the rules for all propositional systems.
- 2nd note contains the rules for predicate logic
Symmetric Intuitionistic Logic
At the last lecture I talked about symmetric intutionistic logic (SIL). I include below
the article by Greg Restall and my (open) homework questions.
Greg Restall, Extending Intuitionistic Logic with Subtraction
- Reprove completeness of Kripke models for SIL. There is a proof in Restall's article
essentially I am asking to reprove this using saturated contexts (as seen in Matt's lecture) instead of
- Can the model construction be extended from Kripke models to
presheaf models s.t. presheafs turn out to be models of
symmetric CCCs? (Here some knowledge gained in Neil's category
theory course may come in handy).
If you have questions about the questions please send me an email.
Last modified: Wed Mar 27 16:01:57 GMT 2002