Relative consistency and accessible domains (Q1202497)

The goal of Hilbert's program --- to give consistency proofs for analysis and set theory within finitist mathematics --- is unattainable; the program is dead. The mathematical instrument, however, that Hilbert invented for attaining his programmatic aim is remarkably well: proof theory has obtained important results and pursues fascinating logical questions; its concepts and techniques are fundamental for the mechanical search and transformation of proofs; and I believe that it will contribute to the solution of classical mathematical problems. Nevertheless, we may ask ourselves whether the results of proof theory are significant for the foundational concerns that motivated Hilbert's program and, more generally, for a reflective examination of the nature of mathematics. The results I alluded to establish the consistency of classical theories relative to constructive ones and give in particular a constructive foundation to mathematical analysis. They have been obtained in the pursuit of a reductive program that provides a coherent scheme for metamathematical work and is best interpreted as a far-reaching generalization of Hilbert's program. For philosophers these definite mathematical results (should) present a profound challenge. To take it on means to explicate the reductionist point of constructive relative consistency proofs; the latter are to secure, after all, classical theories on the basis of more elementary, more evident ones. I take steps towards analyzing the precise character of such implicitly epistemological reductions and thus towards answering the narrow part of the above question.