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.