Return to search

Ordered geometry in Hilbert's Grundlagen der Geometrie

The Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are five groups of axioms, each focused on a logical feature of Euclidean geometry. The first two groups give us ordered geometry, a highly limited setting where there is no talk of measure or angle. From these, we mechanically verify the Polygonal Jordan Curve Theorem, a result of much generality given the setting, and subtle enough to warrant a full verification. Along the way, we describe and implement a general-purpose algebraic language for proof search, which we use to automate arguments from the first axiom group. We then follow Hilbert through the preliminary definitions and theorems that lead up to his statement of the Polygonal Jordan Curve Theorem. These, once formalised and verified, give us a final piece of automation. Suitably armed, we can then tackle the main theorem.

Identiferoai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:691140
Date January 2015
CreatorsScott, Phil
ContributorsFleuriot, Jacques ; Smaill, Alan
PublisherUniversity of Edinburgh
Source SetsEthos UK
Detected LanguageEnglish
TypeElectronic Thesis or Dissertation
Sourcehttp://hdl.handle.net/1842/15948

Page generated in 0.0015 seconds