On September 7, 1930, Gödel announced at a conference that ‘one can give examples of propositions that, while contentually true, are unprovable in the formal system of classical mathematics’. On October 23, he cited both the incompleteness of the formal system of Principia and the unprovability of the consistency of the system by methods formalizable within it. Gödel also went as far as to deny expressly that his theorems killed off Hilbert's programme. Three doubts were salient. First, Gödel's theorems apply only to theories that are formal, in the sense that ‘reasoning in them, in principle, can be completely replaced by mechanical devices’. Second, in order to demonstrate that the consistency of a formal system cannot be proved by methods formalizable in the system itself, it was necessary to appeal to certain features of the method of formalization: a consistency proof formalizable by methods not sharing these features therefore remained a possibility. Third, what Hilbert had demanded was a finitary proof of consistency Gödel's theorem does not rule out unless all finitary methods are formalizable in the system in question. Eventually, Gödel overcame his doubts on all three counts, but to understand why, his reservations must be investigated in detail.
Keywords: Hilbert, Gödel, formal theories, outer consistency, axiomatic formalism