A Case Study in Formalizing Hilbert's Foundations of Geometry in Coq: Establishing Key Properties of Lines in Hilbert's Axiom System
- Resource Type
- Conference
- Authors
- Zhang, Qimeng; Yu, Wensheng
- Source
- 2023 China Automation Congress (CAC) Automation Congress (CAC), 2023 China. :1926-1930 Nov, 2023
- Subject
- Aerospace
Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Power, Energy and Industry Applications
Robotics and Control Systems
Signal Processing and Analysis
Transportation
Geometry
Automation
Buildings
Reliability theory
Topology
History
Foundations of Geometry
Axiom System
Formalization
Coq
- Language
- ISSN
- 2688-0938
Hilbert's “Foundations of Geometry” represents a pivotal milestone in the history of mathematics. The Theorem 8 in “Foundations of Geometry” plays a crucial role by establishing a fundamental property of lines in the plane: the partitioning of the plane into two distinct regions by a line. This property is directly or indirectly utilized in numerous theorem proofs and provides a definition for determining two points either share the same side or occupy opposite sides of a specified line. This definition is essential to the description of Hilbert's axioms. Additionally, this theorem can also be regarded as a special form of the Jordan curve theorem in Topology. This paper outlines the process of formally verifying Hilbert's Theorem 8 using Coq, a reliable and rigorous proof assistant. Departing from Hilbert's original definition, we propose an alternative description of two points lying on a common side of a line and rigorously establish its equivalence to the Hilbert's definition. Building upon this equivalent definition, we completely provide a rigorous demonstration establishing the validity of the theorem. The introduction of this alternative definition enhances the conciseness of our formalization. Our work not only emphasizes the importance of Theorem 8 within Hilbert's axiom system but also lays the foundation for further exploration and verification of propositions derived from this system.