  As to Hilbert's geometry, its attempted formalization fell short of the ideal to which it gave birth. Hilbert found a much more important field to which his “metamathematics” was to be applied, namely arithmetic and analysis. The groundwork was a study of the four foundational problems in axiomatic formulations of pure logic. Propositional logic was thus formalized, found to be consistent and complete, and decidable. The first results about predicate logic are from 1915, when Leopold Löwenheim gave his version of what later became the Löwenheim-Skolem theorem for predicate logic (see the entry on classical logic). He also solved special cases of the decision problem. This development was independent of the Frege-Russell tradition, and was instead based on the algebraic approach to logic of Ernst Schröder. Around 1920, the “Hilbert style” axiomatic approach, as it is often called, was known to everyone and dominated the logical scene; the algebraic approach merged almost without notice with lattice theory. By 1928, in Hilbert and Ackermann's Grundzüge der theoretischen Logik, an axiomatic formal system for predicate logic was presented, together with the problem of its completeness. The latter was solved by Gödel in 1929, published a year later (Gödel 1930). The fourth foundational problem, the decision problem for predicate logic, was shown to have a negative solution in a short paper by Church in 1936 as a corollary to Gödel's incompleteness theorem.