Hilbert's Axioms - Application

Application

These axioms axiomatize Euclidean solid geometry. Removing four axioms mentioning "plane" in an essential way, namely I.3–6, omitting the last clause of I.7, and modifying III.1 to omit mention of planes, yields an axiomatization of Euclidean plane geometry.

Hilbert's axioms, unlike Tarski's axioms, do not constitute a first-order theory because the axioms V.1–2 cannot be expressed in first-order logic.

The value of Hilbert's Grundlagen was more methodological than substantive or pedagogical. Other major contributions to the axiomatics of geometry were those of Moritz Pasch, Mario Pieri, Oswald Veblen, Edward Vermilye Huntington, Gilbert Robinson, and Henry George Forder. The value of the Grundlagen is its pioneering approach to metamathematical questions, including the use of models to prove axioms independent; and the need to prove the consistency and completeness of an axiom system.

Mathematics in the twentieth century evolved into a network of axiomatic formal systems. This was, in considerable part, influenced by the example Hilbert set in the Grundlagen. A 2003 effort (Meikle and Fleuriot) to formalize the Grundlagen with a computer, though, found that some of Hilbert's proofs appear to rely on diagrams and geometric intuition, and as such revealed some potential ambiguities and omissions in his definitions.