Open AccessA Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry
Author(s) -
Gabriel Braun,
Julien Narboux
Publication year - 2016
Publication title -
journal of automated reasoning
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.497
H-Index - 56
eISSN - 1573-0670
pISSN - 0168-7433
DOI - 10.1007/s10817-016-9374-4
Subject(s) - foundations of geometry , mathematical proof , absolute geometry , axiom , mathematics , non euclidean geometry , euclidean geometry , automated theorem proving , convex geometry , geometry , algebra over a field , algebraic geometry , calculus (dental) , pure mathematics , projective geometry , algorithm , regular polygon , dentistry , convex analysis , convex optimization , medicine , convex set
International audienceIn 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 detailed by Schwabhäuser , Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which 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
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom