Theory Higher_Projective_Space_Axioms

theory Higher_Projective_Space_Axioms
  imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We introduce the types of 'point and 'line and an incidence relation between them.
▪ A set of axioms for higher projective spaces, i.e. we allow models of dimension ‹>› 3. 
›

section ‹The axioms for Higher Projective Geometry›

lemma distinct4_def:
  "distinct [A,B,C,D] = ((A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D) ∧ (B ≠ C) ∧ (B ≠ D) ∧ (C ≠ D))"
  by auto

lemma distinct3_def:
  "distinct [A,B,C] = ((A ≠ B) ∧ (A ≠ C) ∧ (B ≠ C))"
  by auto

locale higher_projective_space =
(* One has a type of 'point *)
(* One has a type of 'line *)
(* One has a relation of incidence between 'point and 'line *)
  fixes incid :: "'point ⇒ 'line ⇒ bool"

(* We have the following axioms *)

(* Ax1: Any two distinct 'point are incident with just one line *)
  assumes ax1_existence: "∃l. (incid P l) ∧ (incid M l)"
  assumes ax1_uniqueness: "(incid P k) ⟶ (incid M k) ⟶ (incid P l) ⟶ (incid M l) ⟶ (P = M) ∨ (k = l)"


(* Ax2: If A B C D are four distinct 'point such that AB meets CD, then AC meets BD.
Sometimes this is called Pasch's axiom, but according to Wikipedia it is misleading
since Pasch's axiom refers to something else. *)
assumes ax2: "distinct [A,B,C,D] ⟶ (incid A lAB ∧ incid B lAB) 
⟶ (incid C lCD ∧ incid D lCD) ⟶ (incid A lAC ∧ incid C lAC) ⟶ 
(incid B lBD ∧ incid D lBD) ⟶ (∃I.(incid I lAB ∧ incid I lCD)) ⟶ 
(∃J.(incid J lAC ∧ incid J lBD))"



(** Dimension-related axioms **)
(* Ax3: Every line is incident with at least three 'point.
As I understand it, this axiom makes sure that 'line are not degenerated into 'point
and since it asks for three distinct 'point, not only 2, it captures the idea that
'line have unlimited extent, i.e. there is always a point between two distinct 'point. *)
assumes ax3: "∃A B C. distinct [A,B,C] ∧ (incid A l) ∧ (incid B l) ∧ (incid C l)"

(* Ax4: There exists two 'line that do not meet, hence the geometry is at least 3-dimensional *)
assumes ax4: "∃l m.∀P. ¬(incid P l ∧ incid P m)"


end