Nuprl Definition : euclidean-axioms

Twelve axioms about EuclideanStructure 
give Beeson's constructive version of Tarski's axioms.
They are reflexivity, transitivity, and identity of congruence;
"segment extension"; the "five-segment axiom"; "trivial strict betweeness";
the "inner-Pasch" axiom; the "upper-dimension" axiom;
the "triangle circumscription axiom" (equivalent to the parallel postulate);
the "line-circle continuity axiom";  symmetry and "inner transitivity" of

euclidean-axioms(e) ==
  (∀[a,b:Point].  ab=ba)
  ∧ (∀[a,b,p,q,r,s:Point].  (pq=rs) supposing (ab=rs and ab=pq))
  ∧ (∀[a,b,c:Point].  b ∈ Point supposing ab=cc)
  ∧ (∀[q:Point]. ∀[a:{a:Point| ¬(q a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc))
  ∧ (∀[a,b,c,d,A,B,C,D:Point].
       (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (a b ∈ Point))))
  ∧ (∀[a,b:Point].  a-b-a))
  ∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
       let eu-inner-pasch(e;a;b;c;p;q) in
           p-x-b ∧ q-x-a)
  ∧ (∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (a b ∈ Point))))
  ∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let middle(a;b;c) in ax=bx ∧ ax=cx)
  ∧ (∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point| 
                                                                                             ∧ (q p ∈ Point))} ].
       let uv intersect pq (at radius xy) with Oab  in
           ∧ asnd(uv)=ab
           ∧ p_fst(uv)_q
           ∧ snd(uv)_p_q
           ∧ ¬((fst(uv)) (snd(uv)) ∈ Point) supposing ¬(x b ∈ Point))
  ∧ (∀[a,b,c:Point].  c-b-a supposing a-b-c)
  ∧ (∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d))

Definitions occuring in Statement :  eu-middle: middle(a;b;c) eu-line-circle: intersect pq (at radius xy) with Oab  eu-inner-pasch: eu-inner-pasch(e;a;b;c;p;q) eu-extend: (extend ab by cd) eu-between-eq: a_b_c eu-colinear: Colinear(a;b;c) eu-between: a-b-c eu-congruent: ab=cd eu-point: Point let: let uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) not: ¬A and: P ∧ Q set: {x:A| B[x]}  equal: t ∈ T
Definitions occuring in definition :  set: {x:A| B[x]}  uall: [x:A]. B[x] eu-point: Point and: P ∧ Q eu-between: a-b-c not: ¬A eu-congruent: ab=cd uimplies: supposing a eu-between-eq: a_b_c equal: t ∈ T eu-extend: (extend ab by cd) eu-colinear: Colinear(a;b;c) let: let eu-inner-pasch: eu-inner-pasch(e;a;b;c;p;q) eu-middle: middle(a;b;c) eu-line-circle: intersect pq (at radius xy) with Oab  pi1: fst(t) pi2: snd(t)
FDL editor aliases :  euclidean-axioms

euclidean-axioms(e)  ==
    (\mforall{}[a,b:Point].    ab=ba)
    \mwedge{}  (\mforall{}[a,b,p,q,r,s:Point].    (pq=rs)  supposing  (ab=rs  and  ab=pq))
    \mwedge{}  (\mforall{}[a,b,c:Point].    a  =  b  supposing  ab=cc)
    \mwedge{}  (\mforall{}[q:Point].  \mforall{}[a:\{a:Point|  \mneg{}(q  =  a)\}  ].  \mforall{}[b,c:Point].
              (q\_a\_(extend  qa  by  bc)  \mwedge{}  a(extend  qa  by  bc)=bc))
    \mwedge{}  (\mforall{}[a,b,c,d,A,B,C,D:Point].
              (cd=CD)  supposing  (bd=BD  and  ad=AD  and  bc=BC  and  ab=AB  and  A\_B\_C  and  a\_b\_c  and  (\mneg{}(a  =  b))))
    \mwedge{}  (\mforall{}[a,b:Point].    (\mneg{}a-b-a))
    \mwedge{}  (\mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].  \mforall{}[p:\{p:Point|  a-p-c\}  ].  \mforall{}[q:\{q:Point|  b\_q\_c\}  ]\000C.
              let  x  =  eu-inner-pasch(e;a;b;c;p;q)  in
                      p-x-b  \mwedge{}  q-x-a)
    \mwedge{}  (\mforall{}[a,b,p,q,r:Point].    (Colinear(p;q;r))  supposing  (ra=rb  and  qa=qb  and  pa=pb  and  (\mneg{}(a  =  b))))
    \mwedge{}  (\mforall{}[a,b:Point].  \mforall{}[c:\{c:Point|  \mneg{}Colinear(a;b;c)\}  ].    let  x  =  middle(a;b;c)  in  ax=bx  \mwedge{}  ax=cx)
    \mwedge{}  (\mforall{}[a,b:Point].  \mforall{}[x:\{x:Point|  a\_x\_b\}  ].  \mforall{}[y:\{y:Point|  a\_b\_y\}  ].  \mforall{}[p:\{p:Point|  ap=ax\}  ].
          \mforall{}[q:\{q:Point|  aq=ay  \mwedge{}  (\mneg{}(q  =  p))\}  ].
              let  uv  =  intersect  pq  (at  radius  xy)  with  Oab    in
                      \mwedge{}  asnd(uv)=ab
                      \mwedge{}  p\_fst(uv)\_q
                      \mwedge{}  snd(uv)\_p\_q
                      \mwedge{}  \mneg{}((fst(uv))  =  (snd(uv)))  supposing  \mneg{}(x  =  b))
    \mwedge{}  (\mforall{}[a,b,c:Point].    c-b-a  supposing  a-b-c)
    \mwedge{}  (\mforall{}[a,b,c,d:Point].    (a-b-c)  supposing  (b-c-d  and  a-b-d))

Date html generated: 2016_07_08-PM-06_29_45
Last ObjectModification: 2015_12_31-AM-10_41_22

Theory : euclidean!geometry

Home Index