First-Order Axiom Systems $\mathscr{E}_{d}$ and $\mathscr{E}_{da}$ Extending Tarski's $\mathscr{E}_{2}$ with Distance and Angle Function Symbols for Quantitative Euclidean Geometry

Abstract

Tarski's first-order axiom system $\mathscr{E}_{2}$ for Euclidean geometry is notable for its completeness and decidability. However, the Pythagorean theorem -- either in its modern algebraic form $a^{2}+b^{2}=c^{2}$ or in Euclid's Elements -- cannot be directly expressed in $\mathscr{E}_{2}$, since neither distance nor area is a primitive notion in the language of $\mathscr{E}_{2}$. In this paper, we introduce an alternative axiom system $\mathscr{E}_{d}$ in a two-sorted language, which takes a two-place distance function $d$ as the only geometric primitive. We also present a conservative extension $\mathscr{E}_{da}$ of it, which also incorporates a three-place angle function $a$. The system $\mathscr{E}_{d}$ 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 $\mathscr{E}_{d}$, 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 $\mathscr{E}_{d}$ and $\mathscr{E}_{da}$, motivating the name Quantitative Euclidean Geometry. The traditional analytic geometry can be united under synthetic geometry in $\mathscr{E}_{d}$. Namely, analytic geometry is not treated as a model of $\mathscr{E}_{d}$, but rather, its statements can be expressed as first-order formal sentences in the language of $\mathscr{E}_{d}$. The system $\mathscr{E}_{d}$ is shown to be consistent, complete, and decidable. Finally, we extend the theories to hyperbolic geometry and Euclidean geometry in higher dimensions.