Axiom:Axiom of Triangle Existence

Axiom

Let $\equiv$ be the relation of equidistance.

Let $\mathsf{B}$ be the relation of betweenness.

Then the following axiom holds:

$\forall a,a',b,b',c',p: ab \equiv a'b' \implies$

$\exists c,x: \left({ac \equiv a'c' \land bc \equiv b'c' \land \mathsf{B}cxp}\right) \land \left({\mathsf{B}abx \lor \mathsf{B}bxa \lor \mathsf{B}xab}\right)$

where $a, b, c, a', b', c', x, p$ are points.

Intuition

Draw two congruent line segments, $ab$, $a'b'$.

Let the three points $a',c',b'$ form a triangle.

Pick any point $p$.

Then it is always possible to extend $p$ into some line segment $pc$ passing through segment $ab$ at a point $x$.

Further, it is possible to pick a point $c$ such that a triangle $abc$ is formed congruent to triangle $a'b'c'$.

Note that this axiom still holds in degenerate cases.

For example, if $\triangle{abc} = \triangle{a'b'c'}$ (where $=$ denotes logical equality), then this axiom may be interpreted as "it is possible to drop a line segment from the apex of a triangle passing through the base of the triangle".

This page needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code.

Sources

• June 1999: Alfred Tarski and Steven Givant: Tarski's System of Geometry (Bull. Symb. Log. Vol. 5, no. 2: pp. 175 – 214) : p. $187$ : Axiom $21$