Les axiomes de Tarsky

Axiom between_identity

∀ A B, Bet A B A → A = B

Axiom cong_pseudo_reflexivity

∀ A B : Point, A B ≡ B A

Axiom cong_identity

∀ A B C : Point, A B ≡ C C → A = B

Axiom cong_inner_transitivity

∀ A B C D E F : Point, A B ≡ C D → A B ≡ E F → C D ≡ E F.

Axiom inner_pasch

∀ A B C P Q : Point, Bet A P C → Bet B Q C → ∃ x, Bet P x B /\ Bet Q x A.

Axiom euclid

∀ A B C D T : Point,
Bet A D T → Bet B D C → A<>D →
∃ x, ∃ y, Bet A B x /\ Bet A C y /\ Bet x T y

Axiom five_segments

∀ A A' B B' C C' D D' : Point,
A B ≡ A' B' → B C ≡ B' C' → A D ≡ A' D' → B D ≡ B' D' →
Bet A B C → Bet A' B' C' → A <> B → C D ≡ C' D'

Axiom segment_construction

∀ A B C D : Point, ∃ E : Point, Bet A B E /\ B E ≡ C D

Axiom lower_dim

∃ A, ∃ B, ∃ C, ~ Col A B C

Axiom upper_dim

∀ A B C P Q : Point, P <> Q → A P ≡ A Q → B P ≡ B Q → C P ≡ C Q → Col A B C

Axiom continuity

∀ X Y : Point → Prop,
(∃ A : Point, (∀ x y : Point, X x → Y y → Bet A x y)) →
∃ B : Point, (∀ x y : Point, X x → Y y → Bet x B y)