1993]. What rests on what? The proof-theoretic analysis of mathematics

Whenever a subject is organized systematically for expository or foundational purposes (or both), one must deal with the question: What rests on what? The way in which this is answered in the case of mathematics depends on whether one is considering it informally or formally, i.e. from the point of view of the mathematician or the logician, respectively. The latter usually deals with the question in terms of what specifically follows from what in a given logical/axiomatic setup. Proof theory provides technical notions and results which– when successful–serve to give a more global kind of answer to this question, in terms of reduction of one such system to another; moreover, these results provide a technical bridge from mathematics to philosophy. The purpose of this paper is to give a picture of what is accomplished in these various respects by reductive proof theory. My own approach to that subject is outlined in §1, along with a brief comparison with a more standard account. This is then followed in §2 by a description of some technical results that illustrate the general approach. The paper concludes in §3 with a discussion of how reductive proof theory mediates between mathematics and philosophy. A more technical and comprehensive exposition of the material in §§1-2 has previously been given in my paper [Feferman 1988]