Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2604.22844 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911704053448704 |
|---|---|
| author | Rahnama, Moses |
| author_facet | Rahnama, Moses |
| contents | We identify a structural property of term-rewriting proof systems called operational inexpressibility: no derivation depends on a specified input dimension and also constrains the target question. The canonical instance is direct aggregation on the primitive recursion duplicator $F(x,y,Z)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$, where the step argument $y$ is duplicated on the right. Under any direct whole-term measure the recursor's mass profile coincides with that of a true circular reference; the boundary operator's channel-preservation axiom and the dependency-pair soundness license separate them.
Sound responses split into construction methods (polynomial interpretations, path orderings) extending the proof language, and confession methods (dependency pairs, counter-projection, size-change termination, argument filtering) projecting away the unincorporable dimension under external license; all four share a projection rank and certified-forgetting interface. Arts-Giesl soundness is $Π^0_2$-combinatorial, formalizable in $\mathrm{I}Σ_1$, with an artifact-facing $ω^3$ termination measure inside $\mathrm{RCA}_0$, far below the $\varepsilon_0$-scale of classical Gödelian reflection.
The confessed burden grows quadratically across the canonical trace while residual proof work grows linearly. An architectural necessity theorem shows that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate. A Layer-Crossing-Under-External-License (LCEL) schema places the confession in the Feferman-Beklemishev reflection family rather than the Lawvere-Yanofsky diagonal family, recovering the six-step structural identity with Gödel 1931 as a specialization. A witness-language hierarchy with minimal order $κ^{}$ identifies the boundary as $κ^{}(x)>0$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_22844 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary Rahnama, Moses Logic in Computer Science We identify a structural property of term-rewriting proof systems called operational inexpressibility: no derivation depends on a specified input dimension and also constrains the target question. The canonical instance is direct aggregation on the primitive recursion duplicator $F(x,y,Z)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$, where the step argument $y$ is duplicated on the right. Under any direct whole-term measure the recursor's mass profile coincides with that of a true circular reference; the boundary operator's channel-preservation axiom and the dependency-pair soundness license separate them. Sound responses split into construction methods (polynomial interpretations, path orderings) extending the proof language, and confession methods (dependency pairs, counter-projection, size-change termination, argument filtering) projecting away the unincorporable dimension under external license; all four share a projection rank and certified-forgetting interface. Arts-Giesl soundness is $Π^0_2$-combinatorial, formalizable in $\mathrm{I}Σ_1$, with an artifact-facing $ω^3$ termination measure inside $\mathrm{RCA}_0$, far below the $\varepsilon_0$-scale of classical Gödelian reflection. The confessed burden grows quadratically across the canonical trace while residual proof work grows linearly. An architectural necessity theorem shows that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate. A Layer-Crossing-Under-External-License (LCEL) schema places the confession in the Feferman-Beklemishev reflection family rather than the Lawvere-Yanofsky diagonal family, recovering the six-step structural identity with Gödel 1931 as a specialization. A witness-language hierarchy with minimal order $κ^{}$ identifies the boundary as $κ^{}(x)>0$. |
| title | Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2604.22844 |