ABSTRACT
FOUNDATIONAL AND MATHEMATICAL USES OF HIGHER TYPES
§1. Introduction. A central theme of proof theory is expressed by the following question:
‘What parts of ordinary mathematics (in particular of analysis) can be carried out in certain restricted formal systems?’