Nuprl Definition : euclidean-axioms

Twelve axioms about a 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
betweeness.⋅

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].  a = 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 x = 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 x = 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|

                                                                                             aq=ay

                                                                                             ∧ (¬(q = p ∈ Point))} ].

       let uv = intersect pq (at radius xy) with Oab  in
           afst(uv)=ab
           ∧ 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: b supposing a, uall: ∀[x:A]. B[x], pi1: fst(t), pi2: snd(t), not: ¬A, and: P ∧ Q, set: {x:A| B[x]} , equal: s = 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: b supposing a, eu-between-eq: a_b_c, equal: s = 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

Latex:
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 afst(uv)=ab \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