2025/11/11 by Guo, Hongyu
Mathematics · #Mathematics and Applications #History and Theory of Mathematics #Homotopy and Cohomology in Algebraic Topology
paper · doi:10.48550/arxiv.2511.08494
Tarski's first-order axiom system \mathscrE2 for Euclidean geometry is notable for its completeness and decidability. However, the Pythagorean theorem -- either in its modern algebraic form a2+b2=c2 or in Euclid's Elements -- cannot be directly expressed in \mathscrE2, since neither distance nor area is a primitive notion in the language of \mathscrE2. In this paper, we introduce an alternative axiom system \mathscrEd in a two-sorted language, which takes a two-place distance function d as the only geometric primitive. We also present a conservative extension \mathscrEda of it, which also incorporates a three-place angle function a. The system \mathscrEd has two distinctive features: it is simple (with a single geometric primitive) and it is quantitative. Numerical distance can be directly expressed in this language. The Axiom of Similarity plays a central role in \mathscrEd, effectively killing two birds with one stone: it provides a rigorous foundation for the theory of proportion and similarity, and it implies Euclid's Parallel Postulate (EPP). The Axiom of Similarity can be viewed as a quantitative formulation of EPP. The Pythagorean theorem and other quantitative results from similarity theory can be directly expressed in the languages of \mathscrEd and \mathscrEda, motivating the name Quantitative Euclidean Geometry. The traditional analytic geometry can be united under synthetic geometry in \mathscrEd. Namely, analytic geometry is not treated as a model of \mathscrEd, but rather, its statements can be expressed as first-order formal sentences in the language of \mathscrEd. The system \mathscrEd is shown to be consistent, complete, and decidable. Finally, we extend the theories to hyperbolic geometry and Euclidean geometry in higher dimensions.