quality:correction, information:classification, linguistic:translation, stylistic:tone
Discussion

According to Tarski and Givant (1999: 192-93), none of the above axioms are fundamentally new. The first four axioms establish some elementary properties of the two primitive relations. For instance, Reflexivity and Transitivity of Congruence establish that congruence is an equivalence relation over line segments. The Identity of Congruence and of Betweenness govern the trivial case when those relations are applied to nondistinct points. The theorem xy ≡ zz ↔ x = y ↔ Bxyx extends these Identity axioms.

A number of other properties of Betweenness are derivable as theorems including:

The last two properties totally order the points making up a line segment.

The Upper and Lower Dimension axioms together require that any model of these axioms have dimension 2, i.e. that we are axiomatizing the Euclidean plane. Suitable changes in these axioms yield axiom sets for Euclidean geometry for dimensions 0, 1, and greater than 2 (Tarski and Givant 1999: Axioms 8, 8, 9, 9, 9). Note that solid geometry requires no new axioms, unlike the case with Hilbert's axioms. Moreover, Lower Dimension for n dimensions is simply the negation of Upper Dimension for n - 1 dimensions.

When the number of dimensions is greater than 1, Betweenness can be defined in terms of congruence (Tarski and Givant, 1999). First define the relation "≤" (where a b ≤ c d {\displaystyle ab\leq cd} is interpreted "the length of line segment a b {\displaystyle ab} is less than or equal to the length of line segment c d {\displaystyle cd} "):

In the case of two dimensions, the intuition is as follows: For any line segment xy, consider the possible range of lengths of xv, where v is any point on the perpendicular bisector of xy. It is apparent that while there is no upper bound to the length of xv, there is a lower bound, which occurs when v is the midpoint of xy. So if xy is shorter than or equal to zu, then the range of possible lengths of xv will be a superset of the range of possible lengths of zw, where w is any point on the perpendicular bisector of zu.

Betweenness can then be defined by using the intuition that the shortest distance between any two points is a straight line:

The Axiom Schema of Continuity assures that the ordering of points on a line is complete (with respect to first-order definable properties). As was pointed out by Tarski, this first-order axiom schema may be replaced by a more powerful second-order Axiom of Continuity if one allows for variables to refer to arbitrary sets of points. The resulting second-order system is equivalent to Hilbert's set of axioms. (Tarski and Givant 1999)

The Axioms of Pasch and Euclid are well known. The Segment Construction axiom makes measurement and the Cartesian coordinate system possible—simply assign the length 1 to some arbitrary non-empty line segment. Indeed, it is shown in (Schwabhäuser 1983) that by specifying two distinguished points on a line, called 0 and 1, we can define an addition, multiplication and ordering, turning the set of points on that line into a real-closed ordered field. We can then introduce coordinates from this field, showing that every model of Tarski's axioms is isomorphic to the two-dimensional plane over some real-closed ordered field.

The standard geometric notions of parallelism and intersection of lines (where lines are represented by two distinct points on them), right angles, congruence of angles, similarity of triangles, tangency of lines and circles (represented by a center point and a radius) can all be defined in Tarski's system.

Let wff stand for a well-formed formula (or syntactically correct first-order formula) in Tarski's system. Tarski and Givant (1999: 175) proved that Tarski's system is:

This has the consequence that every statement of (second-order, general) Euclidean geometry which can be formulated as a first-order sentence in Tarski's system is true if and only if it is provable in Tarski's system, and this provability can be automatically checked with Tarski's algorithm. This, for instance, applies to all theorems in Euclid's Elements, Book I. An example of a theorem of Euclidean geometry which cannot be so formulated is the Archimedean property: to any two positive-length line segments S and S there exists a natural number n such that nS is longer than S. (This is a consequence of the fact that there are real-closed fields that contain infinitesimals.) Other notions that cannot be expressed in Tarski's system are the constructability with straightedge and compass and statements that talk about "all polygones" etc.

Gupta (1965) proved the Tarski's axioms independent, excepting Pasch and Reflexivity of Congruence.

Negating the Axiom of Euclid yields hyperbolic geometry, while eliminating it outright yields absolute geometry. Full (as opposed to elementary) Euclidean geometry requires giving up a first order axiomatization: replace φ(x) and ψ(y) in the axiom schema of Continuity with x ∈ A and y ∈ B, where A and B are universally quantified variables ranging over sets of points.