Rice's Theorem under Self-Modification: Elevation Operators and a Normal Form
cs.LO, cs.AI, cs.CL, math.LO
Submitted: 2026-09-10
Updated: 2026-09-28
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
The gist: The undecidability of a program's static semantic properties is governed by Rice's theorem.
Terminology
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 Π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.
Related papers
- An Information-Flow Perspective on Explainability Requirements: Specification and Verification
- A programming language combining quantum and classical control
- Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
- Encoder-Decoder Transformers: Logical Characterizations and Periodicity
- Ultraconstructive Model Theory via Bounded Adversarial Finite Structures