Matthias Schirn (LMU) gives a talk at the MCMP Colloquium (20 November, 2013) titled "Hilbert's metamathematics, finitist consistency proofs and the concept of infinity". Abstract: The main focus of my talk is on a critical analysis of some aspects of Hilbert’s proof-theoretic programme in the 1920s. During this period, Hilbert developed his metamathematics or proof theory to defend classical mathematics by carrying out, in a purely finitist fashion, consistency proofs for formalized mathematical theories T. The key idea underlying metamathematical proofs was to establish the consistency of T by means of weaker, but at the same time more reliable methods than those that could be formalized in T. It was in the light of Gödel’s incompleteness theorems that finitist metamathematics as designed by Hilbert and his collaborators turned out to be too weak to lay the logical foundations for a significant part of classical mathematics. In the 1930s, Hilbert responded to Gödel’s challenge by extending his original finitist point of view. The extension was guided by two central, though possibly conflicting ideas: firstly, to make sure that it preserved the quintessence of finitist metamathematics; secondly, to carry out, within the extended proof-theoretic bounds, a finitist consistency proof for a large part of mathematics, in particular for second-order arithmetic. I begin by briefly characterizing Hilbert’s metamathematics in the 1920s, with particular emphasis on his conception of finitist consistency proofs for formalized mathematical theories T. In subsequent sections, I try to shed light on some difficulties to which his project gives rise. One difficulty that I discuss is the fact, widely ignored in the pertinent literature, that Hilbert’s language of finitist metamathematics fails to supply the conceptual resources for formulating a consistency statement qua unbounded quantification. Another difficulty emerges from Hilbert’s tacit assumptions of infinity in metamathematics. On the way, I shall comment on the relationship between finitism and intuitionism, on Gentzen’s “finitist” consistency proof for number theory (1936) and on W. W. Tait’s objection to an interpretation of Hilbert’s finitism by Niebergall and Schirn. I conclude with remarks on the extension of the finitist point of view in Hilbert and Bernays’s monumental work Grundlagen der Mathematik (vol 1, 1934; vol. 2, 1939) and philosophical remarks on consistency proofs and the notion of soundness.