This paper is devoted to the general question, which assertions φ have the property,

if φ is provable classically, then φ is

(*) provable constructively.

More generally, we consider the question, what is the “constructive content” of a given classical proof? Our aim is to formulate rules in a form applicable to mathematical practice. Often a mathematician has the feeling that there will be no difficulty constructivizing a certain proof, only a number of routine details; although it can be quite laborious to set them all out. We believe that most such situations will come quite easily under the scope of the rules given here; the metamathematical machinery will then take care of the details.

This basic idea is not new; it has been discussed by Gödel and by Kreisel. Kreisel's investigations [Kr] were based on Herbrand's theorem; in unpublished memoranda he has also used Gödel's methods on some examples. These methods of Gödel (the double-negation and Dialectica interpretations) lie at the root of our work here. Previous work, however, has been limited to traditional formal systems of number theory and analysis. It is only recently that formal systems adequate to formalize constructive mathematics as a whole have been developed. Thus, for the first time we are in a position to formulate logical theorems which are easily applicable to mathematical practice. It is this program which we here carry out.

Now that the work has been placed in some historical context, let us return to the main question: which φ have the property (*)? Upon first considering the problem, one might guess that any φ which makes no existential assertions (including disjunctions) should have the property (*).