Semantic Reflection Incompatibility: A Universal Proof Technique for Impossibility Results

What is the SRI Technique? The Semantic Reflection Incompatibility (SRI) technique is a powerful method for proving that formal systems cannot talk about themselves in certain ways. While classical results in mathematical logic show that some problematic formula exists, SRI goes much further—it proves that every formula fails when you try to internalize certain semantic properties. The Core Idea Imagine you're working with a formal system S (like Peano Arithmetic) and you want it to have an internal predicate P_S that captures some semantic property—like "this formula is true" or "this formula is provable" or "this formula is valid." For P_S to do its job properly (to be "adequate"), it needs to satisfy certain closure properties. For instance, if P_S is supposed to formalize truth, then it should respect modus ponens: if P_S says "φ is true" and "φ → ψ is true," then P_S should say "ψ is true." The SRI technique reveals that these very adequacy requirements—the properties that make P_S work correctly—create a fatal problem: they force the system to prove P_S applies to everything, including formulas where it demonstrably cannot apply. How It Works: The Six Phases Phase 1 (Setup): You start with your formal system S, a semantic property Q you want to internalize, and your attempted formalization P_S. Phase 2 (Adequacy Characterization): You figure out exactly what closure properties P_S must satisfy to adequately formalize Q. These are things like necessitation ("if S proves φ, then S proves P_S(⌜φ⌝)"), modus ponens closure, conjunction closure, etc. Phase 3 (Internal Constraint Analysis): You identify what the system must be able to prove about P_S for it to function as intended—basically, what makes P_S "work" internally. Phase 4 (Obstruction Construction): Using the classical diagonal lemma, you construct a self-referential formula ψ that essentially says "P_S doesn't apply to me." This is similar to the liar paradox or Gödel's construction. You can prove locally that S cannot prove P_S(⌜ψ⌝)—if it did, you'd get a contradiction. Phase 5 (Universal Propagation): Here's where SRI's innovation shines. You prove a propagation lemma: if S proves P_S applies to ANY formula φ₀ (even something trivial like "0=0"), then the adequacy properties force S to prove P_S applies to the obstruction formula ψ. This works through a careful 21-step derivation that uses only the adequacy properties you identified in Phase 2. You start with P_S(⌜φ₀⌝), use necessitation to get P_S(⌜⊤⌝) (where ⊤ is a tautology), then systematically apply closure properties to build up to P_S(⌜ψ⌝). But this creates a contradiction! Phase 4 showed S cannot prove P_S(⌜ψ⌝), yet Phase 5 shows that if S proves P_S for anything, it must prove P_S(⌜ψ⌝). The only way out is that S cannot prove P_S(⌜φ⌝) for any formula φ whatsoever. Phase 6 (Categorical Invariance): You verify that this result doesn't depend on accidental features of your construction—it holds uniformly across all similar systems. The Key Insight The propagation mechanism is what makes SRI special. Classical diagonalization gives you one bad formula. SRI shows that the very properties needed to make P_S adequate create a "domino effect": if P_S applies anywhere, adequacy forces it to propagate everywhere, including to the obstruction where it provably cannot apply. It's like discovering that a bridge design has a fundamental flaw: not just that one specific bridge falls down, but that any attempt to build a bridge with those design requirements will fail, because the requirements themselves create forces that inevitably lead to collapse. What This Means SRI reveals that certain kinds of semantic self-reflection are not just difficult but structurally impossible. When a formal system is strong enough to support self-reference, and when adequacy demands certain closure properties, and when those properties enable propagation to obstructions, you hit an absolute barrier: the system cannot prove its semantic predicate applies to anything. This isn't a limitation of our cleverness or a gap in our techniques—it's a fundamental feature of how formal systems work when they try to talk about themselves in sufficiently rich ways.