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?’