# Proof systems for intuitionistic logic

Roy Dyckhoff ( School of Computer Science, University of St Andrews. )

- 14:00 24th October 2008 ( week 2, Michaelmas Term 2008 )Lecture Theater B

We survey the wide range of proof systems proposed for intuitionistic logic, emphasising the differences and their design for different purposes, ranging from ease of philosophical or other semantic justification through programming language semantics to automated reasoning. In particular we will mention (and perhaps even cover) a basic Hilbert-Frege system, Gentzen's natural deduction system

**NJ**, its modification**LJ**(aka**G1**) systems of Gentzen, the G3-style systems of Ketonen and Kleene, the multi-succedent calculus of Maehara, the focused calculi**LJQ**and**LJT**of Herbelin motivated by ideas of linear logic, the depth-bounded calculus**G4ip**of (independently) Vorob'ev, Hudelmaier and myself, the resolution calculus of Mints, the labelled calculus of Negri, and the deep inference calculus of Brünnler. [Some of my work on**LJT**was joint work with Luis Pinto; some of that on**LJQ**was joint work with Stéphane Lengrand.]