 As observed earlier, Hilbert attempted to overcome the incompleteness of first-order arithmetic by introducing as axioms \(\Pi^0_1\)-statements all of whose instances had been finitistically proved (Hilbert 1931a). In a way he modified the concept of a “formal” theory by invoking finitist provability. Bernays, in his letter to Gödel of January 18, 1931 (Gödel 2003: 86–88), proposed a rule of a more general form. He indicated also that it would allow the elimination of the induction principle—in exchange for dealing with infinite proofs.