Description

This course examines different options for representing the structure of
proof, such as natural deduction, sequent systems, proofnets, display
logic and calculus of structures.  We will focus on the topological &
structural properties of different kinds of proof (single premise, single
conclusion, multiple premise, multiple conclusion, directed, and
undirected proofnets, etc.), the techniques useful for representing
different kinds of logics (classical, constructive, modal, substructural,
etc.) the kinds of methods used for proving normalisation and cut
elimination theorems, and the relationships between different proof
systems.  

The core of the course will be straightforward presentations of
normalisation and cut elimination proofs in simple settings (logics with a
minimum of structural rules so the proofs are manageable), and then
modifications and additions are made on the basis of this foundation.