 But despite these constructive tendencies, many logicians of the 1920s (including Hilbert) continued to regard higher-order type theory, and not its first-order fragment, as the appropriate logic for investigations in the foundations of mathematics. The ultimate hope was to provide a consistency proof for the whole of classical mathematics (including set theory). But, in the meanwhile, researchers still were somewhat unclear about certain basic distinctions. Hilbert at times fails to observe the distinction between a first-order axiom-schema and a second-order axiom; Brouwer’s intuitionism is sometimes identified with “finitism”; the relationships between completeness (in several senses), categoricity (also in several senses), and first-order and higher-order logic were not yet understood. Indeed, Gregory Moore points out that even Gödel, in his 1929 proof of the completeness of first-order logic, did not fully understand the notion of categoricity and its relationship to second-order logic (Moore 1988: 125).