general_self_ref_impossible

formal source

 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
 155query existed, it would be:
 1561. Not RSTrue
 1572. Not RSFalse
 1583. Outside the ontology
 159
 160But we've already shown such queries can't exist consistently.
 161We can still state what WOULD happen if we could define one: -/
 162
 163/-- If we could define a self-referential query c where:
 164    - c is "correct" when c stabilizes iff c encodes truth
 165    - c encodes "I don't stabilize"
 166
 167    Then c cannot be RSTrue. -/
 168theorem self_ref_not_rs_true
 169    (c : ℝ)