GeneralSelfRefQuery

formal source

 121/-- A more general self-referential query: c encodes "I don't RSStab."
 122    We model this as: there's a function φ that tells us "what c asserts"
 123    and c asserts ¬RSStab(c). -/
 124structure GeneralSelfRefQuery where
 125  config : ℝ
 126  /-- c "asserts" a proposition -/
 127  asserts : Prop
 128  /-- That proposition is ¬RSStab(c) -/
 129  encodes_negation : asserts ↔ ¬RSStab config
 130  /-- c is "correct" if what it asserts matches its stabilization status -/
 131  correctness : RSStab config ↔ asserts
 132
 133/-- **THEOREM 2**: General self-referential queries are contradictory.
 134
 135    The correctness condition and encoding condition together imply:
 136    RSStab(c) ↔ asserts ↔ ¬RSStab(c)
 137
 138    This is P ↔ ¬P, which is impossible. -/
 139theorem general_self_ref_impossible : ¬∃ q : GeneralSelfRefQuery, True := by
 140  intro ⟨q, _⟩
 141  -- q.correctness: RSStab q.config ↔ q.asserts
 142  -- q.encodes_negation: q.asserts ↔ ¬RSStab q.config
 143  -- Combining: RSStab q.config ↔ ¬RSStab q.config
 144  have h1 := q.correctness
 145  have h2 := q.encodes_negation
 146  -- RSStab ↔ asserts ↔ ¬RSStab
 147  have h : RSStab q.config ↔ ¬RSStab q.config := h1.trans h2
 148  by_cases hs : RSStab q.config
 149  · exact (h.mp hs) hs
 150  · exact hs (h.mpr hs)
 151
 152/-! ## The Three-Part Theorem from the Paper -/
 153
 154/-! For the paper's Theorem 4.1, we need to show that IF a self-referential