Proof Interpretations

Ulrich Kohlenbach

June 1998

Abstract:

These lecture notes are a polished version of notes from a BRICS PhD course given in the spring term 1998.

Their purpose is to give an introduction to two major proof theoretic techniques: functional interpretation and (modified) realizability. We focus on the possible use of these methods to extract programs, bounds and other effective data from given proofs.

Both methods are developed in the framework of intuitionistic arithmetic in higher types.

We also discuss applications to systems based on classical logic. We show that the combination of functional interpretation with the so-called negative translation, which allows to embed various classical theories into their intuitionistic counterparts, can be used to unwind non-constructive proofs.

Instead of combining functional interpretation with negative translation one can also use in some circumstances a combination of modified realizability with negative translation if one inserts the so-called A-translation (due to H. Friedman) as an intermediate step.

Contents

1

Introduction: Unwinding proofs

2

Intuitionistic logic and arithmetic in all finite types

3

Modified realizability

4

Majorizability and the fan rule

5

Gödel's functional (`Dialectica-')interpretation

6

Negative translation and its use combined with functional interpretation

7

The Friedman A-translation

8

Final comments

Available as PostScript, PDF, DVI.