2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Anonymous Jun 2 at 18:19
1
$\begingroup$

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$.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Anonymous Jun 2 at 18:35
1
$\begingroup$

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$.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.