Tarski's axioms

Tarski's axioms, due to Alfred Tarski, are an axiom set for the substantial fragment of Euclidean geometry that is formulable in first-order logic with identity, and requiring no set theory (i.e., that part of Euclidean geometry that is formulable as an elementary theory). Other modern axiomizations of Euclidean geometry are Hilbert's axioms and Birkhoff's axioms.

Overview

Early in his career Tarski taught geometry and researched set theory. His coworker Steven Givant (1999) explained Tarski's take-off point:
:From Enriques, Tarski learned of the work of Mario Pieri, an Italian geometer who was strongly influenced by Peano. Tarski preferred Pieri's system f his ''Point and Sphere'' memoir where the logical structure and the complexity of the axioms were more transparent.
Givant then says that "with typical thoroughness" Tarski devised his system:
:What was different about Tarski's approach to geometry? First of all, the axiom system was much simpler than any of the axiom systems that existed up to that time. In fact the length of all of Tarski's axioms together is not much more than just one of Pieri's 24 axioms. It was the first system of Euclidean geometry that was simple enough for all axioms to be expressed in terms of the primitive notions only, without the help of defined notions. Of even greater importance, for the first time a clear distinction was made between full geometry and its elementary — that is, its first order — part.

Like other modern axiomatizations of Euclidean geometry, Tarski's employs a formal system consisting of symbol strings, called sentences, whose construction respects formal syntactical rules, and rules of proof that determine the allowed manipulations of the sentences. Unlike some other modern axiomatizations, such as Birkhoff's and Hilbert's, Tarski's axiomatization has no primitive objects other than ''points'', so a variable or constant cannot refer to a line or an angle. Because points are the only primitive objects, and because Tarski's system is a first-order theory, it is not even possible to define lines as sets of points. The only primitive relations (predicates) are "betweenness" and "congruence" among points.

Tarski's axiomatization is shorter than its rivals, in a sense Tarski and Givant (1999) make explicit. It is more concise than Pieri's because Pieri had only two primitive notions while Tarski introduced three: point, betweenness, and congruence. Such economy of primitive and defined notions means that Tarski's system is not very convenient for ''doing'' Euclidean geometry. Rather, Tarski designed his system to facilitate its analysis via the tools of mathematical logic, i.e., to facilitate deriving its metamathematical properties. Tarski's system has the unusual property that all sentences can be written in universal-existential form, a special case of the prenex normal form. This form has all universal quantifiers preceding any existential quantifiers, so that all sentences can be recast in the form $\forall u \forall v \ldots\exists a \exists b\dots.$ This fact allowed Tarski to prove that Euclidean geometry is decidable: there exists an algorithm which can determine the truth or falsity of any sentence. Tarski's axiomatization is also complete. This does not contradict Gödel's first incompleteness theorem, because Tarski's theory lacks the expressive power needed to interpret Robinson arithmetic .

The axioms

Alfred Tarski worked on the axiomatization and metamathematics of Euclidean geometry intermittently from 1926 until his death in 1983, with Tarski (1959) heralding his mature interest in the subject. The work of Tarski and his students on Euclidean geometry culminated in the monograph Schwabhäuser, Szmielew, and Tarski (1983), which set out the 10 axioms and one axiom schema shown below, the associated metamathematics, and a fair bit of the subject. Gupta (1965) made important contributions, and Tarski and Givant (1999) discuss the history.

Fundamental relations

These axioms are a more elegant version of a set Tarski devised in the 1920s as part of his investigation of the metamathematical properties of Euclidean plane geometry. This objective required reformulating that geometry as a first-order theory. Tarski did so by positing a universe of points, with lower case letters denoting variables ranging over that universe. Equality is provided by the underlying logic (see First-order logic#Equality and its axioms).Tarski and Givant, 1999, page 177 Tarski then posited two primitive relations:
* ''Betweenness'', a triadic relation. The atomic sentence ''Bxyz'' or ''(y)B(x,z)'' denotes that ''y'' is "between" ''x'' and ''z'', in other words, that ''y'' is a point on the line segment ''xz''. (This relation is interpreted inclusively, so that ''Bxyz'' is trivially true whenever ''x=y'' or ''y=z'').
* '' Congruence'' (or "equidistance"), a tetradic relation. The atomic sentence ''Cwxyz'' or ''(w,x)C(y,z)'' or commonly ''wx'' ≡ ''yz'' can be interpreted as ''wx'' is congruent to ''yz'', in other words, that the length of the line segment ''wx'' is equal to the length of the line segment ''yz''.

Betweenness captures the affine aspect (such as the parallelism of lines) of Euclidean geometry; congruence, its metric aspect (such as angles and distances). The background logic includes identity, a binary relation. The axioms invoke identity (or its negation) on five occasions.

The axioms below are grouped by the types of relation they invoke, then sorted, first by the number of existential quantifiers, then by the number of atomic sentences. The axioms should be read as universal closures; hence any free variables should be taken as tacitly universally quantified.

Congruence axioms

; Reflexivity of Congruence:
: $xy \equiv yx\,.$

; Identity of Congruence:
: $xy \equiv zz \rightarrow x=y.$

; Transitivity of Congruence:
: $(xy \equiv zu \land xy \equiv vw) \rightarrow zu \equiv vw.$

Commentary

While the congruence relation $xy \equiv zw$ is, formally, a 4-way relation among points, it may also be thought of, informally, as a binary relation between two line segments $xy$ and $zw$. The "Reflexivity" and "Transitivity" axioms above, combined, prove both:
* that this binary relation is in fact an equivalence relation
** it is reflexive: $xy \equiv xy$.
** it is symmetric $xy \equiv zw \rightarrow zw \equiv xy$.
** it is transitive $(xy \equiv zu \land zu \equiv vw) \rightarrow xy \equiv vw$.
* and that the order in which the points of a line segment are specified is irrelevant.
** $xy \equiv zw \rightarrow xy \equiv wz$.
** $xy \equiv zw \rightarrow yx \equiv zw$.
** $xy \equiv zw \rightarrow yx \equiv wz$.

The "transitivity" axiom asserts that congruence is Euclidean, in that it respects the first of Euclid's " common notions".

The "Identity of Congruence" axiom states, intuitively, that if ''xy'' is congruent with a segment that begins and ends at the same point, ''x'' and ''y'' are the same point. This is closely related to the notion of reflexivity for binary relations.

Betweenness axioms

; Identity of Betweenness
: $Bxyx \rightarrow x=y.$
The only point on the line segment $xx$ is $x$ itself.

; Axiom of Pasch
: $(Bxuz \land Byvz) \rightarrow \exists a\, (Buay \land Bvax).$

; Axiom schema of Continuity
Let φ(''x'') and ψ(''y'') be first-order formulae containing no free instances of either ''a'' or ''b''. Let there also be no free instances of ''x'' in ψ(''y'') or of ''y'' in φ(''x''). Then all instances of the following schema are axioms:
: \exists a \,\forall x\, \forall y\, \phi(x) \land \psi(y)) \rightarrow Baxy\rightarrow \exists b\, \forall x\, \forall y\, \phi(x) \land \psi(y)) \rightarrow Bxby
Let ''r'' be a ray with endpoint ''a''. Let the first order formulae φ and ψ define subsets ''X'' and ''Y'' of ''r'', such that every point in ''Y'' is to the right of every point of ''X'' (with respect to ''a''). Then there exists a point ''b'' in ''r'' lying between ''X'' and ''Y''. This is essentially the Dedekind cut construction, carried out in a way that avoids quantification over sets.

; Lower Dimension
: \exists a \, \exists b\, \exists c\, neg Babc \land \neg Bbca \land \neg Bcab
There exist three noncollinear points. Without this axiom, the theory could be modeled by the one-dimensional real line, a single point, or even the empty set.

Congruence and betweenness

; Upper Dimension
: $(xu \equiv xv) \land (yu \equiv yv) \land (zu \equiv zv )\land (u \ne v) \rightarrow (Bxyz \lor Byzx \lor Bzxy).$
Three points equidistant from two distinct points form a line. Without this axiom, the theory could be modeled by three-dimensional or higher-dimensional space.

; Axiom of Euclid
Each of the three variants of this axiom, all equivalent over the remaining Tarski's axioms to Euclid's parallel postulate, has an advantage over the others:
* A dispenses with existential quantifiers;
* B has the fewest variables and atomic sentences;
* C requires but one primitive notion, betweenness. This variant is the usual one given in the literature.

: A: $((Bxyw \land xy \equiv yw ) \land (Bxuv \land xu \equiv uv) \land (Byuz \land yu \equiv uz)) \rightarrow yz \equiv vw.$
Let a line segment join the midpoint of two sides of a given triangle. That line segment will be half as long as the third side. This is equivalent to the interior angles of any triangle summing to two right angles.

: B: $Bxyz \lor Byzx \lor Bzxy \lor \exists a\, (xa \equiv ya \land xa \equiv za).$
Given any triangle, there exists a circle that includes all of its vertices.

: C: $(Bxuv \land Byuz \land x \ne u) \rightarrow \exists a\, \exists b\,(Bxya \land Bxzb \land Bavb).$
Given any angle and any point ''v'' in its interior, there exists a line segment including ''v'', with an endpoint on each side of the angle.

; Five Segment

:$\rightarrow zu \equiv z'u'.$

Begin with two triangles, ''xuz'' and ''x'u'z'.'' Draw the line segments ''yu'' and ''y'u','' connecting a vertex of each triangle to a point on the side opposite to the vertex. The result is two divided triangles, each made up of five segments. If four segments of one triangle are each congruent to a segment in the other triangle, then the fifth segments in both triangles must be congruent.

This is equivalent to the side-angle-side rule for determining that two triangles are congruent; if the angles ''uxz'' and ''u'x'z''' are congruent (there exist congruent triangles ''xuz'' and ''x'u'z'''), and the two pairs of incident sides are congruent (''xu ≡ x'u''' and ''xz ≡ x'z'''), then the remaining pair of sides is also congruent (''uz ≡ u'z).

; Segment Construction
: \exists z\, xyz \land yz \equiv ab

For any point ''y'', it is possible to draw in any direction (determined by ''x'') a line congruent to any segment ''ab''.

Discussion

Starting from two primitive relations whose fields are a dense universe of points, Tarski built a geometry of line segments. 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:
* Reflexivity: ''Bxxy'' ;
*Symmetry: ''Bxyz'' → ''Bzyx'' ;
* Transitivity: (''Bxyw'' ∧ ''Byzw'') → ''Bxyz'' ;
*Connectivity: (''Bxyw'' ∧ ''Bxzw'') → (''Bxyz'' ∨ ''Bxzy'').
The last two properties totally order the points making up a line segment.

Upper and Lower Dimension together require that any model of these axioms have a specific finite dimensionality. 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 $ab \leq cd$ is interpreted "the length of line segment $ab$ is less than or equal to the length of line segment $cd$"):
:$xy \le zu \leftrightarrow \forall v ( zv \equiv uv \rightarrow \exists w ( xw \equiv yw \land yw \equiv uv ) ).$
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:
:$Bxyz \leftrightarrow \forall u ( ( ux \le xy \land uz \le zy ) \rightarrow u = y ).$

The Axiom Schema of Continuity assures that the ordering of points on a line is complete (with respect to first-order definable properties). The Axioms of Pasch and Euclid are well known. Remarkably, Euclidean geometry requires just the following further axioms:
* ''Segment Construction''. This axiom makes measurement and the Cartesian coordinate system possible—simply assign the real number of 1 to some arbitrary non-empty line segment;

Let ''wff'' stand for a well-formed formula (or syntactically correct formula) of elementary geometry. Tarski and Givant (1999: 175) proved that elementary geometry is:
*Consistent: There is no wff such that it and its negation are both theorems;
*Complete: Every sentence or its negation is a theorem provable from the axioms;
* Decidable: There exists an algorithm that assigns a truth value to every sentence. This follows from Tarski's:
** Decision procedure for the real closed field, which he found by quantifier elimination (the Tarski–Seidenberg theorem);
**Axioms admitting of a (multi-dimensional) faithful interpretation as a real closed field.
Gupta (1965) proved the above axioms independent, ''Pasch'' and ''Reflexivity of Congruence'' excepted.

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.

Comparison with Hilbert

Hilbert's axioms for plane geometry number 16, and include Transitivity of Congruence and a variant of the Axiom of Pasch. The only notion from intuitive geometry invoked in the remarks to Tarski's axioms is triangle. (Versions B and C of the Axiom of Euclid refer to "circle" and "angle," respectively.) Hilbert's axioms also require "ray," "angle," and the notion of a triangle "including" an angle. In addition to betweenness and congruence, Hilbert's axioms require a primitive binary relation "on," linking a point and a line. The Axiom schema of Continuity plays a role similar to Hilbert's two axioms of Continuity. This schema is indispensable; Euclidean geometry in Tarski's (or equivalent) language cannot be finitely axiomatized as a first-order theory. Hilbert's axioms do not constitute a first-order theory because his continuity axioms require second-order logic.

The first four groups of axioms of Hilbert's axioms for plane geometry are bi-interpretable with Tarski's axioms minus continuity.

See also

* Euclidean geometry
* Euclidean space

Notes

References

*
*Givant, Steven (1999) "Unifying threads in Alfred Tarski's Work", Mathematical Intelligencer 21:47–58.
*Gupta, H. N. (1965) ''Contributions to the Axiomatic Foundations of Geometry''. Ph.D. thesis, University of California-Berkeley.
*. Available as a 200
reprint
Brouwer Press,
*
*Schwabhäuser, W., Szmielew, W., and Alfred Tarski, 1983. ''Metamathematische Methoden in der Geometrie''. Springer-Verlag.
*

{{Mathematical logic

Elementary geometry
Foundations of geometry
Mathematical axioms