# Michael Beeson's Research

-->
Foundations of Geometry

# Introduction to the Foundations of Geometry

This subject involves writing down axioms for plane (or solid) geometry, and studying the consequences of those axioms. Before one gets to the axioms, one has to choose a language. That means choosing the following things:

1. the primitive ``sorts'', such as point, line, and plane, over which variables can range
2. the primitive relations, such as incidence (a point lies on a line), betweenness B(x, y, z) ( y is between x and z), and equidistance E( a,b,c,d) (segment ab is congruent to segment cd )
3. any constant or functions symbols one may wish to include, such as three constants for three non-collinear points, or a function symbol for the intersection point of two lines, etc.

There are a great many possible choices of a language for geometry. Two that have received the most study are due to Hilbert (1899) and Tarski (1926), respectively. 1899 is the date of publication of Hilbert's famous book, Foundations of Geometry. 1926 is the date when Tarski lectured on his axiom system, although for various reasons it did not appear in print until much later.

Hilbert's language has the three sorts mentioned above, and his betweenness relation is strict , that is, B( x,y,z ) implies that x, y, z are distinct points. In 1899, the modern distinction between first-order and second-order languages was not clearly understood, even by Hilbert; he clearly states that there are three fundamental sorts (so a line is not just a set of points), but then he defines rays and segments as sets of points, and angles as pairs of rays. Nowadays, if we have variables ranging over sets of objects, we call that a second-order language; and if we need sets of those sets, that is called third-order. Hilbert, taken literally, is using a third-order language, since angles are sets of rays, and rays are sets of points. It is, however, not too difficult to reformulate Hilbert using a first-order language with three sorts (point, line, and plane) and two incidence relations (point incident on line, and point incident on plane).

Tarski has only one sort: points. That means that in Tarski geometry, lines are represented as pairs of points, and angles are represented by triples of points. Tarski used a clever trick, called the five-segment axiom, to express the SAS triangle congruence principle without explicitly mentioning angles. The beauty of Tarski's axiom system is the austerity of the language and axioms. Fewer than a dozen axioms are required to axiomatize geometry, and they are all expressed in the primitives of the language, without needing to introduce abbreviations for defined concepts. A number of very basic properties, that you might think would be axioms, can actually be proved. In particular, the interpretations of Hilbert's axioms, expressed in this more parsimonious language, can be proved. I have written out the details because one person wanted to see them; perhaps there will be others interested.

If you would like to study these things, here are the places to begin:

1. Hilbert's book, Foundations of Geometry (1899). There are numerous editions available, including a Kindle edition for \$1.99.
2. A famous letter of Givant and Tarski to Schwabhäuser. This letter lists and explains Tarski's axioms, and gives some history of the development of the axiom system, as some of the original 1926 axioms were proved to be consequences of the others. Annoyingly, it is illegal for me to link you to a pdf of that letter. You will have to get it through your university's library. The reference is Tarski's System of Geometry, by Givant and Tarski, in the Bulletin of Symbolic Logic, Volume 5, Number 2, June 1999. There is also a brief introduction to Tarski's axioms (using pictures, not symbols) in the first part of Proof and Computation in Geometry.
3. Wanda Szmielew developed geometry carefully from Tarski's axioms in her 1965 lecture notes. These notes eventually became incorporated in the book Metamathematische Methoden in der Geometrie", by Schwabhäuser, Szmielew, and Tarski (SST for short). That book appeared only in 1983, after Szmielew's death, and is in German. You should try to read it, even if your German is weak, because it is mostly symbols anyway. It has recently been reprinted with a new foreword by me (Michael Beeson). You can read the foreword (in English) here.
4. The textbook by Greenberg, and the textbook by Hartshorne, both develop geometry on the basis of Hilbert's axioms. You can also learn about non-Euclidean geometry from these textbooks.

I have worked on two different projects in the foundations of geometry:

1. Constructive geometry.

This is geometry with intuitionistic logic. If you don't know what that means, think of it as geometry in which, when you prove a point exists (depending on some given points), you must show how to construct it by ruler and compass, without using arguments by cases, so that given approximations to the original points, you can construct an approximation to the final point. Since many of Hilbert's and Tarski's original proofs did use definition by cases, it is not obvious that on the basis of suitable axioms, one can actually define multiplication and addition geometrically, as Descartes and Hilbert did. Some new constructions are necessary.

The word "constructive" in "constructive geometry" might mean intuitionistic logic, or it might refer to ruler and compass constructions. In my first paper on the subject, Constructive Geometry, I showed that there is a connection: Things you can prove to exist in constructive geometry can be constructed with ruler and compass.

Within constructive geometry, different versions of the parallel axiom that are provably equivalent (using non-constructive, or "classical" logic) are no longer equivalent. Using certain metamathematical techniques, I was able to show that they really are not equivalent in constructive geometry. I reported on this work in my 2012 paper, Logic of Ruler and Compass Constructions.

In January 2014, I completed two papers presenting all my work on constructive geometry. New readers should ignore the early conference presentations mentioned above, and just read these two papers:

A constructive version of Tarski's geometry, accepted by Annals of Pure and Applied Logic, to appear in 2015.

2. Tarski Formalization in Otter.

This project, on which I collaborated with Larry Wos, involves using the theorem-prover Otter to find proofs of all the theorems in the book SST mentioned above. In summer 2012, we got up to Satz 9.6, which is an important theorem due to Gupta. Just getting that far, we solved four challenge problems posed 21 years ago in Art Quaife's book. Later, we went far enough (Chapter 12) to verify all of Hilbert's axioms, and presented our work at a conference in Vienna. In 2015 we extended this work, finding several proofs of long theorems by methods that did not involve knowing the steps of the book proof in advance, and mechanizing the generation of the input files involved. We prepared a paper for the . There are many web pages about this project on this website, including all the input files and resulting proofs, the PHP tools we used for generating and testing those files, and explanations that are not included in the journal paper. See the top page at Tarski Formalization Project. You can also find links to our papers under the Publications menu item above.