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

TL;DR

The paper introduces two first-order axiom systems, $\mathscr{E}_{d}$ and its conservative extension $\mathscr{E}_{da}$, to formalize quantitative Euclidean geometry with a single distance primitive $d$ and, in $\mathscr{E}_{da}$, an angle primitive $a$. Central to the framework is the Axiom of Similarity, which yields a robust theory of proportion and implies Euclid's Parallel Postulate, enabling direct expression of the Pythagorean relation as $d^2(\mathbf{ab}) + d^2(\mathbf{ac}) = d^2(\mathbf{bc})$ within the language. The authors prove consistency, completeness, and decidability for $\mathscr{E}_{d}$, establish mutual interpretability with Tarski's $\mathscr{E}_{2}$ (with parameters), and present a conservative extension $\mathscr{E}_{da}$ that handles angles; they also sketch extensions to hyperbolic geometry and higher dimensions, thereby unifying analytic geometry within a synthetic, first-order framework. This work advances a compact, fully formal foundation for quantitative geometry, bridging traditional analytic and synthetic approaches while avoiding set theory.

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.

Figures (32)

• Figure S1: Euclid: the Pythagorean theorem---The notion of area is used to state the theorem.
• Figure S2: Euclid: Fundamental Theorem of Proportion---The notion of area is not used to state the theorem but used in the proof.
• Figure S3: Descartes and Hilbert: The definition of the product of two segments is a third segment.
• Figure S4: Axiom of similarity.
• Figure S5: The dimension is at least 2.

Theorems & Definitions (23)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Definition 7
• Definition 8
• Theorem 1
• Theorem 2