Undecidable properties stay undecidable under system self-change
The Semantic Elevation Operator and the Closure of the Undecidable Class under Preservation
Logic in Computer ScienceArtificial IntelligenceComputation and Language
Summary
Some questions about computer programs are impossible to answer no matter what, due to a rule called Rice's theorem. This paper studies what happens when a program can rewrite itself, asking if certain properties stay true after the program changes. The authors show that even when a program changes itself based on its own code, these questions remain impossible to solve. They also prove that building ever more advanced verifiers won't solve this problem completely. Their findings deepen understanding of why certain program properties can never be fully verified.
What this means in practice
- •For program verification engineers: Avoid futile attempts to verify properties stable under self-modification by understanding that some properties remain undecidable despite source-based transformations.
- •For security analysts for self-adaptive systems: Recognize limits on automated guarantees for properties that must be preserved by self-modifying or evolving code systems in cybersecurity settings.
A theory result. No direct application yet.
Authors
Jose Pascual Gumbau Mezquita
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.