The Axioms

We now move onto examining the 11 axioms (10 singular, one axiom schema) of Tarskian geometry! All axioms should be read as universal closures.

The first three axioms concern the congruence relation.

ImportantA1 (Reflexivity of Congruence)

ab \equiv ba

ImportantA2 (Transitivity of Congruence)

(ab \equiv cd \land ab \equiv ef) \implies cd \equiv ef

ImportantA3 (Identity of congruence)

ab \equiv cc \implies a = b

The next axiom concerns segment construction.

ImportantA4 (Segment Construction)

\exists x (Bqax \land ax \equiv bc)

Informally, this axiom says that given any point a, there exists a point x (in the direction of q) such that ax has length bc. It will allow us to construct line segments of arbitrary length at an arbitrary angle.

The following axiom allows us to reason about triangle congrunce.

ImportantA5 (Five-segments Axiom)

\begin{align*} (a \not = b \land Babc \land Ba^\prime b^\prime c^\prime \land ab \equiv a^\prime b^\prime \land bc \equiv b^\prime c^\prime \\ \land \,\, ad \equiv a^\prime d^\prime \land bd \equiv b^\prime d^\prime) \implies cd \equiv c^\prime d^\prime \end{align*}

Say we have two triangles adc and a^\prime d^\prime c^\prime, and we take a point c inbetween a and b and draw a line segment dc giving us the following figure [INSERT FIGURE] consisting of five segments. This axiom states that if four of the segments on one triangle are each congruent to their respective segment on the other triangle, the fifth segments must be congruent.

This axiom is equivalent to the more standard side angle side congruency between triangles, and is the only axiom allowing us to show the congruence of two line segments from a different direction. [EXPAND]

The next two axioms concern the betweenness relation.

ImportantA6 (Identity of Betweenness)

Baba \implies a = b

This one is pretty simple, intuitively the only point on the line segment aa is a itself.

ImportantA7 (Pasch’s axiom)

(Bapc \land Bbqc) \implies \exists x (Bpxb \land Bqxa)

Shows lines through a vertex intersect inside a triangle. [EXPAND]

ImportantA8 (Lower dimension)

\exists a \exists b \exists c (\lnot Babc \land \lnot Bbca \land \lnot Bcab)

This axiom says that there exist three points which are not collinear, and provides a lower bound for the dimension of our geometrical space. Without this axiom, we could model our theory with a single line or point!

ImportantA9 (Upper dimension)

(p \not = q \land ap \equiv aq \land bp \equiv bq \land cp \equiv cq) \implies ( Babc \land Bbca \land Bcab)

Like the previous axiom, this axiom gives an upper bound on the dimension of our space. This axiom states that given points p and q, if three points a,b,c are all equidistant from p and q, then a,b,c are collinear. This along with the other axiom ensure that we are working in two dimensional space.

ImportantA10 (Euclids axiom)

(Badt \land Bbdc \land a \not = d) \implies \exists x \exists y (Babx \land Bacy \land Bxty)

We can visualize this by imagining at and bc as line segments intersecting at d. Then we have an angle \angle bac. Then we can create a line segment xy including t, and intersecting both sides of the angle. This, intersetingly enough, is equivalent to Euclids parallel postulate!

Next we have our final (infinitely many) axioms, the axiom schema of continuity.

ImportantA11 (Continuity axiom)

Let \alpha(x) and \beta(y) be formulas such that a,b are not free. Additionally, let y not be free in \alpha and x not be free in \beta. Then each instance of the following is an axiom. \exists a \forall x \forall y (\alpha(x) \land \beta(y) \implies Baxy) \implies \exists b \forall x \forall y(\alpha(x) \land \beta(y) \implies Bxby)

This is a complicated one. It essentially constructs dedekind cuts over a ray, without quantifying over sets of points.