# Do Tarski's (geometry) axioms imply that all zero segments are congruent?

Tarski's axioms are an alternate formalization of geometry (similar to axiom sets of Euclid and later Hilbert). Do these axioms imply: $$\forall\; x,y\in \text{points},\; x x\equiv y y?$$

If yes, what is the proof? My feeling is that the proof must use Tarski's Identity of Congruence $$xy\equiv zz \rightarrow x = y,$$ but I am unable to find a proof.

• The Identity of Congruence won't give it to you using since congruence is an assumption, not a conclusion, of that axiom. I will show how to prove it using the segment construction axiom and axiom of Euclid an a full answer. – Anonymous Jun 2 at 18:19

This seems surprisingly tricky. Identity of Congruence isn't enough by itself since it goes in the wrong direction.

I want to use the Five Segment Axiom. Let me call your two points $$p,q$$ instead, to avoid a conflict with Wikipedia's notation. If $$p=q$$ then we are done by reflexivity, so assume $$p \ne q$$. Set $$u=z=x'=p$$ and $$u'=z'=x=q$$. Let $$y=y'$$ be the midpoint of $$pq$$ (it takes some more work to prove that it exists), so $$Bpyq$$ and $$py \equiv qy$$. Now we verify that the hypothesis of the Five Segment Axiom is satisfied, and conclude $$zu \equiv z'u'$$ which is to say $$pp \equiv qq$$.

• I like this solution. I found a proof using Euclid's axiom which didn't require proving the existence of a midpoint but required some other facts to be proven. – Anonymous Jun 2 at 18:35

Let $$y$$ and $$v$$ be arbitrary. Let $$z=u=y$$ and $$w=v$$. By the segment construction axiom, there exists $$x$$ such that $$Bvyx$$ and $$yx=vy$$. Then, the hypothesis of the axiom of Euclid (form A using the same letters as I have used here) is satisfied, so we conclude $$yz\equiv vw$$. But indeed $$y=z$$ and $$v=w$$ so we have $$yy\equiv vv$$. Since $$y$$ and $$v$$ were arbitrary, we conclude $$\forall y\forall v (yy\equiv vv)$$.

I implicitly used a couple facts without stating which you should try to prove. Namely, $$Byyy$$ is a tautology, and $$Bvyx$$ iff $$Bxyv$$.

You do not need Euclid's axiom nor five segments, using segment construction build a point $$z$$ such that Bet yxz and xz=yy. Using identity of congruence, we have x=z.

The machine checked proof of this results and many other is available in the GeoCoq library, it the lemma cong_trivial_identity line 72 here: https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Ch02_cong.v