Library hilbert_axioms

Module Type HilbertLanguage.

We need a notion of point and line.

Parameter Point : Set.
Parameter Line : Set.

An incidence relation

Parameter Incid : Point -> Line -> Prop.

Two egalities

Parameter EqP : Point -> Point -> Prop.
Parameter EqL : Line -> Line -> Prop.

Axiom EqP_transitivity : forall l m n, EqP l m -> EqP m n -> EqP l n.
Axiom EqP_reflexivity : forall l, EqP l l.
Axiom EqP_symmetry : forall l m, EqP l m -> EqP m l.

Axiom EqL_transitivity : forall l m n, EqL l m -> EqL m n -> EqL l n.
Axiom EqL_reflexivity : forall l, EqL l l.
Axiom EqL_symmetry : forall l m, EqL l m -> EqL m l.

Axiom EqL_compat_incid : forall A l m, EqL l m -> Incid A l -> Incid A m.
Axiom EqP_compat_incid : forall A B l, EqP A B -> Incid A l -> Incid B l.

Definition Col A B C := exists l : Line, Incid A l /\ Incid B l /\ Incid C l.

Parameter Bet : Point -> Point -> Point -> Prop.

End HilbertLanguage.

Module Type HilbertIncidence.

Declare Module Export HilbertL : HilbertLanguage.

For every pair of distinct points there is a line containing them.

Axiom line_existence : forall A B, A<>B -> exists l, Incid A l /\ Incid B l.

There is only one line going through two points

Axiom line_unicity : forall A B l m, A <> B ->
Incid A l -> Incid B l -> Incid A m -> Incid B m -> EqL l m.

Every line contains at least two points

Axiom two_points_on_line : forall l,
exists A, exists B, Incid B l /\ Incid A l /\ A <> B.

There exists three non collinear points

Axiom plan : exists A, exists B, exists C, ~ Col A B C.

End HilbertIncidence.

Module Type HilbertOrder.

Declare Module Export HilbertL : HilbertLanguage.

Axiom between_col :
forall A B C : Point, Bet A B C ->Col A B C.

Axiom between_comm : forall A B C : Point, Bet A B C -> Bet C B A.

Axiom between_out :
forall A B : Point, A <> B -> exists C : Point, Bet A B C.

Axiom between_only_one :
forall A B C : Point,
Bet A B C -> ~ Bet B C A /\ ~ Bet B A C.

Axiom between_one : forall A B C,
A<>B -> A<>C -> B<>C -> Col A B C ->
Bet A B C \/ Bet B C A \/ Bet B A C.

Definition go_through := fun l A B => exists C, Incid C l /\ Bet A C B.

Axiom Pasch : forall A B C l,
~Col A B C -> ~ Incid A l -> ~ Incid B l -> ~ Incid C l ->
go_through l A B ->
(go_through l A C /\ ~go_through l B C) \/
(go_through l B C /\ ~ go_through l A C).

End HilbertOrder.

Module Type HilbertCongruence.

Declare Module Export HilbertL : HilbertLanguage.

Parameter Cong : Point -> Point -> Point -> Point -> Prop.

Axiom cong_pseudo_transitivity : forall A B C D E F,
   Cong A B C D -> Cong A B E F -> Cong C D E F.

Axiom cong_reflexivity : forall A B, Cong A B A B.

Axiom addition : forall A B C D E F,
  Bet A B C -> Bet D E F ->
  Cong A B D E -> Cong B C E F -> Cong A C D F.

Axiom point_construction_existence : forall A B C D,
C<>D -> exists X, (Bet C X D \/ Bet C D X) /\ Cong C X A B.

Axiom point_construction_unicity : forall A B C D X1 X2,
C<>D ->
Bet C X1 D \/ Bet C D X1 -> Cong C X1 A B ->
Bet C X2 D \/ Bet C D X2 -> Cong C X2 A B ->
EqP X1 X2.
End HilbertCongruence.

Module Type Hilbert.
Declare Module Export HilbertL : HilbertLanguage.

Axiom line_existence : forall A B, A<>B -> exists l, Incid A l /\ Incid B l.

Axiom line_unicity : forall A B l m, A <> B ->
Incid A l -> Incid B l -> Incid A m -> Incid B m -> EqL l m.

Axiom two_points_on_line : forall l,
  exists A, exists B, Incid B l /\ Incid A l /\ A <> B.

Axiom plan : exists A, exists B, exists C, ~ Col A B C.

Axiom between_col : forall A B C : Point, Bet A B C -> Col A B C.

Axiom between_comm : forall A B C : Point, Bet A B C -> Bet C B A.

Axiom between_out :
forall A B : Point, A <> B -> exists C : Point, Bet A B C.

Axiom between_only_one :
forall A B C : Point, Bet A B C -> ~ Bet B C A /\ ~ Bet B A C.

Axiom between_one : forall A B C,
A<>B -> A<>C -> B<>C -> Col A B C ->
Bet A B C \/ Bet B C A \/ Bet B A C.

Definition go_through := fun l A B => exists C, Incid C l /\ Bet A C B.

Axiom Pasch : forall A B C l,
~Col A B C -> ~ Incid A l -> ~ Incid B l -> ~ Incid C l ->
go_through l A B ->
(go_through l A C /\ ~go_through l B C) \/
(go_through l B C /\ ~ go_through l A C).

Parameter Cong : Point -> Point -> Point -> Point -> Prop.

Axiom cong_pseudo_transitivity : forall A B C D E F,
   Cong A B C D -> Cong A B E F -> Cong C D E F.

Axiom cong_reflexivity : forall A B, Cong A B A B.

Axiom addition : forall A B C D E F,
  Bet A B C -> Bet D E F ->
  Cong A B D E -> Cong B C E F -> Cong A C D F.

Axiom point_construction_existence : forall A B C D,
C<>D -> exists X, (Bet C X D \/ Bet C D X) /\ Cong C X A B.

Axiom point_construction_unicity : forall A B C D X1 X2,
C<>D ->
Bet C X1 D \/ Bet C D X1 -> Cong C X1 A B ->
Bet C X2 D \/ Bet C D X2 -> Cong C X2 A B ->
EqP X1 X2.

End Hilbert.

Module Type HilbertParallels.

Declare Module Export HilbertL : HilbertLanguage.

Parameter Par : Point -> Point -> Point -> Point -> Prop.
Axiom euclid_existence : forall A B P,
exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.

Axiom euclid_unicity : forall A B P C1 D1 C2 D2,
~ Col P A B ->
Par A B C1 D1 -> Col P C1 D1 ->
Par A B C2 D2 -> Col P C2 D2 ->
Col C1 C2 D2 /\ Col D1 C2 D2.

End HilbertParallels.