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.
With all due respect, and acknowledgement of the great things that I, and others, have learned from you, I cannot agree that Tarski’s approach to geometry is superior to traditional approaches. Abstraction, elegance, and brevity are important aspects of math – perhaps essential…but those more “cumbersome” tools are useful for helping people to find their own cognitive journey to the brevity, abstraction, and elegance that is the beauty of math. Drawing diagrams with straight-edge and compass, as well as many other constructivist activities, leads to intuition about geometry that is rooted in physicality. A growing chorus claims that math is rooted in the embodied mind, and one should not pretend otherwise, unless he/she is prepared to make the Platonic argument or invoke God.
The Tarski stuff you present makes my eyes bloodshot. Geometry, at its best, is a feast for the eyes as well as the mind.
Perhaps there are people who are using Tarski as a foundation for a constructivist pedagogy for learning geometry – in which case, the end-result might be ultimately better than if Euclid were used as a foundation. But there needs to be a constructivist ladder for the explorer to climb. The majority of people on Earth will not grow up to become professional mathematicians. I counter that the Tarski stuff is pointless (a term you applied to Euclid) for the majority of people on this planet, who can (and must) apply experiential geometry in their professional lives.
-Jeffrey Ventrella
I believe there is a slight tone of joke in this whole article – I really doubt author would like to do all the geometry in such technical terms. Especially that it seems like he doesn’t want to use logical symbols like or, and, there exists.
There is also a downside of Tarski’s axioms – they are first order, so we can’t express stuff about arbitrary sets of points, e.g. “every bounded set of points has a convex hull”. If we wanted to have Tarski’s axioms to allow such statements, theory would become incomplete and undecidable.
Hmm, I hope you’re right about that.
If it was a joke, it sure was long and detailed.
Adam, in addition to not understanding much of your math, it seems I also don’t get your jokes.
Kudos!
-j
Wojowu is correct — this wasn’t intended to be taken entirely seriously.
By the way, at no point did I describe Euclid as pointless! He was the first mathematician to introduce an axiomatic system (admittedly not entirely rigorous by modern standards), and therefore contributed immensely.
When I said `this is completely pointless’, I was merely bemoaning how young mathematicians rote-learn vast swathes of geometrical theorems in preparation for competitions.
My apologies for the misunderstanding.
Cool – now I feel okay about laughing at that last exercise 🙂
-j
Yes, that’s the correct response!
Incidentally, I believe I may now hold the record for the most consecutive closing parentheses.
I believe there is a mistake in geometry axiom no. 3. Surely the inner formula should be:
(C(u, v, w, x) ⇒ (C(u, v, y, z) ⇒ C(w, x, y, z)))
and not:
((C(u, v, w, x) ⇒ C(u, v, y, z)) ⇒ C(w, x, y, z)).
Also, I couldn’t understand what the seventh axiom is about, although I suspect there may be some subtlety of the logic that I’m missing.
Thanks — you’re completely correct.
The seventh axiom is one of the most powerful! It means that we can take sups and infs of definable subsets of the real line, and therefore construct any algebraic number.
For instance, the cube-root of 7 is the sup of all positive reals x with the property that x^3 < 7.
Oh, yes, I see now. I had previously misread it as:
(∀w.((∀x.(∀y.(φ(x) ⇒ (ψ(y) ⇒ B(x, w, y))))) ⇒ ((∀z.((∀x.(∀y.(φ(x) ⇒ (ψ(y) ⇒ B(x, z, y))))) ⇒ ⊥)) ⇒ ⊥))).