Hilbert's programme aimed for finitist consistency proofs of formalized mathematical theories. Gödel's first incompleteness theorem, stating that for any consistent formal theory containing basic arithmetic there are true statements that are neither provable nor refutable in it doesn't have an immediate impact on this programme, as long as it concentrates on consistency. Gödel's \textit{second} incompleteness theorem on the other hand implies that the consistency programme cannot be carried out in its intended meaning. Given the specific way Gödel proved his first theorem, the second theorem can `morally speaking' be regarded a direct corollary of the first (although its formal proof requires the highly technical verification of the Hilbert-Bernays derivability conditions carried out by Bernays in \textit{Grundlagen der Mathematik II}).

In this talk we report on some anticipations of Gödel 1 in the Hilbert school and the consequences which one can draw regarding the importance of Gödel's achievement. In particular, we show that it is not the mere exhibition of an independent sentence, but the implications of Gödel's specific proof method that gives it its great foundational significance.

First, ``in a letter of 3 August 1966 to Constance Reid [Paul] Bernays testified that `some time before' he learned of Gödel's theorems he had himself become `doubtful ... about the completeness of the formal systems' and had `uttered [his doubts] to Hilbert.'\,'' (Dawson, Logical Dilemmas, AK Peters, 1997, p. 72)

This anticipation can be placed in the context of attempts in the Hilbert school to formalize the paradoxes in formal languages. While there seems to have been no such formalization known for a first-order theory (as was later given by Gödel), for higher-order theories, Hilbert and Ackermann give a rather clear approach towards a possible incompleteness result in the seminal textbook \textit{Grundzüge der theoretischen Logik} (Springer, 1928, p. 115). It is obvious that the approaches were never fully worked out, nor was the significance of the potential incompleteness fully understood.

In fact, Gödel's \textit{proof} of the first incompleteness theorem has some specific consequences which don't come with a mere independent sentence. Besides the second incompleteness theorem being (essentially) a corollary, we highlight two important such consequences. First, the proof shows that the first incompleteness theorem is generic in the sense that one cannot resolve the incompleteness by simply adding more axioms (as long as the axiom system stays recursive). Second, it implies the incompleteness of second- and any higher-order logic.

Another objective besides consistency, versions of which have taken on great importance in later developments---exemplified by Kreisel, Feferman, Sieg, Simpson and others---is the goal of \textit{conservativity}, i.e., the provable provability of all elementarily statable theorems by strictly elementary means (``elimination of ideal elements''). While this was not the original concern of Hilbert, it was added to the core objectives in the consolidating phase of the mid to late twenties. It has been noticed, e.g., by Smoryński, that already the first incompleteness theorem shows that the hope for conservativity fails. But here, too, it is the generic version implied by Gödel's proof method that fatally undermines the conservativity programme, rather than the mere existence of an unprovable sentence.

\bigskip

This work is supported by the Udo Keller-Stiftung and makes part of the work elaborated by the second author within an \textit{Opus Magnum} grant of the VolkswagenStiftung on \textit{Die Hilbertsche Beweistheorie}. The second author also received support by national funds through the FCT – Fundação para a Ciência e a Tecnologia, I.P., under the scope of the projects UID/00297/2025 (https://doi.org/10.54499/UID/00297/2025) and UID/PRR/00297/2025 (https://doi.org/10.54499/UID/PRR/00297/2025) (Center for Mathematics and Applications – NOVA Math).

In 1888, Richard Dedekind laid the foundation of universal set theory.
The first to accept it was Bertrand Russell in 1903, and he managed to reconcile the seemingly conflicting method of proof by constructing a diagonal object, invented by Georg Cantor in 1890, with the necessarily existing universal set of universal set theory.
Unfortunately, Dedekind's as well as Russell's demanding concepts were not understood by the mathematicians, neither in Jena (in 1902, Frege) nor in Göttingen (since 1904, Hilbert).
When Paul Finsler reinstated and developed universal set theory further (since 1926), mathematicians were unable to understand him (Göttingen's mathematicians were unwilling), and consequently, it sank into oblivion; until today.