# 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

- coursework, put on the web 27.2.02,
- 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.

Greg Restall, *Extending Intuitionistic Logic with Subtraction*
### Questions

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