16
$\begingroup$

I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983], which has not been translated to English.

On the other hand, searching through internet I have found an interesting recent paper of Michael Beeson about computer verification of Euclides "Elements" starting from Tarski's axioms. Beeson writes that in order to prove 48 theorems from the first book of Euclides, Coq generated about 200 additinal lemmas that establish some "obvious" facts, which however had to be proved rigorously. Those lemmas can compose Book 0 of "Elements", developping an infrastructure, necessary for correct development of elementary Euclidean geometry. So, I am interested if there is any textbook developing Euclidean geometry starting from 11 Tarski's axioms, which would be recommended for self-study or teaching foundations of geometry in universities.

And what about teaching elementary geometry in secondary schools? Are Tarski's axioms good for this purpose?

Improve this question
$\endgroup$
13
  • $\begingroup$ If you are looking for an approach to the Elements that is amenable to computer verification, Avigad, Mumma and Dean's 'A Formal System for Euclid's Elements' is worth looking at. $\endgroup$
    – provocateur
    Commented Oct 17, 2022 at 22:10
  • $\begingroup$ @provocateur Actually, I am looking for a textbook for teaching foundations of geometry to students, future teachers of mathematics., but starting with Tarski's axioms and developing Euclidean geometry in a rigorous manner (without logical ommissions), which would be accessible to a human. $\endgroup$
    – Taras Banakh
    Commented Oct 18, 2022 at 4:57
  • $\begingroup$ For which students would you recommend such a rigorous and foundational approach — at what level in their studies and with what other backgrounds or plans or interests? $\endgroup$
    – user44143
    Commented Oct 27, 2022 at 2:02
  • 1
    $\begingroup$ Maybe a look at "Part 15 Elementary Geometry" of Metamath "us.metamath.org" could be useful. $\endgroup$
    – Gérard Lang
    Commented Oct 27, 2023 at 10:08
  • 1
    $\begingroup$ @TarasBanakh. Thank You, I liked very much your arxiv reference, and I agree on your point that the fact that NBG is fin itely axiomatizable is interesting. I would have liked to see a point concerning the principle of limitation of size in the paragraph on the Gobal choice axiom ! $\endgroup$
    – Gérard Lang
    Commented Oct 27, 2023 at 10:39

1 Answer 1

Reset to default
2
$\begingroup$

I don't think there are other books than "Metamathematische Methoden in der Geometrie" (SST) for a systematic development of geometry. We have formalized the first part of SST in Coq, this is the library GeoCoq, containing also the formalization of Euclid Book 1 plus many other results about foundations of geometry, and Roland Coghetto ported it to Isabelle. So, a very motivated reader could try to understand the proofs from the machined checked proofs... but those are unfortunately not very readable. Michael Beeson told me once, that someone had the project of translating SST in english, but I don't think it was done.

You may be interested in looking at Franz Rother book.

Anyway, I think the development of geometry in the spirit of Tarski and the book is not suitable teach geometry in secondary schools for several reasons:

  1. In Tarski's geometry lines and circles are implicit.
  2. In SST, one can not easily measure lengths nor angles, there is only congruence at the beginning, and it takes 15 chapters before one can define a field and start doing analytic geometry, some author prefer the metric approach where one assume from the beginning a bijection between the line and the reals.
  3. The goal of SST is to provide a systematic development of geometry with minimal assumptions about the use of the parallel postulate and continuity. The first chapters in SST prove results that are valid in both Euclidean and Hyperbolic geometry. This has an impact on some definitions and proofs, and makes them more complicated. Here are some examples:
  • SST proves the existence of the midpoint of a segment only in Chapter 7! because they want to show that it can be done without circle-circle continuity axiom.
  • The definition of a point P being inside an angle ABC is chosen in such a way that it is also valid in hyperbolic geometry: "We say that P is inside angle $ABC$, if there is a point $X$ on segment $AC$ such that P belongs to ray $BX$.", whereas one could choose a simpler definition in Euclidean Geometry.
Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the answer. In fact, learning that there is no such a book in Foundations of Geometry, I am writing it myself and this is rather difficult task, I should say. At the moment I have almost 100 pages for the chapter in affine and projective geometry, where the main aim is to derive the algebraic structure of an R-module over a division ring $R$ from the geometric structure of a Desarguesian affine space. In any case, this is a very interesting project, in spite of the fact that it is rather old-fashioned, as seen from mainly non-existing answers to my geometric questions at MO. $\endgroup$
    – Taras Banakh
    Commented Oct 27, 2023 at 9:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .