Back

Proofs in Deduction Modulo

Gilles Dowek
Section: Computation
Level: Advanced

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

PDFlecture notes

Lecturers

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