Proof Interpretations

Ulrich Kohlenbach

June 1998


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.


Introduction: Unwinding proofs
Intuitionistic logic and arithmetic in all finite types
Modified realizability
Majorizability and the fan rule
Gödel's functional (`Dialectica-')interpretation
Negative translation and its use combined with functional interpretation
The Friedman A-translation
Final comments
Available as PostScript, PDF, DVI.

[BRICS symbol] BRICS WWW home page