 If that is correct, then Hilbert’s decisive step in the 1917/18 lectures was not the isolation of first-order logic—i.e., not step \((\alpha)\). That was a comparatively insignificant matter. That step had already been taken explicitly by Peirce, and tacitly by Weyl and Löwenheim. Hilbert did not treat it as important, and appears to have viewed it primarily as an expository device, a means of simplifying the presentation of the logic of Principia Mathematica. The important step in 1917 was rather the introduction of techniques of metamathematics, and the explicit posing of questions of completeness and consistency and decidability. To pose these questions for systems of logic was an enormous conceptual leap, and Hilbert understood it as such. His own first attempts, made in his 1905 Heidelberg address, had collapsed under the criticisms of Poincaré, and he had struggled to find a satisfactory formulation. And even after he had introduced his metalogical distinctions in his papers of the 1920s, logicians of the caliber of Russell and Brouwer and Ramsey had difficulty in understanding what he was attempting to do. This development was in 1917 anything but inevitable: and without the introduction of the metalogical techniques the history of logic and proof theory in the 1920s and 1930s would have looked very different. Would the Gödel theorems ever have been conceived? Would the work of Löwenheim or Skolem or Zermelo independently have led to an investigation of the metalogical properties of first-order logic? One can in retrospect imagine an alternative path to the technical results \((\beta)\), but there is no reason to suppose that they were fated to emerge either when they did, or as they did.