 Moreover, Hilbert’s own treatment of the metalogical issues is somewhat hasty and informal. He experiments with several versions of the concept of “completeness”: one has the sense that he was rapidly breaking new ground, and was not yet certain which concepts would prove the most fruitful. His proof of the completeness of propositional calculus is a mere sketch, and relegated to a footnote; the parallel problem for first-order logic is not even raised as a conjecture. Even more strikingly, when Bernays eventually in 1926 published his Habilitation, he omitted his proof of the completeness theorem because (as he later ruefully said) the result seemed at the time straightforward and unimportant. (For discussion of this point, see Hilbert [LFL]: 229. For readily available general discussions, see Sieg 1999, Zach 1999, and the essays collected in Sieg 2013; for the original documents and detailed analysis, see Hilbert [LFL.)