A Taste of Proof Theory (2002)

Course of the Midland Graduate School, 27.2. - 27.3.2002

Overview

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

Literature

• 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 Munich, 1999
• 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 it!

Course work

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

Notes

• 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.

Questions

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.