Najwcześniejsza postać formalizmu Hilberta

Abstrakt

The aim of this paper is to describe and analyze the first (1922) of a long series of Hilbert’s works in which he presented the mature version of formalism. His formalism in 1922 can be called mature because it is characterized by an explicit introduction of metamathematics. Hilbert distinguishes several levels of mathematics (not just two, as one may think — formalized mathematics and metamathematics): the level of meaningless arithmetical signs, labelled I-Z in this paper, the level of arithmetic with content (inhaltliche Arithmetik), II-T, which describes signs from level I-Z, the level of formalized mathematics, II-F (Hilbert postulated a full formalization of mathematics), and the level of metamathematics with content, III-MM, which describes signs from level II-F. Hilbert emphasized that the relation of III-MM to II-F is the same as the relation of II-T to I-Z (description, investigation). In this way, he tried to characterize metamathematics. He expected that in III-MM a consistency proof of II-F could be built, which was the aim of Hilbert’s formalism. This paper discusses Hilbert’s first proof of an auxiliary metamathematical theorem. It is indicated that, on level III-MM, Hilbert assumed a part of arithmetic from level II-T and the classical logic. Although in 1922 he did not distinguish explicitly between the finite and infinite mathematics and between the real and ideal mathematics, such a division was implicit in his study. This allows us to assume that already in 1922 Hilbert had an idea of a finitistic consistency proof of infinitistic mathematics, announced a few years later. It appears, therefore, that already in 1922 he had a very clear idea of formalism, which was presented in detail in the middle of the decade. Hilbert was also aware in 1922 that Brouwer’s objections would eventually force him to explain the issue of logical foundations of classical mathematics.