Les axiomes de Tarsky

Axiom between_identity

forall A B, Bet A B A → A = B

Axiom cong_pseudo_reflexivity

forall A B, Cong A B B A

Axiom cong_identity

forall A B C, Cong A B C C → A = B

Axiom cong_inner_transitivity

forall A B C D E F, Cong A B C D → Cong A B E F → Cong C D E F.

Axiom inner_pasch

forall A B C P Q, Bet A P C → Bet B Q C → exists x, Bet P x B /\ Bet Q x A.

Axiom euclid

forall A B C D T,
Bet A D T → Bet B D C → A<>D → exists x, exists y, Bet A B x /\ Bet A C y /\ Bet x T y

Axiom five_segments

forall A A' B B' C C' D D',
Cong A B A' B' → Cong B C B' C' → Cong A D A' D' → Cong B D B' D' →
Bet A B C → Bet A' B' C' → A <> B → Cong C D C' D'

Axiom segment_construction

forall A B C D, exists E, Bet A B E /\ Cong B E C D

Axiom lower_dim

exists A, exists B, exists C, ~ Col A B C

Axiom upper_dim

forall A B C P Q,
P <> Q → Cong A P A Q → Cong B P B Q → Cong C P C Q → Col A B C

Axiom continuity

forall X Y → Prop,
(exists A, (forall x y, X x → Y y → Bet A x y)) → exists B, (forall x y, X x → Y y → Bet x B y)