Paper deep dive

The Semantic Elevation Operator and the Closure of the Undecidable Class under Preservation

Jose Pascual Gumbau Mezquita

Year: 2026Venue: arXiv preprintArea: cs.LOType: PreprintEmbeddings: 47

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%

Last extracted: 9/11/2026, 5:07:09 AM

Summary

This paper formalizes the 'semantic elevation operator' (ΛΦ) to analyze the preservation of semantic properties in self-modifying systems. It proves that for intensional transformations (which depend on source code structure), the elevated property remains undecidable, even though it breaks the extensionality required by Rice's theorem. The proof utilizes Kleene's recursion theorem. The class of non-verifiable properties (U) is shown to be closed under this operator, and unbounded iteration climbs the arithmetical hierarchy to Π02-completeness. The paper also demonstrates that the 'supervisory regress' of verifiers does not terminate.

Entities (9)

Rice's Theorem · theorem · 99%Semantic Elevation Operator · mathematical-operator · 98%Kleene's Recursion Theorem · theorem · 97%Undecidable Class U · mathematical-class · 95%Intensional Transformation · concept · 92%Arithmetical Hierarchy · mathematical-structure · 90%Supervisory Regress · concept · 88%Effective Topos · mathematical-structure · 85%Lawvere's Fixed-Point Theorem · theorem · 85%

Relation Signals (7)

Semantic Elevation Operator → relieson → Kleene's Recursion Theorem

confidence 97% · the proof rests on Kleene's recursion theorem, not on Rice.

Undecidable Class U → isclosedunder → Semantic Elevation Operator

confidence 96% · Consequently the class U of non-verifiable properties is closed under the elevation operator.

Semantic Elevation Operator → governs → Dynamic Property Preservation

confidence 95% · We formalise this transition through a semantic elevation operator ΛΦ, which turns the static question 'does x satisfy P?' into the dynamic question 'is P preserved after x is transformed by Φ?'

Semantic Elevation Operator → provesundecidabilityfor → Intensional Transformation

confidence 93% · when Φ is intensional ... the elevated property remains undecidable

Semantic Elevation Operator → climbs → Arithmetical Hierarchy

confidence 90% · Unbounded iteration of the operator climbs the arithmetical hierarchy -to Π02-completeness-

Supervisory Regress → doesnotterminate → Semantic Elevation Operator

confidence 88% · We further show that the supervisory regress does not terminate

Semantic Elevation Operator → isinstanceof → Lawvere's Fixed-Point Theorem

confidence 85% · in the efective topos, in which elevation appears as an instance of Lawvere's fxed-point theorem

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:The undecidability of a program's static semantic properties is governed by Rice's theorem. Self-modifying systems, however, require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself. We formalise this transition through a semantic elevation operator {\Lambda}{\Phi}, which turns the static question "does x satisfy P?" into the dynamic question "is P preserved after x is transformed by {\Phi}?". We prove that when {\Phi} is intensional (depending on the source code, not only on the computed function), the elevated property remains undecidable even though it breaks the extensionality that Rice's theorem requires; the proof rests on Kleene's recursion theorem, not on Rice. Consequently the class U of non-verifiable properties is closed under the elevation operator. Unbounded iteration of the operator climbs the arithmetical hierarchy -to {\Pi}02-completeness- consolidating non-verifiability as a structural fact. We further show that the supervisory regress does not terminate: no fnite tower of increasingly capable verifiers yields an unconditional certificate. A categorical reading of these results in the efective topos, in which elevation appears as an instance of Lawvere's fxed-point theorem, is left as a direction for future work.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

43,694 characters extracted from source content.

Expand or collapse full text

The semantic elevation operator and the closure of the undecidable class under preservationThanks: The structuring, formal-language editing, and orthotypographic review of this document were conducted with the assistance of the artificial intelligence model Claude, Anthropic, 2026. Abstract. The undecidability of a program’s static semantic properties is governed by Rice’s theorem. Self-modifying systems, however, require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself. We formalise this transition through a semantic elevation operator ΛΦ _ , which turns the static question “does x satisfy P?” into the dynamic question “is P preserved after x is transformed by Φ ?”. We prove that when Φ is intensional (depending on the source code, not only on the computed function), the elevated property remains undecidable even though it breaks the extensionality that Rice’s theorem requires; the proof rests on Kleene’s recursion theorem, not on Rice. Consequently the class U of non-verifiable properties is closed under the elevation operator. Unbounded iteration of the operator climbs the arithmetical hierarchy—to Π20 ^0_2-completeness—consolidating non-verifiability as a structural fact. We further show that the supervisory regress does not terminate: no finite tower of increasingly capable verifiers yields an unconditional certificate. A categorical reading of these results in the effective topos, in which elevation appears as an instance of Lawvere’s fixed-point theorem, is left as a direction for future work. Jose Pascual Gumbau Mezquita University Jaume I de Castelló, Spain gumbau@uji.es 1. Introduction Verifying the safety of a computational system means, formally, deciding whether the program satisfies a semantic property of its behaviour. For fixed systems the limits are classical and well understood: Rice’s theorem states that every non-trivial semantic property is undecidable. But the systems that motivate this work are not fixed: they update, retrain, rewrite themselves. The relevant question is dynamic—“will this system remain safe when it modifies itself?”—and it is this question that we study. We formalise the transition from the static to the dynamic regime as an operator—semantic elevation—which takes a property P and a program transformation Φ and produces a new property: “P is preserved under Φ ”. The article pursues three goals. (1) Isolate the elevation operator as a general construction and determine under which conditions on Φ the elevated property remains non-verifiable. (2) Prove a closure theorem: the class of non-verifiable properties is closed under elevation, and unbounded iteration of the operator deepens non-verifiability by climbing the arithmetical hierarchy. (3) Establish the robustness of the phenomenon: show that non-verifiability is stable under the operator and that the supervisory regress which attempts to evade it does not terminate. The thread running through these results is the Expressivity Principle: the expressivity that makes a system useful is the expressivity that makes it non-verifiable. The expressivity barrier this principle imposes—the obstruction no verifier can cross—manifests statically as Rice’s theorem and, as we show here, dynamically under the elevation operator. This article establishes that the Principle is not a coincidence recurring at each level but a stable property: a fixed point of the elevation operator. A third, geometric reading—that this stability is, in the effective topos, an instance of Lawvere’s fixed-point theorem—is sketched as future work (§7). 1.1. The two regimes, and delimitation Preserving a property P under a self-modification Φ splits into two regimes according to how Φ treats the code. If Φ is extensional—it respects functional equivalence—the elevated property “P is preserved under Φ ” is again a behavioural property, and its undecidability reduces directly to Rice’s theorem; this regime is closed, and we record it (Proposition 5.1) for completeness. If Φ is intensional—it inspects the syntactic form of the program, as every real code rewrite does—the elevated property ceases to be behavioural: it may hold for one index and fail for another computing the same function. Rice’s theorem then loses jurisdiction, and undecidability is established by a deeper reason, Kleene’s recursion theorem (Theorem 4.4). The unbounded iteration (Theorem 4.7) climbs the arithmetical hierarchy to Π20 ^0_2-completeness by a third, independent route: iteration itself. The distinction is not one of difficulty but of jurisdiction: each regime falls under a different governing theorem—Rice in one case, the recursion theorem in the other. Real self-modification is intensional (an agent that rewrites itself operates on its own source), so the intensional case is the one that matters; the extensional case models a domesticated idealisation. Establishing non-verifiability only for the extensional case would leave open the objection that the realistic, intensional case might be verifiable, precisely because Rice does not apply there. Theorem 4.4 closes that door. The joint conclusion is stronger than either regime alone: non-verifiability of persistence does not depend on how self-modification is modelled. 2. Preliminaries Fix an acceptable Gödel numbering φee∈ℕ\ _e\_e of the partial computable functions (PC). We write φe(x)↓ _e(x)\! if the computation halts and φe(x)↑ _e(x)\! otherwise. Let K=x:φx(x)↓K=\x: _x(x)\! \ denote the self-halting set, which is Σ10 ^0_1-complete. A set of partial computable functions P~ P is extensional (or behavioural) if it is closed under equality of functions: φa=φb⇒(φa∈P~⇔φb∈P~) _a= _b ( _a∈ P _b∈ P). Its index set is P=e:φe∈P~P=\e: _e∈ P\. We call P~ P non-trivial if ∅⊊P~⊊PC P . Theorem 2.1 (Rice). If P~ P is a non-trivial behavioural property, then P is undecidable. Theorem 2.2 (Kleene recursion). For every total computable f there exists e with φe≃φf⁡(e) _e _f(e). We write the arithmetical hierarchy as Σn0,Πn0 ^0_n, ^0_n. We use that TOT=x:φx totalTOT=\x: _x total\ is Π20 ^0_2-complete, and Kleene’s T predicate T⁡(e,x,s)T(e,x,s) (“e on input x halts within s steps”), which is primitive recursive. A transformation is a total computable function Φ:ℕ→ℕ , read as one step of self-modification: Φ⁡(x) (x) is the index of the program obtained from x by one rewrite. A transformation is extensional (semantically well-defined) if φx=φy⇒φΦ⁡(x)=φΦ⁡(y) _x= _y _ (x)= _ (y); otherwise it is intensional. This article treats the intensional case: Φ may depend on the source x, not only on the function φx _x it computes. This is the situation modelling real self-modification, where rewriting operates on program syntax. 2.1. Decidability of persistence We work with the classical notion of decidability: a property, identified with its index set, is decidable if that set is recursive. We introduce no proprietary notion of “verifiability”; results are statements of (un)decidability, and “verifiable” is used only as an informal gloss for “decidable”, in the sense of an algorithmic total decider—not in the formal-methods sense of “provable with human assistance”. The object of the article is not the decidability of a static property but that of its persistence under transformation. Definition 2.3. The one-step persistence of P under Φ is decidable if ΛΦ(P) _ (P) (Definition 3.1) is decidable. The unbounded persistence is decidable if ΛΦω(P) _ ^ω(P) (Definition 3.2) is decidable. 2.2. The undecidable class U The class U studied here is the decidability face of non-verifiability: properties whose index set is not recursive, including those residing higher in the arithmetical hierarchy. We do not include the resource face (intractability), which behaves in a logically different way and requires separate treatment. So that the closure theorem is not trivial—every undecidable property is undecidable, and asserting it stays so would say nothing—U is defined not as “every undecidable set” but by its provenance: :=the closure, under ΛΦ and ΛΦω, of the non-trivial behavioural properties.U:=the closure, under _ and _ ^ω, of the non-trivial behavioural properties. Under this reading, “U is closed under ΛΦ _ ” asserts something substantive: elevation never drops below undecidability, even when it breaks extensionality. 3. The semantic elevation operator Definition 3.1 (one-step elevation). For an index set P and a transformation Φ , the one-step elevation of P under Φ is ΛΦ(P):=x∈ℕ:φx∈P~∧φΦ⁡(x)∈P~. _ (P):=\\,x : _x∈ P\ \ _ (x)∈ P\,\. In words: x satisfies the elevated property if the program is safe now (x∈Px∈ P) and remains safe after the next rewrite (Φ⁡(x)∈P (x)∈ P). We adopt the conjunction—“safe now and next”—because it composes cleanly under iteration; the biconditional variant, natural for pointwise contradiction arguments, does not yield the along-the-trajectory iteration we need. Definition 3.2 (limit elevation, ω-persistence). The limit elevation of P under Φ is ΛΦω(P):=x∈ℕ:∀k≥0,φΦk(x)∈P~, _ ^ω(P):=\\,x :∀ k≥ 0,\ _ ^k(x)∈ P\,\, where Φk ^k is the k-th iterate of Φ (Φ0=id ^0=id). In words: no future rewriting trajectory, of any length, breaks P. This is the formalisation of persistent alignment: the guarantee that the safety property survives the entire evolution of the system. Remark 3.3 (intensionality). Because Φ is intensional, the occurrence φΦ⁡(x) _ (x) is not determined by φx _x: two indices x,yx,y with φx=φy _x= _y may have φΦ⁡(x)≠φΦ⁡(y) _ (x)≠ _ (y). Hence ΛΦ(P) _ (P) is not a behavioural property: it is not closed under equality of functions. This is why Rice’s theorem does not apply to ΛΦ(P) _ (P), and why its undecidability (§4) requires a proof of its own. 3.1. The disruption condition For ΛΦ(P) _ (P) to be undecidable, the disruption of Φ cannot be an accident of two isolated indices: the reduction from K (Theorem 4.4) must construct, for each instance x, a witness whose fate under Φ encodes whether x∈Kx∈ K. We therefore take as primary the disruption uniform over a family of syntactic wrappers, and derive the pointwise version as an illustrative case. Definition 3.4 (uniform disruption over wrappers). Φ is uniformly disruptive with respect to a non-trivial behavioural property P~ P if there is a total computable wrapper w:ℕ→ℕw and a witness t∈P~t∈ P such that, for every index e: (i) φw⁡(e)=t∈P~ _w(e)=t∈ P (the wrapper never alters the computed function: every w⁡(e)w(e) computes the same witness of P~ P); and (i) φΦ⁡(w⁡(e))∈P~ _ (w(e))∈ P if φe(e)↓ _e(e)\! , while φΦ⁡(w⁡(e))∉P~ _ (w(e))∉ P if φe(e)↑ _e(e)\! . Condition (i) makes the disruption genuinely intensional: all w⁡(e)w(e) compute the same function t, yet Φ maps them inside or outside P~ P according to a fact—the halting of φe(e) _e(e)—that does not depend on the computed function but on the syntax of the wrapper. This is exactly what an extensional transformation is forbidden to do, so no uniformly disruptive Φ can be extensional, and the article cannot collapse into a corollary of Rice. Crucially, w is total computable: it builds the wrapper always, without ever deciding whether φe(e)↓ _e(e)\! —(un)decidability lives in the behaviour of the wrapper, not in its construction. Observation 3.5 (pointwise disruption). The primary condition immediately yields two witnesses of the same function with opposite fates: taking e1∈Ke_1∈ K and e0∉Ke_0∉ K, the wrappers q1:=w⁡(e1)q_1:=w(e_1) and q0:=w⁡(e0)q_0:=w(e_0) satisfy φq1=φq0=t∈P~ _q_1= _q_0=t∈ P, yet φΦ⁡(q1)∈P~ _ (q_1)∈ P and φΦ⁡(q0)∉P~ _ (q_0)∉ P. These witnesses guarantee the non-triviality of ΛΦ(P) _ (P): q1∈ΛΦ(P)q_1∈ _ (P) and q0∈P∖ΛΦ(P)q_0∈ P _ (P). Lemma 3.6 (uniform reduction via Kleene). If Φ is uniformly disruptive w.r.t. P~ P, then K≤mΛΦ(P)K _m _ (P) via the total function h:=wh:=w; consequently ΛΦ(P) _ (P) is undecidable. Proof. Take h⁡(x):=w⁡(x)h(x):=w(x), total computable by Definition 3.4. Then: • by (i), φh⁡(x)=t∈P~ _h(x)=t∈ P for all x, so h⁡(x)∈Ph(x)∈ P unconditionally; • if x∈Kx∈ K (φx(x)↓ _x(x)\! ): by (i), φΦ⁡(h⁡(x))∈P~ _ (h(x))∈ P, and since h⁡(x)∈Ph(x)∈ P we get h(x)∈ΛΦ(P)h(x)∈ _ (P); • if x∉Kx∉ K (φx(x)↑ _x(x)\! ): by (i), φΦ⁡(h⁡(x))∉P~ _ (h(x))∉ P, so h⁡(x)∉ΛΦ(P)h(x)∉ _ (P). Hence x∈K⇔h⁡(x)∈ΛΦ(P)x∈ K h(x)∈ _ (P). Since K is undecidable and ≤m _m preserves undecidability, ΛΦ(P) _ (P) is undecidable. The reduction is not circular: h⁡(x)h(x) never decides x∈Kx∈ K; it only builds a wrapper embedding the simulation of φx(x) _x(x), and it is the (non-)halting of that simulation—inside Φ⁡(h⁡(x)) (h(x)), not inside the construction of h—that determines membership in ΛΦ(P) _ (P). ∎ 3.2. Non-vacuity: an explicit construction, and a clarifying contrast Fix P~=id P=\id\, the property “computes the identity function”, so P=e:∀z,φe(z)=zP=\e:∀ z,\ _e(z)=z\; it is non-trivial and behavioural. (This witness serves Theorem 4.4; for Theorem 4.7, which needs a complexity condition on P~ P, a different one is used—see there.) An explicit uniformly disruptive Φ . We build the triple (P~,w,Φ)( P,w, ) by the s-m-n theorem. The wrapper w. By s-m-n, define w total so that φw⁡(e) _w(e) is the program that, on input z, returns z, carrying e embedded as inert syntactic data in the code. Then φw⁡(e)=id∈P~ _w(e)=id∈ P for every e: the wrapper never alters the computed function. The transformation Φ . Define Φ as a total computable syntactic rewriter. Given an index x: if x has not the structure of a wrapper w⁡(e)w(e), set Φ⁡(x)=x (x)=x; if x=w⁡(e)x=w(e), let Φ⁡(w⁡(e)) (w(e)) generate (by s-m-n) the index of a program y that runs the simulation of φe(e) _e(e) and, if it halts, returns z: φy(z)=zif φe(e)↓,↑if φe(e)↑. _y(z)= casesz&if _e(e)\! ,\\ \! &if _e(e)\! . cases Then φΦ⁡(w⁡(e))=id∈P~ _ (w(e))=id∈ P iff φe(e)↓ _e(e)\! , i.e. condition (i) holds. Definition 3.4 is thus consistent and non-vacuous; by Lemma 3.6, K≤mΛΦ(id)K _m _ (\id\). Why Φ is realisable. Φ does not run φe(e) _e(e): it is a pure rewriter that reads the syntax of w⁡(e)w(e), extracts e, and synthesises the code of y by s-m-n—a compile-time operation, always terminating. Non-halting appears only when Φ⁡(w⁡(e)) (w(e)) is executed, not when Φ constructs it. This faithfully models real self-modification: an agent does not evaluate the infinite semantics of its code (impossible by Rice) but rewrites its own syntax, injecting modules whose termination it cannot foresee. A contrast: an intensionality that does not work. To see that condition (i)—the coupling to halting—is essential and not gratuitous, consider a Φ′ that rewrites by a decidable syntactic tag, e.g. index parity: Φ′(e)= (e)= an index of idid if e is even, of the empty function if e is odd. This Φ′ is intensional (two indices of idid with opposite fates by parity) and pointwise disruptive, but it is not uniformly disruptive: to use it in a reduction from K one would need to produce wrappers of the parity dictated by φe(e)↓ _e(e)\! —that is, to decide K, which is impossible. Intensionality alone does not suffice; it must be able to encode an undecidable fact, and it is the inert simulation inside the wrapper that achieves this. The critical condition to preserve in any generalisation is that the embedded simulation be at once syntactically visible (so Φ reacts to it) and semantically inert (so φw⁡(e) _w(e) is unchanged); were it to affect the output, w⁡(e)w(e) would cease to compute idid and we would fall back into Rice’s regime. 3.3. An effective class of disruptive rewrites The example of §3.2 shows uniform disruption is non-vacuous, but a single witness says nothing about which rewrites satisfy it. We characterise an effective class of intensional transformations—those following the syntactic-instrumentation pattern—and prove every transformation in it is disruptive. The class is a structural witness, not the totality of rewrites; on its exact scope, see the end of the subsection. Definition 3.7 (syntactic-instrumentation class ℛinst(P)R_inst(P)). Let P~ P be non-trivial with witnesses t∈Pt∈ P (φt∈P~ _t∈ P) and f∉Pf∉ P (φf∉P~ _f∉ P). A total computable Φ belongs to ℛinst(P)R_inst(P) if it admits a decomposition into three compatible total computable functions: (1) Extractor δ:ℕ→ℕ∪⊥δ ∪\ \, reading an index x and extracting a parameter e=δ⁡(x)e=δ(x) (⊥ if x has no wrapper structure). (2) Wrapper generator w:ℕ→ℕw , with δ⁡(w⁡(e))=eδ(w(e))=e and φw⁡(e)=φt∈P~ _w(e)= _t∈ P for all e. (3) Conditional synthesiser inj:ℕ×ℕ→ℕinj ×N (obtained by s-m-n) such that when δ(x)=e≠⊥δ(x)=e≠ one has Φ⁡(x)=inj⁡(t,e) (x)=inj(t,e), with φinj⁡(t,e)(z)=φt(z) _inj(t,e)(z)= _t(z) if φe(e)↓ _e(e)\! and =φf(z)= _f(z) if φe(e)↑ _e(e)\! . Compatibility. On the wrapper family, Φ⁡(w⁡(e))=inj⁡(t,δ⁡(w⁡(e)))=inj⁡(t,e) (w(e))=inj(t,δ(w(e)))=inj(t,e); outside it, δ(x)=⊥δ(x)= and Φ is free. Theorem 3.8 (every syntactic instrumentation is disruptive). Every Φ∈ℛinst(P) _inst(P) is uniformly disruptive w.r.t. P~ P (Definition 3.4). Proof. Let w be as in condition 2. By condition 2, φw⁡(e)=φt∈P~ _w(e)= _t∈ P for all e—condition (i) of Definition 3.4. By compatibility, Φ⁡(w⁡(e))=inj⁡(t,e) (w(e))=inj(t,e); evaluating condition 3: if φe(e)↓ _e(e)\! then φΦ⁡(w⁡(e))=φt∈P~ _ (w(e))= _t∈ P; if φe(e)↑ _e(e)\! then φΦ⁡(w⁡(e))=φf∉P~ _ (w(e))= _f∉ P. Thus φΦ⁡(w⁡(e))∈P~⇔φe(e)↓⇔e∈K _ (w(e))∈ P _e(e)\! e∈ K, condition (i). By Lemma 3.6, K≤mΛΦ(P)K _m _ (P). ∎ Remark 3.9 (scope of ℛinstR_inst: what we claim and what we do not). ℛinst(P)R_inst(P) is a natural, effective class of intensional rewrites: those recognising an inert parameter (δ) and synthesising conditional code (injinj) while preserving the function (w). By Rogers’ isomorphism theorem, working with Gödel indices rather than concrete language syntax loses no generality as regards code recognition and synthesis (parsing and generation are absorbed into δ and injinj). We do not claim every computable rewrite lies in ℛinstR_inst: function-preserving optimisations without instrumentation, refactorings, and transformations that change the computed function (fine-tuning, pruning, quantisation) do not—the last fail even condition (i). ℛinstR_inst is thus an existential witness, not a totality: it establishes that there exist effective, realistic rewrites under which persistence is undecidable. This existential reading is exactly what an impossibility of verification requires, and is stronger as a warning than a universal one: not that every self-modification is dangerous, but that the dangerous ones cannot be told apart in advance—since the wrapper w⁡(e)w(e) preserves the function, a disruptive rewrite is syntactically of the same kind as a benign one, and deciding whether a given rewrite is disruptive would amount to deciding K. 4. The closure theorem Proposition 4.1 (relation between the operators; coinductive characterisation). Let FP:⁡(ℕ)→⁡(ℕ)F_P (N) (N) be FP(S)=P∩Φ−1(S)=x∈P:Φ⁡(x)∈SF_P(S)=P∩ ^-1(S)=\x∈ P: (x)∈ S\, and set ΛΦ[k](P):=FPk(ℕ) _ ^[k](P):=F_P^k(N) (the canonical descending chain from ⊤=ℕ =N). Then (1) ΛΦ[0](P)=ℕ _ ^[0](P)=N, ΛΦ[1](P)=P _ ^[1](P)=P, ΛΦ[2](P)=ΛΦ(P) _ ^[2](P)= _ (P), and in general ΛΦ[k](P)=x:∀j<k,φΦj(x)∈P~ _ ^[k](P)=\x:∀ j<k,\ _ ^j(x)∈ P\; (2) FPF_P is co-continuous (it preserves intersections of descending chains), hence ΛΦω(P)=⋂k≥0ΛΦ[k](P)=gfp⁡(FP) _ ^ω(P)= _k≥ 0 _ ^[k](P)= (F_P), the greatest fixed point of FPF_P. Proof. (1) By induction. ΛΦ[0](P)=FP0(ℕ)=ℕ _ ^[0](P)=F_P^0(N)=N. Assuming ΛΦ[k](P)=x:∀j<k,φΦj(x)∈P~ _ ^[k](P)=\x:∀ j<k,\ _ ^j(x)∈ P\, x∈FP(ΛΦ[k](P))⇔φx∈P~∧∀j<k,φΦj+1(x)∈P~⇔∀j<k+1,φΦj(x)∈P~.x∈ F_P( _ ^[k](P)) _x∈ P ∀ j<k,\ _ ^j+1(x)∈ P ∀ j<k+1,\ _ ^j(x)∈ P. In particular ΛΦ[1]=P _ ^[1]=P and ΛΦ[2]=ΛΦ(P) _ ^[2]= _ (P). (2) Co-continuity. For any family Si\S_i\, Φ−1(⋂iSi)=⋂iΦ−1(Si) ^-1( _iS_i)= _i ^-1(S_i) and P∩(⋅)P∩(·) commutes with intersections, so FP(⋂iSi)=⋂iFP(Si)F_P( _iS_i)= _iF_P(S_i). Limit at ω. By (1), ⋂kΛΦ[k](P)=x:∀k∀j<k,φΦj(x)∈P~=x:∀j,φΦj(x)∈P~=ΛΦω(P) _k _ ^[k](P)=\x:∀ k\,∀ j<k,\ _ ^j(x)∈ P\=\x:∀ j,\ _ ^j(x)∈ P\= _ ^ω(P). Greatest fixed point. FP(ΛΦω(P))=ΛΦω(P)F_P( _ ^ω(P))= _ ^ω(P) directly; and if S⊆FP(S)S F_P(S) then every x∈Sx∈ S has x∈Px∈ P and Φ⁡(x)∈S (x)∈ S, so by induction Φj(x)∈P ^j(x)∈ P for all j, whence S⊆ΛΦω(P)S _ ^ω(P). ∎ Remark 4.2 (reading). Each cut ΛΦ[k](P) _ ^[k](P) is “the programs whose rewriting trajectory stays in P~ P for the first k−1k-1 steps”; the descending limit is safety maintained forever. That ΛΦω(P) _ ^ω(P) is a greatest fixed point is not accidental: the gfp is the coinductive signature of safety properties (“nothing bad ever happens along the trajectory”), dual to the least fixed point of reachability properties. Persistent alignment is thus a coinductive property. Remark 4.3 (classical Tarski vs. effective realisability). The Tarski–Knaster theorem on the complete lattice (⁡(ℕ),⊆)(P(N), ) guarantees the gfp exists as a set, and co-continuity of FPF_P guarantees it is reached in exactly ω steps (no transfinite continuation needed). This is a purely set-theoretic fact, independent of computability: ΛΦω(P) _ ^ω(P) is perfectly well-defined. Theorem 4.7 shows this well-defined object is not computable: it exists classically but no procedure decides it. The undecidability of Theorem 4.7 is substantive precisely because it falls on an object that undoubtedly exists. This tension between classical existence and effective non-realisability has a natural categorical formulation in the effective topos—the constructive failure of co-continuity—which we sketch as future work (§7). Theorem 4.4 (closure under one-step elevation). Let P∈P come from a non-trivial behavioural property, and let Φ be uniformly disruptive w.r.t. P~ P (Definition 3.4). Then ΛΦ(P) _ (P) is undecidable; that is, ΛΦ(P)∈ _ (P) . Proof. By condition (i) of Definition 3.4, ΛΦ(P) _ (P) is not extensional (the w⁡(e)w(e) all compute the same function yet fall inside or outside ΛΦ(P) _ (P) according to Φ ), so Rice does not apply. By Lemma 3.6, K≤mΛΦ(P)K _m _ (P) via the total h=wh=w; since K is undecidable and ≤m _m preserves undecidability, ΛΦ(P) _ (P) is undecidable. Non-triviality is given by the witnesses of Observation 3.5. ∎ This establishes undecidability (ΛΦ(P)∉Δ10 _ (P)∉ ^0_1); it claims no exact arithmetical level, which depends on P~ P. Corollary 4.5 (application to instrumentation rewrites). For every Φ∈ℛinst(P) _inst(P) (Definition 3.7), ΛΦ(P) _ (P) is undecidable. In verification terms: there exist effective, realistic self-modifications under which the preservation of safety is not verifiable, and—since these rewrites preserve the computed function—they cannot be told apart in advance from benign ones without deciding K. Corollary 4.6 (Expressivity Principle, stability form). The class U is stable under ΛΦ _ : non-verifiability does not vanish in passing from the static to the dynamic question but is preserved. Non-verifiability is a fixed point of elevation, not an artefact of the static case. 4.1. Two independent sources of non-verifiability The undecidability of Theorem 4.4 comes from intensionality: lifting extensionality removes Rice’s jurisdiction and instrumentation forces undecidability via Kleene. The arithmetical jump that follows has a different, independent origin: unbounded iteration over the rewriting trajectory, which manifests even for transformations that are not instrumentations. The Φ built in Theorem 4.7 is ad hoc—designed to advance a trajectory counter w⁡(e,k)↦w⁡(e,k+1)w(e,k) w(e,k+1)—and does not belong to ℛinstR_inst; the extractor δ there only ensures Φ is total and unambiguous on all of ℕN, not that it is an instrumentation. The two sources are independent: neutralising one—restricting to extensional rewrites, or bounding trajectory depth—does not remove the other. Non-verifiability of persistent alignment is thus overdetermined. Theorem 4.7 (limit elevation and Π20 ^0_2-completeness). Let P0=e:φe(0)↓∈Σ10P_0=\e: _e(0)\! \∈ ^0_1. There is a total computable transformation Φ such that ΛΦω(P0) _ ^ω(P_0) is Π20 ^0_2-complete. Proof. Upper bound (ΛΦω(P0)∈Π20 _ ^ω(P_0)∈ ^0_2). With Kleene’s T predicate, e∈P0⇔∃sT(e,0,s)e∈ P_0 ∃ s\,T(e,0,s). By Definition 3.2, x∈ΛΦω(P0)⇔∀kφΦk(x)(0)↓⇔∀k∃sT(Φk(x),0,s).x∈ _ ^ω(P_0) ∀ k\, _ ^k(x)(0)\! ∀ k\,∃ s\,T( ^k(x),0,s). Since Φ is total computable, R⁡(x,k,s)≡T⁡(Φk(x),0,s)R(x,k,s)≡ T( ^k(x),0,s) is decidable; the condition has the form ∀k∃sR∀ k\,∃ s\,R, whence ΛΦω(P0)∈Π20 _ ^ω(P_0)∈ ^0_2. Lower bound (TOT≤mΛΦω(P0)TOT _m _ ^ω(P_0)). We reduce TOT=e:φe totalTOT=\e: _e total\, which is Π20 ^0_2-complete. By s-m-n define w:ℕ×ℕ→ℕw ×N total with φw⁡(e,k)(z)=0if φe(k)↓,↑if φe(k)↑, _w(e,k)(z)= cases0&if _e(k)\! ,\\ \! &if _e(k)\! , cases so φw⁡(e,k)(0)↓⇔φe(k)↓ _w(e,k)(0)\! _e(k)\! , i.e. w⁡(e,k)∈P0⇔φe(k)↓w(e,k)∈ P_0 _e(k)\! . Let δ be a syntactic recogniser with δ⁡(w⁡(e,k))=(e,k)δ(w(e,k))=(e,k) and δ(x)=⊥δ(x)= otherwise, and set Φ⁡(x)=w⁡(e,k+1) (x)=w(e,k+1) if δ(x)=(e,k)≠⊥δ(x)=(e,k)≠ , and Φ⁡(x)=x (x)=x otherwise. Then Φ is total computable and unambiguous. Let g⁡(e)=w⁡(e,0)g(e)=w(e,0); the iterates are Φk(g⁡(e))=w⁡(e,k) ^k(g(e))=w(e,k), so g⁡(e)∈ΛΦω(P0)⇔∀kw(e,k)∈P0⇔∀kφe(k)↓⇔e∈TOT.g(e)∈ _ ^ω(P_0) ∀ k\,w(e,k)∈ P_0 ∀ k\, _e(k)\! e . Thus TOT≤mΛΦω(P0)TOT _m _ ^ω(P_0); with the upper bound, ΛΦω(P0) _ ^ω(P_0) is Π20 ^0_2-complete. ∎ Note this Φ does not satisfy Definition 3.4 (its wrappers do not preserve the function: φw⁡(e,k) _w(e,k) varies with k) and is not in ℛinstR_inst—consistent with the two-sources remark: the jump comes from iteration, not intensionality. We chose P0P_0 because “φx(0)↓ _x(0)\! ” is Σ10 ^0_1, unlike “φx=id _x=id” (Π20 ^0_2). Corollary 4.8 (Expressivity Principle, deepening form). There is no point in the rewriting chain where verification becomes decidable: iterating elevation does not relax the barrier but shifts it upward in the arithmetical hierarchy, to Π20 ^0_2-completeness. Certifying persistent alignment is strictly harder than certifying safety at a single instant—and, by the two-sources remark, for two independent reasons: the intensionality of the single step (Theorem 4.4) and the unbounded iteration of the trajectory (Theorem 4.7). Neither can be neutralised by closing the other. 5. The extensional case, by contrast We close the map with the extensional regime. Here the result is a corollary of Rice; we prove it for completeness—so the article covers both regimes—and to make the dividing line with the intensional case visible. Proposition 5.1 (extensional case). If Φ is extensional (semantically well-defined) and P~ P is a non-trivial behavioural property that is P-disruptive under Φ , then ΛΦ(P) _ (P) is undecidable. Proof. As Φ is extensional, φx=φy⇒φΦ⁡(x)=φΦ⁡(y) _x= _y _ (x)= _ (y), so Φ descends to a well-defined Φ~ on behaviours: Φ~(g):=φΦ⁡(x) (g):= _ (x) for any x with φx=g _x=g (representative-independent by extensionality). Then Q:=g∈PC:g∈P~∧Φ~(g)∈P~Q:=\g :g∈ P (g)∈ P\ is an ordinary behavioural property, and its index set equals ΛΦ(P) _ (P) by construction. Q is non-trivial by P-disruption, so Rice applies directly and ΛΦ(P) _ (P) is undecidable. ∎ The difference from Theorem 4.4 is exactly one of jurisdiction: here ΛΦ(P) _ (P) stays extensional (via the descent Φ~ ) and one application of Rice suffices; lifting extensionality (the intensional regime), the descent no longer exists, ΛΦ(P) _ (P) ceases to be behavioural, Rice loses jurisdiction, and Kleene’s recursion theorem is required (Lemma 3.6). This places the extensional/intensional line as the boundary between two regimes of undecidability: below it the persistence is undecidable by Rice; lifting it—intensional transformations, which model genuine self-modification—undecidability does not vanish but changes engine, now depending on Kleene’s recursion theorem. The Expressivity Principle holds on both sides of the line; what changes is why. With Proposition 5.1, Theorem 4.4 and Theorem 4.7, the recursion-theoretic map of preservation under transformation is covered in both regimes (extensional/intensional) and both horizons (one step / ω-limit). 6. The supervisory regress does not terminate A natural way to evade the undecidability of persistence is to delegate it: if no simple decider can certify M0M_0, perhaps a supervisor M1M_1 (at least as capable) can verify it, an M2M_2 can verify M1M_1, and so on. We show the regress does not end: each level re-inherits the undecidability of the one below. The result holds on both sides of the extensional/intensional line, by the same induction, changing only which undecidability theorem is invoked at each step. We formalise “Mn+1M_n+1 supervises MnM_n” as: Mn+1M_n+1 purports to certify the persistence of the safety property for MnM_n—that is, to pronounce on the set ΛΦn(P) _ _n(P) of the lower level. A supervisor is adequate if it audits the full semantic behaviour of MnM_n over an unbounded domain. Lemma 6.1 (lower bound on supervisory expressive capacity). Let MnM_n be Turing-complete. A supervisor Mn+1M_n+1 bounded in resources (halting after a number of steps bounded by its capacity Kn+1K_n+1) is necessarily incomplete for auditing the semantic safety of MnM_n over an unbounded domain. Proof. Bounded resources ⇒ bounded time. By definition, Mn+1M_n+1 issues its verdict after t⁡(Kn+1)<∞t(K_n+1)<∞ steps. Bounded time ⇒ finite inspection horizon. In t⁡(Kn+1)t(K_n+1) steps Mn+1M_n+1 can have simulated or inspected only a finite prefix of MnM_n’s trajectory: the configurations up to some step τ⁡(Kn+1)τ(K_n+1). The behaviour of MnM_n beyond τ⁡(Kn+1)τ(K_n+1) is outside the effectively computed scope. Its observation window is thus a proper finite subset ⊆0,…,τ⁡(Kn+1)⊊ℕO \0,…,τ(K_n+1)\ . (This follows from the time bound, not a memory bound; the conclusion invokes neither Myhill–Nerode nor the pumping lemma.) Finite horizon ⇒ incompleteness. As MnM_n is Turing-complete, there is a self-modification trajectory staying in P~ P for all t≤τ⁡(Kn+1)t≤τ(K_n+1) and violating it at t∗=τ⁡(Kn+1)+1∉t =τ(K_n+1)+1 . Mn+1M_n+1, seeing only O, certifies this trajectory as safe though it contains a genuine violation outside its horizon: it is unsound or incomplete. ∎ Remark 6.2 (pure-recognition case). The lemma is stated for resource-bounded supervisors—the relevant class, since a supervisor that must issue a verdict is time-bounded. A sub-Turing model defined by recognition power rather than time (a finite or pushdown automaton reading the whole trajectory) would fail for a different reason: by Myhill–Nerode, there exist two trajectories of MnM_n—one safe, one violating P~ P—that the automaton cannot distinguish (same equivalence class), so it returns the same verdict for both and is likewise unsound or incomplete. The conclusion is the same; the mechanism (indistinguishability vs. finite horizon) differs. We do not develop this case, as the resource-bounded one already covers the tower. Theorem 6.3 (non-termination of the supervisory regress). Let M0M_0 have transition operator Φ0 _0 with ΛΦ0(P) _ _0(P) undecidable (by Proposition 5.1 if Φ0 _0 is extensional, by Theorem 4.4 if intensional). Then no finite tower M0,M1,…,MkM_0,M_1,…,M_k yields a total correct certificate of persistence. Proof. By induction, via a two-horned dilemma. Base: ΛΦ0(P) _ _0(P) is undecidable by hypothesis. Step: assume level n’s persistence is undecidable, and consider any Mn+1M_n+1; it is sub-Turing or Turing-complete, and neither horn closes the certification. Horn 1 (Mn+1M_n+1 a total decider). If Mn+1M_n+1 were a total correct decider of level n’s persistence, it would decide ΛΦn(P) _ _n(P), contradicting the inductive hypothesis. No supervisor can be a total correct decider; in particular a resource-bounded one is necessarily incomplete (Lemma 6.1). Horn 2 (Mn+1M_n+1 adequate ⇒ Turing-complete). If Mn+1M_n+1 audits the full semantic behaviour of MnM_n over an unbounded domain, then by Lemma 6.1 it must be Turing-complete and, a self-modifying Turing-complete system in turn. Its own persistence ΛΦn+1(P) _ _n+1(P) is then undecidable by the same theorem (Proposition 5.1 or Theorem 4.4), and the next-level supervisor inherits the same obstruction. Neither horn yields a total correct certificate; by induction no finite level closes the regress. ∎ Corollary 6.4 (the two faces of the tower). The regress terminates neither for extensional supervisors (Horn 2 via Proposition 5.1) nor for intensional ones (Horn 2 via Theorem 4.4). The intensional version—supervisors that self-modify by inspecting their own code—is not a separate result: it is Theorem 6.3 with Theorem 4.4 as the engine in Horn 2, in place of Proposition 5.1. The structure of this regress—hierarchical ascent, where each level’s property is “correctly supervise the level below”—differs from the temporal iteration of ΛΦω _ ^ω (§4), where P is fixed and what iterates is the rewriting of a single system. They should not be identified; §7.1 discusses whether both ascents are instances of a common scheme. 7. Open problems 7.1. A closure scheme for ascent operators Theorem 4.4 shows U is stable under the temporal elevation ΛΦ _ ; Theorem 6.3 shows the hierarchical supervisory ascent also re-inherits undecidability. What they share is not the structure of the iteration but the closure property that makes both fail. Conjecture 7.1 (closure scheme). There is an abstract class of “admissible ascent operators”—including temporal elevation and hierarchical supervision—under which U is closed. The closure theorem of this article and the non-termination of the supervisory tower would be two instances of one principle: every admissible ascent preserves non-verifiability. This is the most general form of the Expressivity Principle the present results suggest. Making it precise requires defining the class of ascent operators broadly enough to cover both cases yet narrowly enough not to trivialise closure—the same calibration challenge as the disruption condition here. (The intensional tower is not an open item: Theorem 6.3 covers it. What remains open is the abstract scheme subsuming the tower and ω-elevation as instances of a single closure theorem.) 7.2. The disruption frontier Theorem 3.8 gives one direction: every transformation in ℛinstR_inst is uniformly disruptive. The converse is open and perhaps more interesting: characterise exactly which transformations are disruptive, and determine the complexity of deciding it. Open Problem 7.2. Given a total computable Φ (say, by an index), is it decidable whether Φ is uniformly disruptive with respect to a given P~ P? We conjecture not: that the frontier between disruptive and non-disruptive transformations is itself undecidable. If so, the impossibility of verification would double: undecidable what a rewrite preserves, and undecidable also whether a rewrite is of the kind that makes it undecidable. This would be an additional result, independent of the article’s core, plausibly attacked by reduction from K. 7.3. The categorical reading in the effective topos The results of §4–5 are recursion-theoretic and invoke no category. There is, however, an explanatory reading—why the obstruction appears—that places them in Hyland’s effective topos and reveals them as instances of Lawvere’s fixed-point theorem. We sketch it as a programme; its full formalisation is work in progress. The central idea: in the effective topos, where morphisms are computable functions by construction, the truth object Ω is not Boolean and contains a proper tower 2↪Σ↪Ω2 (Boolean / Sierpiński–dominance / classifier). “P decidable” becomes “χP _P factors through 22”; “P∈P ” becomes “χP _P does not factor through 22”—a categorical condition with content precisely because 2↪Ω2 is proper there. The conjecture is that ΛΦ _ forces the non-factorisation through 22 of its values in U, by an application of Lawvere’s theorem to a fixed-point-free endomorphism of Ω , with the point-surjection built from the universal enumeration of PC. Three pieces to establish: (i) construct the Lawvere obstruction in EffEff for ΛΦ(P) _ (P), with Lawvere as the conclusion explaining the non-factorisation, not a premise; (i) prove the recursively defined U (§2.2) and the categorically defined one coincide under the standard translation; (i) formulate the correspondence between the effective non-realisability of gfp⁡(FP) (F_P) (the constructive failure of co-continuity in the effective topos) and the undecidability of ΛΦω _ ^ω (Theorem 4.7). If completed, the programme yields the deepest form of the Expressivity Principle: expressivity is the existence of the point-surjection onto the function space of the system itself, and it is exactly this morphism that, by Lawvere, forces the fixed point obstructing decision—so utility and non-verifiability are the same morphism seen twice. References [1] H. G. Rice, Classes of recursively enumerable sets and their decision problems, Trans. Amer. Math. Soc. 74 (1953), 358–366. [2] S. C. Kleene, On notation for ordinal numbers, J. Symbolic Logic 3 (1938), 150–155. [3] H. Rogers, Theory of Recursive Functions and Effective Computability, McGraw-Hill, New York, 1967. [4] R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, Berlin, 1987. [5] A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc. 2(42) (1936), 230–265. [6] F. W. Lawvere, Diagonal arguments and cartesian closed categories, in Category Theory, Homology Theory and their Applications I, Lecture Notes in Math. 92, Springer, 1969, 134–145. [7] N. S. Yanofsky, A universal approach to self-referential paradoxes, incompleteness and fixed points, Bull. Symbolic Logic 9(3) (2003), 362–386. [8] J. M. E. Hyland, The effective topos, in The L. E. J. Brouwer Centenary Symposium, North-Holland, 1982, 165–216.

Instant research discovery