I'm working in Hilbert's axioms of Euclidean plane geometry. I have problems with proving one thing concerning vectors. My definition of the vector is as follows:

Vector $\overrightarrow{ab}$ is an ordered pair of points $(a,b)$.

Now I define a relation between vectors $\overrightarrow{ab}$ and $\overrightarrow{cd}$:

If $a=b$ and $c=d$, the vectors are in relation.
If $a\neq b$ and $c=d$, the vectors are not in relation.
If $a=b$ and $c\neq d$, the vectors are not in relation.
If $a\neq b$ and $c\neq d$, the vectors are in relation if and only if all following conditions are true

  1. $|ab|=|cd|$.
  2. Lines $ab$ and $cd$ are parallel.

  3. a. If the lines $ab$ and $cd$ are equal, halfline $ab$ is contained in halfline $cd$ or halfline $cd$ is contained in halfline $ab$.
    b. If the lines $ab$ and $cd$ are disjoint, points $b$ and $d$ lie on the same side of the line $ac$ (in other words in the same halfplane whose border is line $ac$)

Now I want to prove this is an equivalence relation (equivalence classes would be free vectors). The problem is with transitivity in the case when all lines are disjoint. I need to prove:

Let $ab$, $cd$, $ef$ be parallel lines. $b$ and $d$ lie on the same side of the line $ac$, $d$ and $f$ lie on the same side of the line $ce$. Then $b$ and $f$ lie on the same side of the line $ae$.

  • $\begingroup$ At this point of the theory, do you have the notion of a line segment? If so, you may want to show (and use) the fact that the line segments $[ac]$ and $[ce]$ lie on the same side of the line $ae$. $\endgroup$ – paf Aug 25 '16 at 22:12
  • $\begingroup$ Yes, I have this notion and I know how to show this fact. But I still don't know how to prove the thesis. $\endgroup$ – Kulisty Aug 26 '16 at 8:21
  • $\begingroup$ Maybe the following 3-step-approach will lead to success: Step 1: Define a relation $\sim$ by $(a,b)\sim(c,d):\Leftrightarrow\exists v:a+v=c\ \land\ b+v=d $! Step 2: Prove that $\sim$ is an equivalence relation! (This is rather easy.) Step 3: Prove that the definition of $\sim$ is equivalent to your original definition! $\endgroup$ – Xaver Aug 27 '16 at 15:18
  • $\begingroup$ Yes, but how to define this addition? I can't add points. And I think there should be $a+v=b \wedge c+v=d$. $\endgroup$ – Kulisty Aug 28 '16 at 7:47

What you want to prove using Hilbert's axioms has been proved by Gabriel Braun using Tarski's axioms within GeoCoq (the proofs have been checked by a machine).

The definitions of equality of vectors which seems to be equivalent to yours, can be found here: https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Definitions.v In Coq's syntax: Definition EqV A B C D := Parallelogram A B D C / A = B /\ C = D.

Then you can find the proofs that it is an equivalence relation here: https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Annexes/vectors.v It relies on a property of parallelograms that Gabriel Braun has proved in Coq and described in french here: http://gabrielbraun.free.fr/Geometry/Tarski/plg_pseudo_trans.html#/start

Tarski's axioms and Hilbert's axiom (excluding continuity axioms) are mutually interpretable, so the same proof can be done using Hilbert's axioms.

| cite | improve this answer | |

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.