A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

详细信息    查看全文

• 作者：Gabriel Braun ; Julien Narboux
• 关键词：Formalization ; Formal proof ; Geometry ; Coq ; Pappus ; Tarski’s axioms
• 刊名：Journal of Automated Reasoning
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：58
• 期：2
• 页码：209-230
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation;
• 出版者：Springer Netherlands
• ISSN：1573-0670
• 卷排序：58

文摘

In this paper, we report on the formalization of a synthetic proof of Pappus’ theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry, which has been described in detail by Schwabhäuser, Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps that are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski’s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry, which will allow us to provide a connection between analytic and synthetic geometry.