Independence of the parallel postulate

ClassTarski's absolute plane geometry#✓fully proved

A model of Tarski's absolute plane geometry is a type \(M\) of points with a betweenness relation \(B\) and a congruence relation \(C\), where \(B(a, b, c)\) means that \(b\) lies between \(a\) and \(c\) (allowing \(b = a\) or \(b = c\)) and \(C(a, b, c, d)\) means that the segment \(ab\) is congruent to the segment \(cd\), satisfying the following axioms, in which unbound variables range over all points of \(M\) (axioms A1–A9 and A11 of Schwabhäuser–Szmielew–Tarski, that is, all of Tarski's axioms except the Euclidean axiom A10): (A1) \(C(a, b, b, a)\); (A2) if \(C(a, b, c, d)\) and \(C(a, b, e, f)\), then \(C(c, d, e, f)\); (A3) if \(C(a, b, c, c)\), then \(a = b\); (A4) there is a point \(x\) with \(B(a, b, x)\) and \(C(b, x, c, d)\); (A5) if \(a \ne b\), \(B(a, b, c)\), \(B(a', b', c')\), \(C(a, b, a', b')\), \(C(b, c, b', c')\), \(C(a, d, a', d')\) and \(C(b, d, b', d')\), then \(C(c, d, c', d')\); (A6) if \(B(a, b, a)\), then \(a = b\); (A7) if \(B(a, p, c)\) and \(B(b, q, c)\), then there is a point \(x\) with \(B(p, x, b)\) and \(B(q, x, a)\); (A8) there are points \(a, b, c\) such that none of \(B(a, b, c)\), \(B(b, c, a)\) and \(B(c, a, b)\) holds; (A9) if \(p \ne q\), \(C(p, a, q, a)\), \(C(p, b, q, b)\) and \(C(p, c, q, c)\), then \(B(a, b, c)\), \(B(b, c, a)\) or \(B(c, a, b)\); (A11) for all sets \(X, Y \subseteq M\), if there is a point \(a\) with \(B(a, x, y)\) for all \(x \in X\) and \(y \in Y\), then there is a point \(b\) with \(B(x, b, y)\) for all \(x \in X\) and \(y \in Y\).

MathlibExt.Geometry.ParallelPostulateWanted.Geometry.TarskiAbsolute · 35 lines

class TarskiAbsolute (M : Type*) where
  /-- Betweenness: `B a b c` says `b` lies between `a` and `c` (collinear; the
  non-strict convention, allowing `b = a` or `b = c`). -/
  B : M → M → M → Prop
  /-- Congruence of segments: `C a b c d` says `ab` is congruent to `cd`. -/
  C : M → M → M → M → Prop
  /-- **A1** Reflexivity of congruence. -/
  congr_refl : ∀ a b, C a b b a
  /-- **A2** Transitivity of congruence. -/
  congr_trans : ∀ a b c d e f, C a b c d → C a b e f → C c d e f
  /-- **A3** Identity of congruence: a zero-length segment has equal endpoints. -/
  congr_id : ∀ a b c, C a b c c → a = b
  /-- **A4** Segment construction: any segment can be extended to match a given length. -/
  segment_construction : ∀ a b c d, ∃ x, B a b x ∧ C b x c d
  /-- **A5** Five-segment axiom (a substitute for SAS congruence). -/
  five_segment : ∀ a b c d a' b' c' d', a ≠ b →
    B a b c → B a' b' c' →
    C a b a' b' → C b c b' c' → C a d a' d' → C b d b' d' →
    C c d c' d'
  /-- **A6** Identity of betweenness. -/
  betw_id : ∀ a b, B a b a → a = b
  /-- **A7** Inner Pasch. -/
  inner_pasch : ∀ a b c p q, B a p c → B b q c → ∃ x, B p x b ∧ B q x a
  /-- **A8** Lower-dimension axiom: there exist three non-collinear points. -/
  lower_dim : ∃ a b c, ¬ B a b c ∧ ¬ B b c a ∧ ¬ B c a b
  /-- **A9** Upper-dimension axiom (2D): three points equidistant from two
  distinct points are collinear. -/
  upper_dim : ∀ a b c p q, p ≠ q → C p a q a → C p b q b → C p c q c →
    B a b c ∨ B b c a ∨ B c a b
  /-- **A11** Continuity (second-order form): if some point `a` precedes the
  whole of `Y` as seen from `X` — every `x ∈ X` lies between `a` and every
  `y ∈ Y` — then some point `b` lies between every `x ∈ X` and every
  `y ∈ Y`. -/
  continuity : ∀ X Y : Set M,
    (∃ a, ∀ x ∈ X, ∀ y ∈ Y, B a x y) → (∃ b, ∀ x ∈ X, ∀ y ∈ Y, B x b y)

Used by 2

Used byTarski's Euclidean axiom · Independence of the parallel postulate

DefinitionTarski's Euclidean axiom#✓fully proved

For a model \(M\) of Tarski's absolute plane geometry with betweenness relation \(B\), where \(B(a, b, c)\) means that \(b\) lies between \(a\) and \(c\) (allowing \(b = a\) or \(b = c\)), the Euclidean axiom A10 holds in \(M\) when for all points \(a, b, c, d, t\) of \(M\) with \(B(a, d, t)\), \(B(b, d, c)\) and \(a \ne d\) there are points \(x\) and \(y\) of \(M\) with \(B(a, b, x)\), \(B(a, c, y)\) and \(B(x, t, y)\).

In the presence of the other axioms of absolute geometry, this axiom is equivalent to Euclid's parallel postulate.

def Euclidean (M : Type*) (T : TarskiAbsolute M) : Prop :=
  ∀ a b c d t : M, T.B a d t → T.B b d c → a ≠ d →
    ∃ x y : M, T.B a b x ∧ T.B a c y ∧ T.B x t y

Uses 1 · Used by 1

Statement usesTarski's absolute plane geometry

Used byIndependence of the parallel postulate

TheoremIndependence of the parallel postulate#●ready to prove

Tarski's Euclidean axiom A10 is independent of Tarski's axioms of absolute plane geometry: there is a model of absolute plane geometry in which the Euclidean axiom holds, and there is a model of absolute plane geometry in which it fails.

public theorem_wanted parallel_postulate_independent :
    (∃ (M : Type) (T : TarskiAbsolute M), Euclidean M T) ∧
    (∃ (M : Type) (T : TarskiAbsolute M), ¬ Euclidean M T)

Sources

• Independence of Euclid's parallel postulate; the hyperbolic-plane models are due to E. Beltrami (1868) and F. Klein (1871). Tarski's axiomatization: W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer (1983). Formalized in HOL Light by John Harrison and in Isabelle by Tim Makarios (T.J.M. Makarios, A Mechanical Verification of the Independence of Tarski's Euclidean Axiom, MSc thesis, Victoria University of Wellington, 2012; Isabelle/AFP entry Tarskis_Geometry). Problem parallel_postulate_independent of the lean-eval benchmark.

Uses 2

Statement usesTarski's Euclidean axiom · Tarski's absolute plane geometry

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.