CHAPTER 7 - EXTRACTING COMPUTATIONAL CONTENT FROM PROOFS

Summary

The treatment of our subject—proof and computation—would be incomplete if we could not address the issue of extracting computational content from formalized proofs. The first author has over many years developed a machine-implemented proof assistant, Minlog, within which this can be done where, unlike many other similar systems, the extracted content lies within the logic itself. Many non-trivial examples have been developed, illustrating both the breadth and the depth of Minlog, and some of them will be seen in what follows. Here we shall develop the theoretical underpinnings of this system. It will be a theory of computable functionals (TCF), a self-generating system built from scratch and based on minimal logic, whose intended model consists of the computable functions on partial continuous objects, as treated in the previous chapter. The main tool will be (iterated) inductive definitions of predicates and their elimination (or least-fixed-point) axioms. Its computational strength will be roughly that of ID_<ω, but it will be more adaptable and computationally applicable.

After developing the system TCF, we shall concentrate on delicate questions to do with finding computational content in both constructive and classical existence proofs. We discuss three “proof interpretations” which achieve this task: realizability for constructive existence proofs and, for classical proofs, the refined A-translation and Gödel's Dialectica interpretation. After presenting these concepts and proving the crucial soundness theorem for each of them, we address the question of how to implement such proof interpretations.