Introduction to Proof Theory
Posted under: Course and Workshop Descriptions; Logic and Computation.
Proof theory studies proofs as mathematical objects. It is not only a part of logic, it is also of importance for linguistics and computer science:
- parsing a sentence with a categorial grammar is the same as searching a proof in a deductive system, and
- the two paradigms of proof-search-as-computation and proof-normalization-as-computation are the foundations for logic programming and functional programming.
The course will give a basic introduction to proof theory, focussing on those aspects of the field that are most relevant to ESSLLI. In particular, the student will learn what is a deductive system and why cut elimination is important. The course will also discuss the presentation of proofs via proof nets, which are graph-like objects that allow to quotient away the syntactic bureaucracy of deductive systems. Finally, we will also see how category theory can be used to describe proofs as algebraic objects.
The main emphasis will be put on the observation that the various ways of presenting proofs are just different aspects of the same theory. We will use the notion of deep inference to substanciate this observation and to visualize the close relationship between deductive systems, categories, and proof nets: A morphism in a category is the same as a derivation in a deductive system, and a proof net is the same as the flowgraph of a derivation or the coherence graph in the category.
The course outline is as follows:
Lecture 1: Introduction and Overview
Lecture 2: Deductive Systems — Proofs as Syntactic Objects
Lecture 3: Cut Elimination — Proofs as Objects for Rewriting
Lecture 4: Proof Nets — Proofs as Combinatorial Objects
Lecture 5: Logic and Categories — Proofs as Algebraic Objects
Further particulars (e.g, prerequisites):
The course does not require any knowledge in proof theory nor category theory. But the student should know the basics of propositional logic.
I’ve been teaching a related course on “Proof Nets and the Identity of Proofs” at ESSLLI 2006. Lecture notes are available here: http://www.lix.polytechnique.fr/~lutz/papers/ESSLLI06notes.pdf
