The Semantic Elevation Operator and the Closure of the Undecidable Class under Preservation
- URL: http://arxiv.org/abs/2609.11326v1
- Date: Thu, 10 Sep 2026 09:56:17 GMT
- Title: The Semantic Elevation Operator and the Closure of the Undecidable Class under Preservation
- Abstract summary: Self-modifying systems require analysing not whether a property holds now, but whether it is preserved when the system rewrites itself.<n>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?"<n>We prove that when is intensional, the elevated property remains undecidable even though it breaks the extensionality that Rice's theorem requires.
- Score: 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- 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
- Partial Identification under Causal Orders by Linear Programming [46.16293902963101]
We show that any counterfactual inquiry induces a partial, topological ordering over relevant variables.<n>This allows bounding arbitrary counterfactual and nested counterfactual queries.
arXiv Detail & Related papers (2026-08-25T11:42:38Z) - What Syntax Cannot See: The Dynamic Syntactic Invariance Principle and Several Instances of the Same Hidden Assumption, and a Contradiction [0.0]
This paper develops a single method, find what an accepted result silently assumed, make it a variable, and prove what follows once it is dropped.<n>It shows it keeps working across domains with nothing in common.
arXiv Detail & Related papers (2026-08-02T03:10:44Z) - A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus [5.076419064097734]
We give the first machine-checked account of a 1-topos core, in Cubical Agda.<n>We show that interventions and Pearl's rules are stable under every topology.<n>We add a phenomenon the programme does not consider: a machine-checked contextuality obstruction.
arXiv Detail & Related papers (2026-07-17T05:05:31Z) - The SIGReg Objective as Variational Free Energy: A Theoretical Active-Inference Account of JEPA World Models [47.471225029744424]
Joint-Embedding Predictive Architectures (JEPAs) are the dominant design for latent world models.<n>We show that the choice of anti-collapse regulariser determines whether a JEPA's training objective, a prediction loss plus a weighted embedding regulariser, is a valid Active Inference (AIF) variational free energy.
arXiv Detail & Related papers (2026-07-15T08:59:36Z) - Greedy Coordinate Diffusion: Effective and Semantically Coherent Adversarial Attacks via Diffusion Guidance [48.34904668359272]
Adrial attacks on large language models have limited practical impact despite extensive research.<n>We introduce Greedy Coordinate Diffusion (GCD), a novel framework that efficiently generates adversarial attacks against safety-aligned models.<n>GCD maintains low perplexity and high semantic adherence to the adversary's original intent.
arXiv Detail & Related papers (2026-06-14T01:18:53Z) - VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization [4.067416725742151]
We apply Verifiable Growing Physical Transformer with Recursive Self-Improvement to two RH-adjacent certification tasks.<n>First, we construct and verify a finite RH-boundary certificate for inequality on a parameterized safe lower curve over a region.<n>Second, we initiate a formal Lagarias-route certificate. Lagarias criterion states that RH is equivalent to the global inequality.
arXiv Detail & Related papers (2026-06-13T04:12:25Z) - Closing the Loop on Latent Reasoning via Test-Time Reconstruction [45.08180971427891]
Recent work moves intermediate reasoning from natural-language traces into latent or cache-level representations.<n>We propose ReLAT, a self-supervised test-time training method that closes this loop using the query itself as the reference.<n>We show that ReLAT consistently improves over single-model inference, text-based collaboration, open-loop latent collaboration, and alternative test-time training objectives.
arXiv Detail & Related papers (2026-06-04T14:54:40Z) - A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem [0.0]
Rice's theorem states that no non-trivial semantic property of programs is decidable.<n>We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP)<n>The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot)
arXiv Detail & Related papers (2026-04-11T20:45:58Z) - The Computational Boundary of Inference: Capability Internalization, Training, and the Turing Jump [0.0]
This paper gives a formal separation result in classical computability theory.<n>We prove that finite internal self-modification remains inside $mathcalC(A)$, while stabilized revision is governed by the jump $A'$ via the relativized limit lemma.
arXiv Detail & Related papers (2026-04-09T22:56:56Z) - Exact Structural Abstraction and Tractability Limits [0.0]
Exact correctness depends only on the induced classes $s sim_R simation' iff mathrmAdm_R(s)$.<n>Decision, search, approximation, statistical, randomized horizon, and distributional guarantees all reduce to this same quotient-recovery problem.
arXiv Detail & Related papers (2026-04-08T17:59:47Z) - Proving Theorems Recursively [80.42431358105482]
We propose POETRY, which proves theorems in a level-by-level manner.
Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level.
We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
arXiv Detail & Related papers (2024-05-23T10:35:08Z) - Some consequences of Sica's approach to Bell's inequalities [55.2480439325792]
Louis Sica derived Bell's inequalities from the hypothesis that the time series of outcomes observed in one station does not change if the setting in the other station is changed.
In this paper, Sica's approach is extended to series with non ideal efficiency and to the actual time structure of experimental data.
arXiv Detail & Related papers (2024-03-05T13:59:52Z) - On the Convergence of Gradient Descent for Large Learning Rates [55.33626480243135]
We show that convergence is impossible when a fixed step size is used.<n>We provide a proof of this in the case of linear neural networks with a squared loss.<n>We also prove the impossibility of convergence for more general losses without requiring strong assumptions such as Lipschitz continuity for the gradient.
arXiv Detail & Related papers (2024-02-20T16:01:42Z) - Partial Counterfactual Identification of Continuous Outcomes with a
Curvature Sensitivity Model [30.77874108094485]
We propose a novel sensitivity model called Curvature Sensitivity Model.
This allows us to obtain informative bounds by bounding the curvature of level sets of the functions.
We then propose an implementation of our Curvature Sensitivity Model in the form of a novel deep generative model.
arXiv Detail & Related papers (2023-06-02T10:30:37Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.