For literally thousands of years, people have been writing books about elementary geometry. Many of these, such as Bradley and Gardiner’s *Plane Euclidean Geometry*, are concerned with solving problems in Euclidean geometry. They are subsequently bought by many adolescents intending to compete in the *International Mathematical Olympiad*.

This is completely pointless.

We shall instead explore Tarski’s cool, slender, axiomatic approach to geometry. This has numerous advantages over the cumbersome alternatives:

**Simplicity:** there are only three concepts, namely the idea of a ‘point’ and the relations of ‘betweenness’ and ‘congruence’. These could be understood by the entire populace of the Clapham omnibus.
**Brevity:** memorising hundreds of definitions, lemmas and theorems will provoke a reaction of ‘tl;dr‘ from all but the most hardened tediophiles. Fortunately, Tarski only has eleven axioms which rest on top of the seven axioms and two inference rules of first-order logic.
**Decidability:** we can algorithmically decide whether or not a statement is true, and provide a perfectly rigorous proof without all of that mucking about with diagram dependency.
**Innumeracy:** no arithmetic is required, let alone algebra.

So, without further ado, we shall introduce the framework. To make this entirely self-contained (and therefore giving geometry textbooks an unfair advantage, since they assume knowledge of concepts such as algebra) we shall include first-order logic here.

### Language

The language is an especially simple one, in that it is first-order and involves no function symbols. It is constructed inductively as follows:

**Variables** are typically written as lowercase letters, such as *x* and *y, *and understood to represent geometrical points. We allow the use of the prime symbol to enable an unbounded number of variables with a finite alphabet (such as *x*‘, *x*”, *x*”’, *x*”” and so on).
**Atomic formulae** are expressions of the following form (where *w*, *x*, *y*, *z* are variables):
- (
*x* = *y*), (read as ‘*x* and *y* are the same point’);
- B(
*x*, *y*, *z*), (read as ‘*y* lies on the line segment with endpoints *x* and *z*‘);
- C(
*w*, *x*, *y*, *z*), (read as ‘the distance between *w* and *x* is the same as the distance between *y* and *z*‘);
- ⊥, (read as ‘false’).

**Formulae** are constructed inductively in terms of atomic formulae:
- Every atomic formula is a formula;
- If P and Q are formulae, then so is (P ⇒ Q) (read as ‘P implies Q’);
- If
*x* is a variable and P is a formula, then (∀*x*.P) is a formula (read as ‘for all *x*, P is true’).

**Sentences** are formulae in which every variable is *bound* (every variable *x* is enclosed within the scope of a ∀*x *quantifier).

That is all.

### Axioms

Axioms are formulae which are assumed without proof. Firstly, we have seven logical axiom-schema:

**Axiom K:** for all formulae P and Q, the formula (P ⇒ (Q ⇒ P)) is an axiom.
**Axiom S:** for all formulae P, Q and R, the formula ((P ⇒ (Q ⇒ R)) ⇒ ((P ⇒ Q) ⇒ (P ⇒ R))) is an axiom.
**Double negative elimination:** for every formula P, the formula (((P ⇒ ⊥) ⇒ ⊥) ⇒ P) is an axiom.
**Reflexivity of equality:** for every variable *x*, the formula (∀*x*.(*x* = *x*)) is an axiom.
**Instantiation of equality:** if *x* and *y* are variables, and P is a formula not containing ∀*y*, then (∀*x*.(∀*y*.((*x* = *y*) ⇒ (P ⇒ P[*y*/*x*])))) is an axiom, where P[*y*/*x*] is the formula obtained by replacing every instance of *x* in the formula P with *y*.
**Universal instantiation:** if *x* and *y* are variables and P is a formula, then (∀*x*.(P ⇒ P[*y*/*x*])) is an axiom.
**Seventh axiom:** if *x* is a variable and P and Q are formulae, with *x* not occurring unbound in P, then ((∀*x*.(P ⇒ Q)) ⇒ (P ⇒ (∀*x*.Q))) is an axiom.

These are augmented with eleven geometric axioms:

**Reflexivity of congruence:** (∀*x*.(∀*y*.C(*x*, *y*, *y*, *x*))) is an axiom, which is logically equivalent to the symmetry property of metric spaces.
**Identity of congruence:** (∀*x*.(∀*y*.(∀*z*.(C(*x*, *y*, *z*, *z*) ⇒ (*x* = *y*))))), which is logically equivalent to another metric property.
**Transitivity of congruence:** (∀*u*.(∀*v*.(∀*w*.(∀*x*.(∀*y*.(∀*z*.(C(*u*, *v*, *w*, *x*) ⇒ (C(*u*, *v*, *y*, *z*) ⇒ C(*w*, *x*, *y*, *z*))))))))), which (together with reflexivity of congruence) implies that congruence of line segments is an equivalence relation.
**Identity of betweenness:** (∀*x*.(∀*y*.(B(*x*, *y*, *x*) ⇒ (*x* = *y*)))), which means that if a point lies on a degenerate line segment with equal endpoints, then it is the endpoints.
**Pasch’s axiom:** (∀*u*.(∀*v*.(∀*x*.(∀*y*.(∀*z*.(B(*x*, *u*, *z*) ⇒ (B(*y*, *v*, *z*) ⇒ ((∀*w*.(B(*u*, *w*, *y*) ⇒ (B(*v*, *w*, *x*) ⇒ ⊥))) ⇒ ⊥)))))))), which means that any two internal cevians intersect at a point.
**Existence of triangles:** ((∀*x*.(∀*y*.(∀*z*.((((B(*x*, *y*, *z*) ⇒ ⊥) ⇒ B(*y*, *z*, *x*)) ⇒ ⊥) ⇒ B(*z*, *x*, *y*))))) ⇒ ⊥), which forces the geometry to be non-empty and at least two-dimensional.
**Continuity:** for any formulae φ(*x*) and ψ(*y*), each with only one free variable, we have the axiom (∀*w*.((∀*x*.(∀*y*.(φ(*x*) ⇒ (ψ(*y*) ⇒ B(*w*, *x*, *y*))))) ⇒ ((∀*z*.((∀*x*.(∀*y*.(φ(*x*) ⇒ (ψ(*y*) ⇒ B(*x*, *z*, *y*))))) ⇒ ⊥)) ⇒ ⊥))), which means that we can construct a point given by a Dedekind cut whose sets are definable subsets of a ray.
**Five segment:** (∀*u*.(∀*x*.(∀*y*.(∀*z*.(∀*u**‘*.(∀*x’*.(∀*y’*.(∀*z’*.(((*x* = *y*) ⇒ ⊥) ⇒ (B(*x*, *y*, *z*) ⇒ (B(*x*‘, *y*‘, *z*‘) ⇒ (C(*y*, *x*, *y*‘, *x*‘) ⇒ (C(*y*, *z*, *y*‘, *z*‘) ⇒ (C(*u*, *x*, *u*‘, *x*‘) ⇒ (C(*u*, *y*, *u*‘, *y*‘) ⇒ C(*u*, *z*, *u*‘, *z*‘)))))))))))))))), which means that a triangle with an extended edge is rigid.
**Segment construction:** (∀*u*.(∀*v*.(∀*x*.(∀*y*.((∀*z*.(B(*x*, *y*, *z*) ⇒ (C(*y*, *z*, *u*, *v*) ⇒ ⊥))) ⇒ ⊥))))), which means that we can construct the other endpoint of a segment with a specified endpoint, length and direction.
**Euclid’s axiom:** To forbid hyperbolic geometry, introduce the axiom (∀*u*.(∀*v*.(∀*x*.(∀*y*.(∀*z*.(((*x* = *u*) ⇒ ⊥) ⇒ (B(*x*, *u*, *v*) ⇒ (B(*y*, *u*, *z*) ⇒ ((∀*a*.(∀*b*.(B(*x*, *y*, *a*) ⇒ (B(*a*, *v*, *b*) ⇒ (B(*b*, *z*, *x*) ⇒ ⊥))))) ⇒ ⊥))))))))), which is equivalent to the parallel postulate.
**All points are coplanar:** To forbid higher-dimensional geometry, introduce the axiom (∀*u*.(∀*v*.(∀*x*.(∀*y*.(∀*z*.(((*u* = *v*) ⇒ ⊥) ⇒ (C(*u*, *x*, *v*, *x*) ⇒ (C(*u*, *y*, *v*, *y*) ⇒ (C(*u*, *z*, *v*, *z*) ⇒ ((B(*z*, *x*, *y*) ⇒ ⊥) ⇒ ((B(*y*, *z*, *x*) ⇒ ⊥) ⇒ B(*x*, *y*, *z*)))))))))))), which means that the perpendicular bisector of two given distinct points is a line.

### Rules of inference

A theorem is a formula that is provably true. In order to assign truth to formulae, we are allowed the following rules of inference:

- Every axiom is automatically a theorem.
**Modus ponens:** If P and (P ⇒ Q) are theorems, then so is Q.
**Generalisation:** If P is a theorem, and *x* is a variable, then (∀*x*.P) is also a theorem.

Armed with these axioms and rules of inference, we can prove many theorems in geometry. It is a remarkable fact (known as *completeness*), first established by Alfred Tarski, that if P is a sentence then either P is a theorem or its negation (P ⇒ ⊥) is a theorem. This is really awesome, since it leads to the following corollary:

**Decidability of geometry:** We can decide whether a sentence in geometry is true or false, simply by exhaustively proving things until we establish either the sentence or its negation as a theorem.

The theory of algebraically-closed fields of characteristic 0 is also decidable (Lefschetz principle), as is the first-order theory of the reals (also proved by Tarski, and used as a lemma in proving that geometry is decidable). Peano arithmetic is undecidable, a fact known as Gödel’s *Incompleteness Theorem*.

We are now ready to prove things using this system. Here’s a simple problem:

**Exercise 1 (triangle inequality):** Prove (∀*a*.(∀*b*.(∀*x*.(∀*y*.(∀*z*.(C(*x*, *z*, *x*, *a*) ⇒ (C(*y*, *z*, *y*, *b*) ⇒ (B(*x*, *y*, *a*) ⇒ (B(*x*, *y*, *b*) ⇒ B(*x*, *a*, *b*)))))))))) using the Tarski axioms together with the rules of inference.

If you found that too easy, here’s a slightly more challenging one:

**Exercise 2 (question 6, IMO 2011):** Prove (∀*a*.(∀*b*.(∀*c*.(∀*d*.(∀*a*‘.(∀*b*‘.(∀*c*‘.(∀*o*‘.(∀*o*.(∀*p*.(∀*q*.(∀*r*.(∀*s*.(∀*t*.(∀*u*.(∀*v*.(C(*o*, *a*, *o*, *b*) ⇒ (C(*o*, *b*, *o*, *c*) ⇒ (C(*o*, *c*, *o*, *d*) ⇒ (C(*o*, *d*, *d*, *p*) ⇒ (B(*o*, *d*, *p*) ⇒ (C(*q*, *a*, *o*, *a*) ⇒ (C(*r*, *a*, *p*, *a*) ⇒ (C(*q*, *a*‘, *r*, *a*‘) ⇒ (C(*q*, *b*, *o*, *b*) ⇒ (C(*r*, *b*, *p*, *b*) ⇒ (C(*q*, *b*‘, *r*, *b*‘) ⇒ (C(*s*, *b*, *o*, *b*) ⇒ (C(*t*, *b*, *p*, *b*) ⇒ (C(*s*, *b’*, *t*, *b’*) ⇒ (C(*s*, *c*, *o*, *c*) ⇒ (C(*t*, *c*, *p*, *c*) ⇒ (C(*s*, *c**‘*, *t*, *c**‘*) ⇒ (C(*u*, *c*, *o*, *c*) ⇒ (C(*v*, *c*, *p*, *c*) ⇒ (C(*u*, *c’*, *v*, *c’*) ⇒ (C(*u*, *a*, *o*, *a*) ⇒ (C(*v*, *a*, *p*, *a*) ⇒ (C(*u*, *a**‘*, *v*, *a**‘*) ⇒ (((*q* = *o*) ⇒ ⊥) ⇒ (((*r* = *p*) ⇒ ⊥) ⇒ (((*s* = *o*) ⇒ ⊥) ⇒ (((*t* = *p*) ⇒ ⊥) ⇒ (((*u* = *o*) ⇒ ⊥) ⇒ (((*v* = *p*) ⇒ ⊥) ⇒ (C(*o*‘, *a*‘, *o*‘, *b*‘) ⇒ (C(*o*‘, *c*‘, *o*‘, *b*‘) ⇒ ((∀*z*.(C(*o*, *z*, *o*, *a*) ⇒ (C(*o*‘, *z*, *o*‘, *a*‘) ⇒ ((((B(*o*, *o*‘, *z*) ⇒ ⊥) ⇒ B(*o*‘, *z*, *o*)) ⇒ ⊥) ⇒ B(*z*, *o*, *o*‘))))) ⇒ ⊥)))))))))))))))))))))))))))))))))))))))))))))))) using the Tarski axioms together with the rules of inference.