theorem
proved
term proof
general_self_ref_impossible
show as:
view Lean formalization →
formal statement (Lean)
139theorem general_self_ref_impossible : ¬∃ q : GeneralSelfRefQuery, True := by
proof body
Term-mode proof.
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. -/