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
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914151396278272 |
|---|---|
| author | Guo, Hongyu |
| author_facet | Guo, Hongyu |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_08494 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | 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 Guo, Hongyu Logic Logic in Computer Science Metric Geometry 03B30, 03C35, 51M05, 51M10 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. |
| title | 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 |
| topic | Logic Logic in Computer Science Metric Geometry 03B30, 03C35, 51M05, 51M10 |
| url | https://arxiv.org/abs/2511.08494 |