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, ...)

- First-order logic

First-order language, first-order logic, proofs, models.
- 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.
- 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.
- Type theory

Type theory as a first-order
theory. Deduction and computations in type theory. Girard's theorem.
- 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