MetaPrinciple

formal source

  36This is a THEOREM, not an axiom. If there exists a self-recognizing element,
  37then the type must be nonempty (we can extract the element from the existential).
  38-/
  39theorem MetaPrinciple (X : Type*) :
  40    (∃ (R : X → X → Prop), ∃ x, R x x) → Nonempty X := by
  41  intro ⟨_, x, _⟩
  42  exact ⟨x⟩
  43
  44/-- Constructive version: recognition implies existence. -/
  45theorem recognition_implies_existence {X : Type*}
  46    (h : ∃ (R : X → X → Prop), ∃ x, R x x) : Nonempty X :=
  47  MetaPrinciple X h
  48
  49/-- The contrapositive: emptiness implies no self-recognition. -/
  50theorem empty_has_no_self_recognition (X : Type*) (h : IsEmpty X) :
  51    ¬(∃ (R : X → X → Prop), ∃ x, R x x) := by
  52  intro ⟨_, x, _⟩
  53  exact h.elim x
  54
  55/-! ## Recognition Structure -/
  56
  57/-- A recognition structure on a type.
  58
  59This captures the minimal structure needed for "things to be recognized."
  60-/
  61structure RecognitionStructure (X : Type*) where
  62  /-- The recognition relation: R x y means "x recognizes y". -/
  63  recognizes : X → X → Prop
  64  /-- At least one thing can recognize itself (closure). -/
  65  has_self_recognition : ∃ x, recognizes x x
  66
  67/-- Any recognition structure implies nonemptiness. -/
  68theorem recognition_structure_nonempty {X : Type*}
  69    (R : RecognitionStructure X) : Nonempty X :=