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:


Course work

  1. coursework, put on the web 27.2.02,
  2. coursework, put on the web 6.3.02,


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


  1. 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 prime theories.
  2. 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.

Thorsten Altenkirch
Last modified: Wed Mar 27 16:01:57 GMT 2002