Theory Projective_Plane_Axioms

theory Projective_Plane_Axioms
  imports Main
begin

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

(* Update: In 2021, Niels Mündler, from the Technical University of Munich, kindly updated the formalization
to replace axiomatizations by locales. *)

text ‹
Contents:
\begin{itemize}
\item We introduce the types of points and lines and an incidence relation between them.
\item A set of axioms for the projective plane (the models of these axioms are
n-dimensional with $n\ge 2$).
\end{itemize}
›

section ‹The Axioms of the Projective Plane›


locale projective_plane =
  (* One has a type of points *)
  (* One has a type of lines *)
  (* One has an incidence relation between points and lines *)
  (* which is all expressed in the following line *)
  fixes incid :: "'point ⇒ 'line ⇒ bool"

  (* Ax1: Any two (distinct) points lie on a (unique) line *)
  assumes ax1: "∃l. incid P l ∧ incid Q l"

  (* Ax2: Any two (distinct) lines meet in a (unique) point *)
  assumes ax2: "∃P. incid P l ∧ incid P m"

  (* The uniqueness part *)
  assumes ax_uniqueness: "⟦incid P l; incid Q l; incid P m; incid Q m⟧ ⟹  P = Q ∨ l = m"

  (* Ax3: There exists four points such that no three of them are collinear *)
  assumes ax3: "∃A B C D. distinct [A,B,C,D] ∧ (∀l.
              (incid A l ∧ incid B l ⟶ ¬(incid C l) ∧ ¬(incid D l)) ∧
              (incid A l ∧ incid C l ⟶ ¬(incid B l) ∧ ¬(incid D l)) ∧
              (incid A l ∧ incid D l ⟶ ¬(incid B l) ∧ ¬(incid C l)) ∧
              (incid B l ∧ incid C l ⟶ ¬(incid A l) ∧ ¬(incid D l)) ∧
              (incid B l ∧ incid D l ⟶ ¬(incid A l) ∧ ¬(incid C l)) ∧
              (incid C l ∧ incid D l ⟶ ¬(incid A l) ∧ ¬(incid B l)))"


end