Metric Geometry – Constructing an Equilateral Triangle Using Tarski’s Axioms

euclidean-geometrymg.metric-geometrytriangles

In Euclid's first geometry proposition, he constructs an equilateral triangle given an arbitrary line segment. I was wondering if it was possible to prove this straight from Tarski's axioms for geometry (see https://en.wikipedia.org/wiki/Tarski%27s_axioms). This amounts to proving the following statement:

Given points $a,b$ prove that there exists a point $x$ such that $ax\equiv ab$ and $bx\equiv ab$.

Euclid's reasoning behind this is that the two circles centered at $a$ and $b$ with radius $ab$ "obviously" intersect. More generally we could ask whether we could formally prove if any two circles that "obviously" intersect at two points actually do so, given by the following statement:

Given points $a,b,c,d$ such that $Babc$ and $Bbcd$ prove that there exists a point $x$ such that $ax\equiv ac$ and $dx\equiv db$.

I am not really sure on how to get a nontrivial point (meaning not some arbitrary point) outside of the line that $a,b,c,d$ lie in.

Best Answer

Here is one way to construct an equilateral triangle on $p$ and $q$ using Tarski's axioms -- i.e. combining the existential axioms to get the vertex of such a triangle, omitting the proof by the other axioms that this works.

Let $vw\ge xy$ abbreviate $\exists z(Bxyz \wedge vw = xz)$.

enter image description here

By Lower Dimension, there are $a,b,c$ which are not collinear. Assume without loss of generality that $c$ is not on the line between $p$ and $q$, and that $cp \ge cq$.

By Continuity, choose $m$ with $Bpmq$ and $mp=mq$.

By Continuity, choose $d$ with $Bcdp$ and $dp=dq$.

By Segment Construction, choose $e$ with $Bmde$ and $de=pq$.

By Continuity, choose $t$ with $Bmte$ and $pt=pq$.

For all these uses of Continuity, the axiom actually requires a pair of inequalities rather than an equality. So for the last line, we can let $\phi(x) = Bmxe \wedge px \le pq$, and $\psi(y)=Bmye \wedge py \ge pq$, and use the continuity axiom in the form $$\forall x\, \forall y\,[(\phi(x) \wedge \psi(y)) \to Bmxy]\, \to\, \exists t\, \forall x\, \forall y\,[(\phi(x) \wedge \psi(y)) \to Bxty]$$ The other uses of the continuity axiom are similar.

Related Question