Proofs in Deduction Modulo
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'
- 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
- 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.
78153 Le Chesnay Cedex