The axioms of a Hilbert plane

HilbertPlane P L is a plane with points P and lines L, a betweenness, and congruence of segments and of angles, that meets Hilbert's axioms of incidence (I1 to I3), of order (B1 to B4, with Pasch's axiom as B4) and of congruence (C1 to C6). Playfair's axiom, HilbertPlane.Playfair, is not among them. The axioms of continuity are HilbertPlane.Archimedes and HilbertPlane.Dedekind.

Apart from Mathlib, this file is all that the statement of the main theorem, Hilbert.playfair_independent_continuous, depends on.

Contents

• the axioms: HilbertPlane, Collinear, OnRay, SameSide
• Playfair's axiom: HilbertPlane.Parallel, HilbertPlane.Playfair
• the axioms of continuity: HilbertPlane.Archimedes, HilbertPlane.Dedekind

def ParallelPostulate.Hilbert.Collinear {P : Type u_1} {L : Type u_2} (lies : P → L → Prop) (A B C : P) : Prop

Three points on one line.

Equations

• ParallelPostulate.Hilbert.Collinear lies A B C = ∃ (l : L), lies A l ∧ lies B l ∧ lies C l

def ParallelPostulate.Hilbert.OnRay {P : Type u_1} (btw : P → P → P → Prop) (A B C : P) : Prop

C is on the ray from A through B, and is not A.

Equations

• ParallelPostulate.Hilbert.OnRay btw A B C = (C = B ∨ btw A C B ∨ btw A B C)

def ParallelPostulate.Hilbert.SameSide {P : Type u_1} {L : Type u_2} (lies : P → L → Prop) (btw : P → P → P → Prop) (l : L) (A B : P) : Prop

A and B are on the same side of l: neither is on l, and no point of l is between them.

Equations

• ParallelPostulate.Hilbert.SameSide lies btw l A B = (¬lies A l ∧ ¬lies B l ∧ ¬∃ (C : P), lies C l ∧ btw A C B)

structure ParallelPostulate.Hilbert.HilbertPlane (P : Type u_3) (L : Type u_4) : Type (max u_3 u_4)

A Hilbert plane: Hilbert's axioms of incidence, order and congruence. A segment is a pair of points and an angle ABC is a triple with its vertex B in the middle; the fields seg_swap, ang_swap and ang_rays say that congruence does not see the order of the ends of a segment, the order of the two rays of an angle, or the points chosen on the rays.

• lies : P → L → Prop

  The point lies on the line.

• btw : P → P → P → Prop

  btw A B C: B is between A and C.

• segCong : P → P → P → P → Prop

  segCong A B C D: the segment AB is congruent to the segment CD.

• angCong : P → P → P → P → P → P → Prop

  angCong A B C D E F: the angle ABC, at B, is congruent to the angle DEF, at E.

• I1 (A B : P) : A ≠ B → ∃! l : L, self.lies A l ∧ self.lies B l
• I2 (l : L) : ∃ (A : P), ∃ (B : P), A ≠ B ∧ self.lies A l ∧ self.lies B l
• I3 : ∃ (A : P), ∃ (B : P), ∃ (C : P), ¬Collinear self.lies A B C
• B1 (A B C : P) : self.btw A B C → A ≠ B ∧ B ≠ C ∧ A ≠ C ∧ Collinear self.lies A B C ∧ self.btw C B A
• B2 (A B : P) : A ≠ B → ∃ (C : P), self.btw A B C
• B3 (A B C : P) : A ≠ B → B ≠ C → A ≠ C → Collinear self.lies A B C → (self.btw A B C ∨ self.btw B A C ∨ self.btw A C B) ∧ ¬(self.btw A B C ∧ self.btw B A C) ∧ ¬(self.btw A B C ∧ self.btw A C B) ∧ ¬(self.btw B A C ∧ self.btw A C B)
• B4 (A B C : P) (l : L) : ¬Collinear self.lies A B C → ¬self.lies A l → ¬self.lies B l → ¬self.lies C l → (∃ (D : P), self.lies D l ∧ self.btw A D B) → ∃ (E : P), self.lies E l ∧ (self.btw A E C ∨ self.btw B E C)
• seg_swap (A B : P) : self.segCong A B B A
• ang_swap (A B C : P) : self.angCong A B C C B A
• ang_rays (A B C A' C' : P) : OnRay self.btw B A A' → OnRay self.btw B C C' → self.angCong A B C A' B C'
• C1 (A B C R : P) : A ≠ B → C ≠ R → ∃! D : P, OnRay self.btw C R D ∧ self.segCong A B C D
• C2 (A B C D E F : P) : self.segCong A B C D → self.segCong A B E F → self.segCong C D E F
• C2_refl (A B : P) : self.segCong A B A B
• C3 (A B C D E F : P) : self.btw A B C → self.btw D E F → self.segCong A B D E → self.segCong B C E F → self.segCong A C D F
• C4 (A B C D F G : P) (l : L) : ¬Collinear self.lies A B C → D ≠ F → self.lies D l → self.lies F l → ¬self.lies G l → (∃ (E : P), SameSide self.lies self.btw l E G ∧ self.angCong A B C E D F) ∧ ∀ (E E' : P), SameSide self.lies self.btw l E G → self.angCong A B C E D F → SameSide self.lies self.btw l E' G → self.angCong A B C E' D F → OnRay self.btw D E E'
• C5 (A B C D E F G H I : P) : self.angCong A B C D E F → self.angCong A B C G H I → self.angCong D E F G H I
• C5_refl (A B C : P) : self.angCong A B C A B C
• C6 (A B C D E F : P) : ¬Collinear self.lies A B C → ¬Collinear self.lies D E F → self.segCong A B D E → self.segCong A C D F → self.angCong B A C E D F → self.segCong B C E F ∧ self.angCong A B C D E F ∧ self.angCong A C B D F E

def ParallelPostulate.Hilbert.HilbertPlane.Parallel {P : Type u_1} {L : Type u_2} (H : HilbertPlane P L) (l m : L) : Prop

Two lines are parallel when they have no point in common.

Equations

• H.Parallel l m = ¬∃ (A : P), H.lies A l ∧ H.lies A m

def ParallelPostulate.Hilbert.HilbertPlane.Playfair {P : Type u_1} {L : Type u_2} (H : HilbertPlane P L) : Prop

Playfair's axiom: through a point that is not on a line there is at most one line parallel to it.

Equations

• H.Playfair = ∀ (l : L) (A : P), ¬H.lies A l → ∀ (m m' : L), H.lies A m → H.Parallel m l → H.lies A m' → H.Parallel m' l → m = m'

def ParallelPostulate.Hilbert.HilbertPlane.Archimedes {P : Type u_1} {L : Type u_2} (H : HilbertPlane P L) : Prop

Archimedes' axiom. Laid off one after the other along the ray from A through B, starting at A, enough copies of a segment CD reach B or pass it.

Equations

• One or more equations did not get rendered due to their size.

def ParallelPostulate.Hilbert.HilbertPlane.Dedekind {P : Type u_1} {L : Type u_2} (H : HilbertPlane P L) : Prop

Dedekind's axiom. Split the points of a line into two parts, neither empty, so that no point of either part is between two points of the other. Then there is one point, and only one, that is between every point of the one part and every point of the other, unless it is one of them.

Equations

• One or more equations did not get rendered due to their size.