Tarski's axioms are anaxiom system forEuclidean geometry, specifically for that portion of Euclidean geometry that is formulable infirst-order logic withidentity (i.e. is formulable as anelementary theory). As such, it does not require an underlyingset theory. The only primitive objects of the system are "points" and the only primitive predicates are "betweenness" (expressing the fact that a point lies on a line segment between two other points) and "congruence" (expressing the fact that the distance between two points equals the distance between two other points). The system contains infinitely many axioms.

The axiom system is due toAlfred Tarski who first presented it in 1926.^[1] Other modern axiomizations of Euclidean geometry areHilbert's axioms (1899) andBirkhoff's axioms (1932).

Using his axiom system, Tarski was able to show that the first-order theory of Euclidean geometry isconsistent,complete anddecidable: every sentence in its language is either provable or disprovable from the axioms, and we have an algorithm which decides for any given sentence whether it is provable or not.

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 ofMario Pieri, an Italian geometer who was strongly influenced by Peano. Tarski preferred Pieri's system [of hisPoint 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 theprimitive 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 aformal system consisting of symbol strings, calledsentences, whose construction respects formalsyntactical rules, and rules of proof that determine the allowed manipulations of the sentences. Unlike some other modern axiomatizations, such asBirkhoff's andHilbert's, Tarski's axiomatization has noprimitive objects other thanpoints, 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 afirst-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 fordoing Euclidean geometry. Rather, Tarski designed his system to facilitate its analysis via the tools ofmathematical 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 theprenex normal form. This form has alluniversal quantifiers preceding anyexistential quantifiers, so that all sentences can be recast in the form${\displaystyle \mathrm{\forall }u\mathrm{\forall }v\dots \mathrm{\exists }a\mathrm{\exists }b\dots .}$ This fact allowed Tarski to prove that Euclidean geometry isdecidable: there exists analgorithm which can determine the truth or falsity of any sentence. Tarski's axiomatization is alsocomplete. This does not contradictGödel's first incompleteness theorem, because Tarski's theory lacks the expressive power needed to interpretRobinson arithmetic (Franzén 2005, pp. 25–26).

Alfred Tarski worked on the axiomatization and metamathematics ofEuclidean 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 10axioms and oneaxiom schema shown below, the associatedmetamathematics, and a fair bit of the subject. Gupta (1965) made important contributions, and Tarski and Givant (1999) discuss the history.

These axioms are a more elegant version of a set Tarski devised in the 1920s as part of his investigation of the metamathematical properties ofEuclidean plane geometry. This objective required reformulating that geometry as afirst-order theory. Tarski did so by positing auniverse ofpoints, with lower case letters denoting variables ranging over that universe.Equality is provided by the underlying logic (seeFirst-order logic#Equality and its axioms).^[2] Tarski then posited two primitive relations:

• Betweenness, atriadic relation. Theatomic sentenceBxyz denotes that the pointy is "between" the pointsx andz, in other words, thaty is a point on theline segmentxz. (This relation is interpreted inclusively, so thatBxyz is trivially true wheneverx=y ory=z.)
• Congruence (or "equidistance"), atetradic relation. Theatomic sentenceCwxyz or commonlywx ≡yz can be interpreted aswx iscongruent toyz, in other words, that thelength of the line segmentwx is equal to the length of the line segmentyz.

Betweenness captures theaffine aspect (such as the parallelism of lines) of Euclidean geometry; congruence, itsmetric aspect (such as angles and distances). The background logic includesidentity, abinary relation denoted by =.

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 asuniversal closures; hence anyfree variables should be taken as tacitlyuniversally quantified.

Reflexivity of congruence

${\displaystyle xy\equiv yx.}$

Identity of congruence

${\displaystyle xy\equiv zz\to x=y.}$

Transitivity of congruence

${\displaystyle (xy\equiv zu\wedge xy\equiv vw)\to zu\equiv vw.}$

While the congruence relation${\displaystyle 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${\displaystyle xy}$ and${\displaystyle zw}$. Thereflexivity andtransitivity axioms above, combined, prove both:

• that this binary relation is in fact anequivalence relation
  • it is reflexive:${\displaystyle xy\equiv xy}$.
  • it is symmetric${\displaystyle xy\equiv zw\to zw\equiv xy}$.
  • it is transitive${\displaystyle (xy\equiv zu\wedge zu\equiv vw)\to xy\equiv vw}$.
• and that the order in which the points of a line segment are specified is irrelevant.
  • ${\displaystyle xy\equiv zw\to xy\equiv wz}$.
  • ${\displaystyle xy\equiv zw\to yx\equiv zw}$.
  • ${\displaystyle xy\equiv zw\to yx\equiv wz}$.

Thetransitivity axiom asserts that congruence isEuclidean, in that it respects the first ofEuclid's "common notions".

Theidentity of congruence axiom states, intuitively, that ifxy is congruent with a segment that begins and ends at the same point,x andy are the same point. This is closely related to the notion ofreflexivity forbinary relations.

Identity of betweenness

${\displaystyle Bxyx\to x=y.}$

The only point on the line segment${\displaystyle xx}$ is${\displaystyle x}$ itself.

Axiom of Pasch

${\displaystyle (Bxuz\wedge Byvz)\to \mathrm{\exists }a(Buay\wedge Bvax).}$

Axiom schema of continuity

Let φ(x) and ψ(y) befirst-order formulae containing nofree instances of eithera orb. Let there also be no free instances ofx in ψ(y) or ofy in φ(x). Then all instances of the following schema are axioms:

${\displaystyle \left(\mathrm{\exists }a\mathrm{\forall }x\mathrm{\forall }y[(\varphi (x)\wedge \psi (y))\to Baxy]\right)\to \mathrm{\exists }b\mathrm{\forall }x\mathrm{\forall }y[(\varphi (x)\wedge \psi (y))\to Bxby].}$

Letr be a ray with endpointa. Let the first order formulae φ and ψ define subsetsX andY ofr, such that every point inY is to the right of every point ofX (with respect toa). Then there exists a pointb inr lying betweenX andY. This is essentially theDedekind cut construction, carried out in a way that avoids quantification over sets.

Note that the formulae φ(x) and ψ(y) may contain parameters, i.e. free variables different froma,b,x,y. And indeed, each instance of the axiom scheme that does not contain parameters can be proven from the other axioms.^[3]

Lowerdimension

${\displaystyle \mathrm{\exists }a\mathrm{\exists }b\mathrm{\exists }c[\mathrm{\neg }Babc\wedge \mathrm{\neg }Bbca\wedge \mathrm{\neg }Bcab].}$

There exist three noncollinear points. Without this axiom, the theory could bemodeled by the one-dimensionalreal line, a single point, or even the empty set.

Upperdimension

${\displaystyle (xu\equiv xv)\wedge (yu\equiv yv)\wedge (zu\equiv zv)\wedge (u\ne v)\to (Bxyz\vee Byzx\vee Bzxy).}$

Three points equidistant from two distinct points form a line. Without this axiom, the theory could be modeled bythree-dimensional or higher-dimensional space.

Axiom of Euclid

Three variants of this axiom can be given, labeled A, B and C below. They are equivalent to each other given the remaining Tarski's axioms, and indeed equivalent to Euclid'sparallel postulate.

A:${\displaystyle ((Bxyw\wedge xy\equiv yw)\wedge (Bxuv\wedge xu\equiv uv)\wedge (Byuz\wedge yu\equiv uz))\to yz\equiv vw.}$

Let a line segment join the midpoint of two sides of a giventriangle. That line segment will be half as long as the third side. This is equivalent to theinterior angles of any triangle summing to tworight angles.

B:${\displaystyle Bxyz\vee Byzx\vee Bzxy\vee \mathrm{\exists }a(xa\equiv ya\wedge xa\equiv za).}$

Given anytriangle, there exists acircle that includes all of its vertices.

C:${\displaystyle (Bxuv\wedge Byuz\wedge x\ne u)\to \mathrm{\exists }a\mathrm{\exists }b(Bxya\wedge Bxzb\wedge Bavb).}$

Given anyangle and any pointv in its interior, there exists a line segment includingv, with an endpoint on each side of the angle.

Each variant has an advantage over the others:

• A dispenses withexistential quantifiers;
• B has the fewest variables andatomic sentences;
• C requires but one primitive notion, betweenness. This variant is the usual one given in the literature.

Five segment

${\displaystyle (x\ne y\wedge Bxyz\wedge B{x}^{\prime }{y}^{\prime }{z}^{\prime }\wedge xy\equiv x^{\prime }{y}^{\prime }\wedge yz\equiv y^{\prime }{z}^{\prime }\wedge xu\equiv x^{\prime }{u}^{\prime }\wedge yu\equiv y^{\prime }{u}^{\prime })\to zu\equiv z^{\prime }{u}^{\prime }.}$

Begin with twotriangles,xuz andx'u'z'. Draw the line segmentsyu andy'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 eachcongruent to a segment in the other triangle, then the fifth segments in both triangles must be congruent.

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

Segment construction

${\displaystyle \mathrm{\exists }z[Bxyz\wedge yz\equiv ab].}$

For any pointy, it is possible to draw in any direction (determined byx) a line congruent to any segmentab.

According to Tarski and Givant (1999: 192-93), none of the aboveaxioms 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 anequivalence relation over line segments. The identity of congruence and of betweenness govern the trivial case when those relations are applied to nondistinct points. The theoremxy≡zz ↔x=y ↔Bxyx extends these Identity axioms.

A number of other properties of betweenness are derivable as theorems^[4] including:

• Reflexivity:Bxxy ;
• Symmetry:Bxyz →Bzyx ;
• Transitivity: (Bxyw ∧Byzw) →Bxyz ;
• Connectivity: (Bxyw ∧Bxzw) → (Bxyz ∨Bxzy).

The last two propertiestotally 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 forEuclidean geometry fordimensions 0, 1, and greater than 2 (Tarski and Givant 1999: Axioms 8⁽¹⁾, 8⁽ⁿ⁾, 9⁽⁰⁾, 9⁽¹⁾, 9⁽ⁿ⁾ ). Note thatsolid geometry requires no new axioms, unlike the case withHilbert's axioms. Moreover,lower dimension forn dimensions is simply the negation ofupper dimension forn - 1 dimensions.

When the number of dimensions is greater than 1, betweenness can be defined in terms ofcongruence (Tarski and Givant, 1999). First define the relation "≤" (where${\displaystyle ab\le cd}$ is interpreted "the length of line segment${\displaystyle ab}$ is less than or equal to the length of line segment${\displaystyle cd}$"):

${\displaystyle xy\le zu\leftrightarrow \mathrm{\forall }v(zv\equiv uv\to \mathrm{\exists }w(xw\equiv yw\wedge yw\equiv uv)).}$

In the case of two dimensions, the intuition is as follows: For any line segmentxy, consider the possible range of lengths ofxv, wherev is any point on the perpendicular bisector ofxy. It is apparent that while there is no upper bound to the length ofxv, there is a lower bound, which occurs whenv is the midpoint ofxy. So ifxy is shorter than or equal tozu, then the range of possible lengths ofxv will be a superset of the range of possible lengths ofzw, wherew is any point on the perpendicular bisector ofzu.

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

${\displaystyle Bxyz\leftrightarrow \mathrm{\forall }u((ux\le xy\wedge uz\le zy)\to u=y).}$

The axiom schema of continuity assures that the ordering of points on a line iscomplete (with respect to first-order definable properties). As was pointed out by Tarski, this first-order axiom schema may be replaced by a more powerfulsecond-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 ofPasch and Euclid are well known. Thesegment construction axiom makesmeasurement and theCartesian 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 areal-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.

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

• Consistent: There is no wff such that it and its negation can both be proven from the axioms;
• Complete: Every wff or its negation is a theorem provable from the axioms;
• Decidable: There exists analgorithm that decides for every wff whether is it is provable or disprovable from the axioms. This follows from Tarski's:
  • Decision procedure for thereal closed field, which he found byquantifier elimination (theTarski–Seidenberg theorem);
  • Axioms admitting the above-mentioned representation as a two-dimensional plane over areal closed field.

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 inEuclid's Elements, Book I. An example of a theorem of Euclidean geometry which cannot be so formulated is theArchimedean property: to any two positive-length line segmentsS₁ andS₂ there exists a natural numbern such thatnS₁ is longer thanS₂. (This is a consequence of the fact that there are real-closed fields that contain infinitesimals.^[5]) Other notions that cannot be expressed in Tarski's system are theconstructability with straightedge and compass and statements that talk about "all polygons" etc.^[6]

Gupta (1965) proved the Tarski's axioms independent, exceptingPasch andreflexivity of congruence.

Negating the axiom of Euclid yieldshyperbolic geometry, while eliminating it outright yieldsabsolute 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 withx ∈A andy ∈B, whereA andB are universally quantified variables ranging over sets of points.

Further simplifications for the fragment describing the plane Euclidean geometry of ruler and segment-transporter constructions, as well as for that of ruler and compass constructions were provided in (Pambuccian 2024). Each axiom of the axiom systems presented there is aprenex statement with at most 5 variables.

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 istriangle. (VersionsB andC 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 primitivebinary relation "on," linking a point and a line.

Hilbert uses two axioms of continuity, and they requiresecond-order logic. By contrast, Tarski'saxiom schema of continuity consists of infinitely many first-order axioms. Such a schema is indispensable; Euclidean geometry in Tarski's (or equivalent) language cannot be finitely axiomatized as afirst-order theory.

Hilbert's system is therefore considerably stronger: everymodel is isomorphic to the real plane${\displaystyle {\mathbb{R}}^2}$ (using the standard notions of points and lines). By contrast, Tarski's system has many non-isomorphic models: for every real-closed fieldF, the planeF² provides one such model (where betweenness and congruence are defined in the obvious way).^[7]

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

• Euclidean geometry
• Euclidean space
• Hilbert's axioms
• Birkhoff's axioms

• Franzén, Torkel (2005),Gödel's Theorem: An Incomplete Guide to Its Use and Abuse, A K Peters,ISBN 1-56881-238-8
• Givant, Steven (1 December 1999)."Unifying threads in Alfred Tarski's Work".The Mathematical Intelligencer.21 (1):47–58.doi:10.1007/BF03024832.ISSN 1866-7414.S2CID 119716413.
• Greenberg, Marvin Jay (2010)."Old and New Results in the Foundations of Elementary Plane Euclidean and Non-Euclidean Geometries"(PDF).The American Mathematical Monthly.117 (3): 198.doi:10.4169/000298910x480063.
• Gupta, H. N. (1965).Contributions to the Axiomatic Foundations of Geometry (Ph.D. thesis). University of California-Berkeley.
• Tarski, Alfred (1959), "What is elementary geometry?", in Leon Henkin, Patrick Suppes and Alfred Tarski (ed.),The axiomatic method. With special reference to geometry and physics. Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, pp. 16–29,MR 0106185.
  • Available as a 2007reprint, Brouwer Press,ISBN 1-4437-2812-8
• Tarski, Alfred; Givant, Steven (1999),"Tarski's system of geometry",The Bulletin of Symbolic Logic,5 (2):175–214,CiteSeerX 10.1.1.27.9012,doi:10.2307/421089,ISSN 1079-8986,JSTOR 421089,MR 1791303,S2CID 18551419
• Schwabhäuser, W.;Szmielew, W.;Tarski, Alfred (1983).Metamathematische Methoden in der Geometrie. Springer-Verlag.
• Szczerba, L. W. (1986)."Tarski and Geometry"(PDF).Journal of Symbolic Logic.51 (4):907–12.doi:10.2307/2273904.JSTOR 2273904.S2CID 35275962.
• Pambuccian, V. (2024)."The simplicity degree of Tarski's Euclidean geometry of ruler and dividers is 5".Results in Mathematics.79 (4):1–26.doi:10.1007/s00025-024-02186-4.

• Elementary geometry
• Foundations of geometry
• Mathematical axioms

• Articles with short description
• Short description is different from Wikidata