Classical proofs as programs: How, what and why

Abstract

We recapitulate Friedman's conservative extension result of (suitable) classical over constructive systems for Π ⁰₂ sentences, viewing it in two lights: as a translation of programs from an almost-functional language (with C) back to its functional core, and as a translation of a constructive logic for a functional language to a classical logic for an almost-functional language. We investigate the computational properties of the translation and of classical proofs and characterize the classical proofs which give constructions in concrete, computational terms, rather than logical terms. We characterize different versions of Friedman's translation as translating slightly different almost-functional languages to a functional language, thus giving a general method for arriving at a sound reduction semantics for an almost-functional language with a mixture of eager and lazy constructors and destructors, as well as integers, pairs, unions, etc. Finally, we describe how to use classical reasoning in a disciplined manner in giving classical (yet constructivizable) proofs of sentences of greater complexity than Π ⁰₂ . This direction offers the possibility of applying classical reasoning to more general programming problems.

Supported in part by an NSF graduate fellowship and NSF grant CCR-8616552 and ONR grant N00014-88-K-0409