Elementary Geometry (Tarski's Axioms)

Origin. Tarski lectured on the system at Warsaw in 1926–27; publication was delayed, first by other projects and then by the war, which destroyed the galley proofs. The axioms appeared in 1948, and a reduced set in "What is elementary geometry?" (in Henkin, Suppes, and Tarski, eds., The Axiomatic Method, 1959). Gupta's Berkeley thesis (1965) removed redundancies; the definitive treatment is Schwabhäuser, Szmielew, and Tarski, Metamathematische Methoden in der Geometrie (1983). Tarski and Givant, "Tarski's system of geometry" (BSL 5, 1999), give the history.

Models. Points, and nothing else — no lines, no planes, no sets, no numbers. Two primitive relations suffice: betweenness and congruence. The result is a first-order theory that is complete and decidable, whose models are exactly the Cartesian planes F² over real closed fields F. Hilbert's 1899 axioms are not first-order — the continuity axioms quantify over sets — and that is the difference the whole entry turns on: Tarski's continuity is a schema, so the theory stays elementary, and being elementary is what buys the decision procedure.

Formalism.

Language: one sort (points), variables a, b, c, …; no constants, no functions. Two primitives: B(a, b, c) — b lies between a and c (non-strict; degenerate cases allowed) ab ≡ cd — the segment ab is congruent to the segment cd (a quaternary relation)

The axioms (Schwabhäuser–Szmielew–Tarski): ten axioms and one schema. A1 Reflexivity of congruence: ab ≡ ba A2 Transitivity of congruence: ab ≡ pq ∧ ab ≡ rs → pq ≡ rs A3 Identity of congruence: ab ≡ cc → a = b A4 Segment construction: ∃x (B(q, a, x) ∧ ax ≡ bc) A5 Five-segment: the congruence-transfer axiom that replaces SAS A6 Identity of betweenness: B(a, b, a) → a = b A7 Pasch (inner form): B(a, p, c) ∧ B(b, q, c) → ∃x (B(p, x, b) ∧ B(q, x, a)) A8 Lower dimension: ∃a∃b∃c (¬B(a,b,c) ∧ ¬B(b,c,a) ∧ ¬B(c,a,b)) A9 Upper dimension: fixes the dimension to 2 (variants fix n) A10 Euclid's axiom: the parallel postulate, in a betweenness form A11 Continuity schema: for all φ, ψ with the stated free variables, ∃a ∀x ∀y (φ(x) ∧ ψ(y) → B(a, x, y)) → ∃b ∀x ∀y (φ(x) ∧ ψ(y) → B(x, b, y)) — a Dedekind cut condition, one instance per definable pair of sets.

The representation theorem: Every model of the theory is isomorphic to F² for some real closed field F, and conversely. The construction: the first ten axioms give an ordered field structure on a line, with an arbitrary segment as the unit; the continuity schema forces real closure.

Completeness and decidability (Tarski): Since the models are exactly the planes over real closed fields, and RCF is complete, the geometry is complete: every sentence in the language of B and ≡ is provable or refutable. Since RCF is decidable, so is the geometry — the two are bi-interpretable, and the decision procedure for elementary geometry is the decision procedure for RCF. Consistency follows: ℝ² is a model.

Not finitely axiomatizable: the continuity schema is essential and cannot be replaced by finitely many first-order axioms. Dropping it gives the theory of planes over arbitrary Pythagorean/Euclidean ordered fields, which is incomplete.

Contrast with Hilbert (1899): Hilbert's primitives: points, lines, planes; incidence, betweenness, two congruence relations. Hilbert's continuity axioms (Archimedes, line completeness) quantify over sets or over ℕ — second-order. His system is therefore categorical (up to the standard set-theoretic background) and not a first-order theory, so it is neither complete nor decidable in the relevant senses. Categoricity and decidability are alternatives here, and Tarski chose the second. Birkhoff (1932) takes ℝ as given and axiomatizes via a ruler and protractor — also not elementary.

Symbols.

Metatheory. The theory is consistent, complete, and decidable — Tarski's result, and the sharpest available answer to what geometry is, formally. The mechanism is the representation theorem plus RCF's completeness: geometry and real algebra are bi-interpretable, so every metatheoretic property transfers, in both directions and for free. The comparison with Hilbert is the substance: Hilbert's axioms are categorical because they are second-order, and second-order categoricity buys nothing effective, since the second-order consequence relation is not axiomatizable. Tarski's are first-order, hence not categorical — every real closed field gives a model, including countable ones — and hence complete and decidable. Incompleteness does not touch this theory: there is no interpretation of Q in it, because ℕ is not definable in a real closed field, which is the same fact that makes RCF decidable. The continuity schema is what forces real closure and it is also what makes the theory non-finitely-axiomatizable; both facts have the same source.

Applies to. Automated theorem proving in geometry — the Wu and Gröbner methods, and the direct CAD-based procedures, are RCF procedures applied through the bi-interpretation. Formal verification of geometric algorithms. Computational geometry over exact arithmetic. Foundations of geometry and the axiomatic method, which is Tarski's own framing. Mechanized reformalizations (the GeoCoq project formalizes SST in Coq). Constructive and intuitionistic geometry (Beeson), which modifies the base logic and is placed by that modification.

Limitations. Elementary only: no quantification over point sets, so continuity is a schema over definable sets and the theory cannot state the completeness of the line. Doubly exponential decision procedure, inherited from RCF, with a matching lower bound — decidability here is a theorem, not a tool, for anything beyond small problems. Not finitely axiomatizable and not categorical; a reader who wants ℝ² uniquely must go second-order and lose the decision procedure. The dimension is fixed by axiom, so each dimension is a different theory. Higher geometry — anything involving limits, curvature, or measure — is outside the language entirely.

© 2026 Lingenic LLC