  A philosophically more satisfactory continuation of Hilbert’s Program in proof theoretic terms has been suggested by Kreisel  (1983;  1968)  and Feferman  (Feferman, 1988;  Feferman, 1993a).  This work proceeds from a wider conception of Hilbert’s Program as an attempt to justify ideal mathematics by restricted means. In this conception, the aim of Hilbert’s proof theory was to show that, at least as far as a certain class of real propositions is concerned, ideal mathematics does not go beyond real mathematics. A finitary consistency proof of the kind envisaged by Hilbert would have accomplished this: if ideal mathematics proves a real proposition, then this proposition is already provable by real (i.e., finitary) methods. In a sense this reduces ideal mathematics to real mathematics. A proof-theoretic reduction of a theory \(T\) to a theory \(S\) shows that, as far as a certain class of propositions is concerned, if \(T\) proves a proposition, then \(S\) proves it too, and the proof of this fact is itself finitary. Hilbert’s proof theoretic program can then be seen to be a search for a proof theoretic reduction of all of mathematics to finitary mathematics; in a relativized program one looks for reductions of theories weaker than all of classical mathematics to theories often stronger than finitary mathematics. Proof theorists have obtained a number of such results, including reductions of theories which on their face require a significant amount of ideal mathematics for their justification (e.g., subsystems of analysis) to finitary systems.  (Feferman, 1993b)  has used such results in combination with other results that show that most, if not all, of scientifically applicable mathematics can be carried out in systems for which such reductions are available to argue against the  indispensability argument  in the philosophy of mathematics. The philosophical significance of such proof theoretic reductions is currently the subject of debate  (Hofweber, 2000;  Feferman, 2000).