Page 9 - Textos de Matemática Vol. 38

1 1.1
PROOF INTERPRETATIONS
FERNANDO FERREIRA
Abstract. Stephen Kleene defined in 1945 an interpretation (known as realiz- ability) of Heyting arithmetic with the aim of making explicit the constructive content of intuitionistic proofs. Subsequently, this interpretation was modified by Georg Kreisel in the context of finite type arithmetic. A more sophisticated interpretation (functional interpretation) was found by Kurt G¨odel in 1958. It is an interpretation which, contrary to Kreisel’s modified realizability, is able to deal with Markov’s principle and, by this very reason, applies to classical proofs of existential statements via the negative translations (e.g., of G¨odel- Gentzen) of classical logic into intuitionistic logic. More recently, starting in the last decade, Ulrich Kohlenbach has been urging a shift of attention on the kind of information that interpretative proof theory should be focusing. He has been defending a shift of attention from precise witnesses to the extrac- tion of bounds from proofs of ∀∃ sentences. This shift of attention opened the way to the analysis of certain non-constructive principles and to the practical extraction of numerical bounds from proofs in classical analysis.
The traditional interpretations of Kleene/Kreisel and G¨odel (and Kohlen- bach) are based on transformations of formulas which preserve truth in the full set theoretic model. In the present course, we carefully introduce the the- oretical framework of finite type arithmetic and study the main properties of the traditional proof interpretations. We also study new proof interpretations (bounded interpretations) which are based on false assignments of formulas. They interpret novel principles, with no analogue in the known interpretations. For instance, a very general form of L. E. J. Brouwer’s Fan theorem (seen as a form of collection) is interpreted, and certain non-intuitionistic principles like weak K¨onig’s lemma or the lesser limited principle of omniscience (in the termi- nology of Errett Bishop) are either interpreted or can, somehow, be dealt with. Another feature of the bounded interpretations is the fact that they also inter- pret classically inconsistent principles. Nevertheless, they do apply to classical (or semi-intuitionistic) arithmetic and analysis. We also discuss some results of Kohlenbach obtained via more traditional interpretations.
Many results discussed in the course are not stated in their most general form, and many results are not given due credit during the exposition. We chose to make these simplifications in order to ease the understanding of the material and to speed-up the exposition. We provide a small annotated biblio- graphy which the reader can consult to find the full results, due credit and, eventually, find some clues to pursue the study of these matters.
First lecture
The language of finite type arithmetic
The finite types T are defined inductively: 0 (the base type) is a finite type; if τ and σ are finite types then τ → σ is a finite type. It is useful to have
1