Abstract In this paper, we study the metamathematics of consistent arithmetical theories $T$ (containing $\textsf {I}\varSigma _{1}$); we investigate numerical properties based on proof predicates that depend on numerations of the axioms. Numeral Completeness. For every true (in $\mathbb {N}$) sentence $\vec {Q}\vec {x}.\varphi (\vec {x})$, with $\varphi (\vec {x})$ a $\varSigma _{1}(\textsf {I}\varSigma _1)$-formula, there is a numeration $\tau $ of the axioms of $T$ such that $\textsf {I}\varSigma _1\vdash \vec {Q}\vec {x}. \texttt {Pr}_{\tau }(\ulcorner \varphi (\overset {\text{.} }{\vec {x}})\urcorner )$, where $\texttt {Pr}_{\tau }$ is the provability predicate for the numeration $\tau $. Numeral Consistency. If $T$ is consistent, there is a $\varSigma _{1}(\textsf {I}\varSigma _1)$-numeration $\tau $ of the axioms of $\textsf {I}\varSigma _{1}$ such that $\textsf {I}\varSigma _1\vdash \forall\, x. \texttt {Pr}_{\tau }(\ulcorner \neg \textit {Prf}(\ulcorner \perp \urcorner , \overset {\text{.}}{x})\urcorner )$, where $\textit {Prf}(x,y)$ denotes a $\varDelta _{1}(\textsf {I}\varSigma _1)$-definition of ‘$y$ is a $T$-proof of $x$’. Finitist consistency is addressed by generalizing a result of Artemov: Partial finitism. If $T$ is consistent, there is a primitive recursive function $f$ such that, for all $n\in \mathbb {N}$, $f(n)$ is the code of an $\textsf {I}\varSigma _{1}$-proof of $\neg\, \textit{Prf}(\ulcorner \perp \urcorner ,\overline {n})$. These results are not in conflict with Gödel’s Incompleteness Theorems. Rather, they allow to extend their usual interpretation and show a deep connection to reflections in Hilbert’s last papers of 1931.

On June 4, 1925, Hilbert delivered an address to the Westphalian Mathematical Society in Miinster; that was, as a quick calculation will convince you, almost exactly sixty years ago. The address was published in 1926 under the title Über dasUnendlicheand is perhaps Hilbert's most comprehensive presentation of his ideas concerning the finitist justification of classical mathematics and the role his proof theory was to play in it. But what has become of the ambitious program for securing all of mathematics, once and for all? What of proof theory, the very subject Hilbert invented to carry out his program? The Hilbertian ambition reached out too far: in its original form, the program was refuted by Gödel's Incompleteness Theorems. And even allowing more than finitist means in metamathematics, the Hilbertian expectations for proof theory have not been realized: a constructive consistency proof for second-order arithmetic is still out of reach. (And since that theory provides a formal framework for analysis, it was considered by Hilbert and Bernays as decisive for proof theory.) Nevertheless, remarkable progress has been made. Two separate, but complementary directions of research have led to surprising insights: classical analysis can be formally developed in conservative extensions of elementary number theory; relative consistency proofs can be given by constructive means for impredicative parts of second order arithmetic. The mathematical and metamathematical developments have been accompanied by sustained philosophical reflections on the foundations of mathematics. This indicates briefly the main themes of the contributions to the symposium; in my introductory remarks I want to give a very schematic perspective, that is partly historical and partly systematic.