Tarski's axioms
Encyclopedia : T : TA : TAR : Tarski's axioms
Tarski's axioms, due to Alfred Tarski, are an axiom set for the substantial fragment of Euclidean geometry, called "elementary," that is formulable in first-order logic with identity, and requiring no set theory. Other modern axiomizations of Euclidean geometry are those by Hilbert and George Birkhoff.
The axioms
Alfred Tarski worked on the axiomatization and metamathematics of Euclidean geometry intermittently from 1926 until his 1983 death, with Tarski (1959) heralding his mature interest in the subject. The work of Tarski and his student and disciples 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 resulting metamathematics, and a fair bit of the subject. Gupta (1965) made important contributions, and Tarski and Givant (1999) discuss much of 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 of Euclidean plane geometry. This objective required reformulating that geometry as a first-order theory. Tarski did so by positing a universe of points and two primitive relations: a triadic relation of "betweenness," and a tetradic relation of "congruence" (or "equidistance"). The notation employed here is a slight variant of Tarski's. Let lower case letters denote variables ranging over the universe of points. That y is "between" x and z, i.e., that x, y, and z are collinear with y "between", is denoted by the atomic sentence xyz. Let xy denote the line segment whose endpoints are x and y. The intuitive meaning of the atomic sentence wx ≡ yz is that wx is congruent to yz. Informally, the "distance" between w and x is the same as the distance between y and z. Betweenness captures the affine aspect of Euclidean geometry; congruence, the metric aspect. Identity, invoked five times, is a primitive binary relation that is part of the underlying logic.
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. Variables not existentially quantified can be taken as tacitly universally quantified.
Congruence alone:
Reflexivity of Congruence:
- [xy \equiv yx\,]
Identity of Congruence:
- [(xy \equiv zz) \rightarrow (x=y)]
Transitivity of Congruence:
- [((xy \equiv zu) \and (xy \equiv vw)) \rightarrow (zu \equiv vw)]
Betweenness alone:
Identity of Betweenness:
- [xyx \rightarrow (x=y)]
Axiom of Pasch:
- [\exists a[(xuz and yvz) rightarrow (uay and vax)]]
Draw line segments connecting any two vertices of a given triangle with the sides opposite the vertices. These two line segments must then intersect at some point inside the triangle.
Axiom schema of Continuity Let φ(x) and ψ(y) be first-order formulae in which a and b do not occur free. Moreover, there are no free instances of x in ψ(y) or of y in φ(x). Then all instances of
- [\exists a \exists b[(varphi(x) and psi(y) rightarrow axy) rightarrow (varphi(x) and psi(y) rightarrow xby)]]
Let the first-order formulae φ and ψ each determine an endpoint of xy. If there exists a longer line segment of which xy is a part (so that xy is not coextensive with the universe), there exists a point between x and y.
Lower Dimension:
- [\exists a \exists b \exists c (\neg abc \and \neg bca \and \neg cab)], logically equivalent to [\neg \forall x \forall y \forall z (xyz \or yzx \or zxy)]
Congruence and Betweenness:
Upper Dimension:
- [((xu \equiv xv) \and (yu \equiv yv) \and (zu \equiv zv) \and (u \ne v)) \rightarrow (xyz \or yzx \or zxy)]
Axiom of Euclid: Each of the three variants of this axiom, all equivalent 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: [((xyw \and xy \equiv yw ) \and (xuv \and xu \equiv xv) \and (yuz \and yu \equiv zu)) \rightarrow (yz \equiv vw)]
- B:[\exists a[xyz or yzx or zxy or ((xa equiv ya) and (xa equiv za))]]
- C: [ \exists a \exists b[(xuv and yuz and x ne u) rightarrow (xya and xzb and avb)]]
Five Segment:
- [((x \ne y) \and (x' \ne y') \and xyz \and x'y'z' \and (xy \equiv x'y') \and (yz \equiv y'z') \and (xu \equiv x'u') \and (yu \equiv y'u') ) \rightarrow (zu \equiv z'u')]
Segment Construction:
- [ \exists a [wxa and (xa equiv yz)]]
Discussion
Starting from a dense universe of points and two primitive relations over points, Tarski in essence built a geometry of line segments. According to Tarski and Givant (1999: 192-93), none of the above axioms is fundamentally new. The first four axioms establish some elementary properties of the two primitive relations. For instance, Reflexivity and Transitivity (whose true name, "Euclidian," aliases with Euclid's axiom) of Congruence establish that congruence is an equivalence relation. 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 ↔ xyx extends these Identity axioms.A number of other properties of betweenness are derivable as theorems including:
- Reflexivity: xxy ;
- Symmetry: xyz → zyx ;
- Transitivity: (xyw ∧ yzw) → xyz ;
- Connectivity: (xyw ∧ xzw) → (xyz ∨ xzy).
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 Euclidian geometry for dimensions 0, 1, and greater than 2 (Tarski and Givant 1999: Axioms 8(1), 8(n), 9(0), 9(1), 9(n) ). 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 dimension > 1, betweenness can be defined in terms of congruence.
The Axiom schema of Continuity assures that the universe of points is dense. The Axioms of Pasch and Euclid are well known. Remarkably, Euclidian geometry requires but two more axioms:
- Segment Construction. This axiom makes measurement and the Cartesian coordinate system possible--simply assign the value of 1 to some arbitrary line segment;
- Five Segments. This bears on the congruence of triangles.
Let "wff" abbreviate "syntactically correct formula of elementary geometry." Tarski (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 wff or its negation is a theorem provable from the axioms;
- Decidable: There exists a finite algorithm that assigns a truth value to every wff. This is so because Tarski's axioms and primitive relations constitute a model of a real closed field. Tarski proved the latter decidable by quantifier elimination. Gupta (1965) proved all axioms independent, Pasch and Reflexivity of Congruence excepted.
Comparison with Hilbert
Hilbert's axioms for plane geometry number 14, 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.References
- Gupta, H. N., 1965. Contributions to the Axiomatic Foundations of Geometry. Ph.D. thesis, University of California-Berkeley.
- Alfred Tarski, 1959, '"What is Elementary Geometry?" in Leon Henkin, Patrick Suppes, and Tarski, A., eds., The Axiomatic Method, with Special Reference to Geometry and Physics. North Holland.
- ------, and Givant, Steven, 1999, "Tarski's system of geometry," Bulletin of Symbolic Logic 5: 175-214. [link]
- Schwabhäuser, W., Szmielew, W., and Alfred Tarski, 1983. Metamathematische Methoden in der Geometrie. Springer-Verlag.
- Szczerba, L. W., 1986, "Tarski and Geometry," Journal of Symbolic Logic 51: 907-12.
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.
