The Simplicity Degree of Tarski’s Euclidean Geometry of Ruler and Dividers is 5

We present an axiom system for the plane Euclidean geometry of ruler and dividers constructions, expressed in Tarski’s language, with points as the only variables and with the predicates of betweenness and equidistance as the only primitive notions. All axioms are statements about at most 5 points, and it is known that no axiom system with all axioms statements about at most 4 points exists in that language, so the axiom system presented here can be called the simplest possible one. This corrects an error in Pambuccian (Math Chronicle 18:63–74, 1989) and shows that the Pasch axiom can be replaced by three statements, a 3-variable one, a 4-variable one, and a 5-variable one in the context of plane Euclidean geometry over Pythagorean ordered fields. Viewed from the vantage point of the weak elementary Euclidean Pasch-free geometry, the Pasch axiom turns out to be equivalent to both a universal 5-variable sentence and to a positive 5-variable sentence.