Hilbert's program relativized; Proof-theoretical and foundational reductions

Abstract

In the Symposium on Hilbert's Program to which the following was contributed, I was asked to talk about the metamathematical aspects of Hilbert's Program (H.P.), while the other two speakers (Simpson and Prawitz) were to deal with the mathematical and philosophical aspects respectively. However, more so than for other foundational schemes, these three aspects of H.P., both as originally conceived and in its subsequent developments, are intimately linked. Here I shall survey a body of proof-theoretical results stemming from H.P., but organized in a way that is closely tied to various reductive foundational aims, albeit going beyond those advanced by Hilbert. I believe this view of reductive proof-theory (not original with me) helps one to better understand what has been achieved thereby than other, more familiar accounts.