this issue
next article in this issue

Document Details :

Title: The Finite and the Infinite
Subtitle: On Hilbert's Formalist Approach before and after Gödel's Incompleteness Theorems
Author(s): SCHIRN, Matthias
Journal: Logique et Analyse
Volume: 245    Date: 2019   
Pages: 1-34
DOI: 10.2143/LEA.245.0.3285703

Abstract :
In this essay, I discuss formalist and finitist aspects of Hilbert’s proof-theoretic programme in the 1920s and 1930s. I begin by pointing out some difficulties arising from his construction of intuitive number theory in his first paper on metamathematics in the 1920s and by characterizing the nature of his metamathematics. In what follows, I argue that Hilbert’s paradigm of a transfinite axiom as well as the other 'ordinary' transfinite axioms derivable from it fail to supply any formal explication of the term 'infinite' or 'transfinite'. On the one hand, Hilbert regards both the mathematical and the logical signs as detached from all meaning once the process of formalization of contentual mathematics has been completely carried out. On the other hand, there are several places where he characterizes the finitary or real sentences of the language of formalized arithmetic, in contrast to its transfinite or ideal sentences, expressly as meaningful. I make a proposal to explain why for Hilbert it might still be of interest to be able to rely on meaningful sentences in the language of formalized arithmetic. In section 5, I critically discuss several aspects in Hilbert and Bernays’s extension of the finitist point of view in the second volume of Foundations of Mathematics (1939). In section 6, I argue that by appreciating the distinctive character of the notion of an 'approximative' consistency proof we can make good sense of the nature of the consistency proofs that Hilbert outlines both in his classical papers on proof theory in the 1920s and in the first volume of Foundations of Mathematics (1934). I further argue that a weak version of Hilbert’s programme is compatible with Gödel’s second incompleteness theorem by using only what are clearly natural provability predicates.

Download article