# A textbook on foundations of geometry in spirit of Tarski

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?

• 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. Commented Oct 17, 2022 at 22:10
• @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. Commented Oct 18, 2022 at 4:57
• 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?
– user44143
Commented Oct 27, 2022 at 2:02
• Maybe a look at "Part 15 Elementary Geometry" of Metamath "us.metamath.org" could be useful. Commented Oct 27, 2023 at 10:08
• @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 ! Commented Oct 27, 2023 at 10:39

• 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.
• 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. Commented Oct 27, 2023 at 9:10