Back

Description

Deduction modulo is a new framework that seems particularily well-suited to study proofs and proof search methods in various theories, such as equational theories, the simple type theory, set theory, stratified set theories, etc. The goal of this course is to present deduction modulo and to use it to present basic results in proof theory (Gentzen' theorem, Girard's theorem, Crabbe' counter-example, ...)

1. First-order logic
   First-order language, first-order logic, proofs, models.
2. Natural deduction and cut elimination
   Natural deduction, classical and constructive logic, Curry-de Bruijn-Howard isomorphism, cut elimination in the empty theory, applications to proof search and to programming in constructive logic.
3. Deduction modulo
   Deduction and computation in proof search, rewriting terms and rewriting propositions. The equivalence lemma. Prawitz' cuts and cuts modulo. Reducibility candidates. Pre-models. Examples of theories having the cut elimination property. Set theory as a theory modulo. Crabbé's counter-example.
4. Type theory
   Type theory as a first-order theory. Deduction and computations in type theory. Girard's theorem.
5. Equality and arithmetic
   Equality cuts. Induction cuts. Leibniz' equality. Numbers in type theory. Cut elimination in arithmetics.

Materials

lecture notes

Lecturers

Gilles Dowek
INRIA-Rocquencourt
B.P. 105
78153 Le Chesnay Cedex
France
Gilles.Dowek@inria.fr
http://pauillac.inria.fr/~dowek