Library GeoCoq.Axioms.makarios_variant_axioms

We describe here a variant of the axiom system proposed by T.J.M. Makarios in June 2013. This variant has a slightly different five_segment axioms and allows to remove the cong_pseudo_reflexivity axiom. All axioms have been shown to be independent except cong_identity and inner_pasch.

Class Tarski_neutral_dimensionless_variant := {
MTpoint : Type;
BetM : MTpoint → MTpoint → MTpoint → Prop;
CongM : MTpoint → MTpoint → MTpoint → MTpoint → Prop;
Mpoint_equality_decidability : ∀ A B : MTpoint, A = B ∨ ¬ A = B;
Mcong_identity : ∀ A B C, CongM A B C C → A = B;
Mcong_inner_transitivity : ∀ A B C D E F,
   CongM A B C D → CongM A B E F → CongM C D E F;
Msegment_construction : ∀ A B C D,
   ∃ E, BetM A B E ∧ CongM B E C D;
Mfive_segment : ∀ A A' B B' C C' D D',
   CongM A B A' B' →
   CongM B C B' C' →
   CongM A D A' D' →
   CongM B D B' D' →
   BetM A B C → BetM A' B' C' → A ≠ B →
   CongM D C C' D';
Mbetween_identity : ∀ A B, BetM A B A → A = B;
Minner_pasch : ∀ A B C P Q,
   BetM A P C → BetM B Q C →
   ∃ X, BetM P X B ∧ BetM Q X A;
MPA : MTpoint;
MPB : MTpoint;
MPC : MTpoint;
Mlower_dim : ¬ (BetM MPA MPB MPC ∨ BetM MPB MPC MPA ∨ BetM MPC MPA MPB )
}.