pith. sign in

arxiv: 2604.22844 · v3 · pith:DK5UXYZ4new · submitted 2026-04-21 · 💻 cs.LO

Operational Inexpressibility at the Step-Duplicating Primitive Recursor Orientation Boundary

Moses Rahnama This is my paper

Pith reviewed 2026-05-22 11:11 UTC · model grok-4.3

classification 💻 cs.LO
keywords operational inexpressibilityprimitive recursion duplicatorterm rewritingdependency pairsproof systemsreflection principlesarchitectural necessity
0
0 comments X

The pith

Operational inexpressibility arises because no derivation can depend on a specified input dimension while constraining the target question.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper identifies a structural property in term-rewriting proof systems known as operational inexpressibility, where no derivation depends on a specified input dimension and also constrains the target question. The canonical case appears in the primitive recursion duplicator that copies the step argument y onto the right-hand side of the recursive rule. If the property holds, then all sound responses split into construction methods that enlarge the proof language and confession methods that project away the dimension under external license. The work proves an architectural necessity theorem requiring duplication for any first-order step rule that emits a per-step record while preserving its generator. It situates the confession inside a reflection hierarchy rather than a diagonal argument.

Core claim

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)→x, F(x,y,S(n))→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.

What carries the argument

The primitive recursion duplicator F(x,y,Z)→x, F(x,y,S(n))→G(y,F(x,y,n)) that duplicates the step argument y on the right-hand side, which coincides with a circular reference under direct whole-term measures but is separated by the boundary operator.

If this is right

  • Sound responses split into construction methods such as polynomial interpretations and path orderings that extend the proof language, and confession methods such as dependency pairs that project away the dimension.
  • All four families of methods share a common projection rank and certified-forgetting interface.
  • The confessed burden grows quadratically along the canonical trace while residual proof work grows linearly.
  • Any first-order step rule that emits a per-step record frame while preserving its generator must duplicate.
  • The Layer-Crossing-Under-External-License schema recovers the six-step structural identity with Gödel 1931 as a special case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The distinction between the duplicator and a genuine circular reference may guide the design of automated termination checkers for recursive programs in functional languages.
  • The witness-language hierarchy with minimal order kappa could classify other inexpressible constructs across different proof systems.
  • The reflection-family placement suggests testable connections between termination arguments and ordinal analyses in proof theory.

Load-bearing premise

The boundary operator's channel-preservation axiom together with dependency-pair soundness separates the recursor mass profile from that of a true circular reference under any direct whole-term measure.

What would settle it

A concrete derivation that depends on the duplicated step dimension y while still constraining the target question, or a mass-profile calculation in which the recursor and a circular reference remain indistinguishable after the boundary operator is applied.

read the original abstract

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 $\Pi^0_2$-combinatorial, formalizable in $\mathrm{I}\Sigma_1$, with an artifact-facing $\omega^3$ termination measure inside $\mathrm{RCA}_0$, far below the $\varepsilon_0$-scale of classical G\"odelian 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\"odel 1931 as a specialization. A witness-language hierarchy with minimal order $\kappa^{}$ identifies the boundary as $\kappa^{}(x)>0$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The manuscript identifies a structural property termed 'operational inexpressibility' in term-rewriting proof systems: no derivation depends on a specified input dimension while also constraining the target question. The canonical case is the primitive recursion duplicator with rules F(x,y,Z)→x and F(x,y,S(n))→G(y,F(x,y,n)), where the step argument y is duplicated. Under direct whole-term measures the recursor's mass profile coincides with circular references, but the boundary operator's channel-preservation axiom together with dependency-pair soundness separate them. The paper classifies handling methods into construction (polynomial interpretations, path orderings) and confession (dependency pairs, counter-projection, size-change termination, argument filtering) approaches that share a projection rank and certified-forgetting interface; it states that Arts-Giesl soundness is Π⁰₂-combinatorial and formalizable in IΣ₁ with an ω³ termination measure inside RCA₀; it proves an architectural necessity theorem that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate; and it situates the confession inside an LCEL schema belonging to the Feferman-Beklemishev reflection family, recovering a six-step structural identity with Gödel 1931 as a special case, while introducing a witness-language hierarchy with minimal order κ.

Significance. If the claimed separations, necessity theorem, and complexity bounds hold, the work supplies a new structural lens on duplicating recursors in termination analysis and proof systems, together with an explicit embedding into reflection hierarchies that recovers classical diagonal arguments as instances. The explicit placement of Arts-Giesl soundness inside IΣ₁ and RCA₀ with a concrete ω³ measure, the distinction between quadratic confessed burden and linear residual proof work, and the architectural necessity result constitute concrete, checkable contributions that could inform both automated termination tools and proof-theoretic classifications.

major comments (2)
  1. [Architectural necessity theorem / LCEL schema section] The architectural necessity theorem (stated in the abstract and presumably proved in the section developing the LCEL schema) asserts that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate. The precise statement of the theorem, the exact hypotheses on 'record frame' and 'preserving its generator', and the key inference step that forces duplication should be exhibited explicitly so that the load-bearing claim can be verified against the term-rewriting rules given for the duplicator.
  2. [Separation argument / boundary operator subsection] The claim that the boundary operator's channel-preservation axiom plus dependency-pair soundness separates the recursor's mass profile from that of a true circular reference (abstract, paragraph 1) is central to the operational-inexpressibility distinction. The manuscript should supply the exact formulation of the channel-preservation axiom and the dependency-pair soundness lemma that licenses the separation, together with the direct whole-term measure under which the profiles otherwise coincide.
minor comments (3)
  1. [Witness-language hierarchy paragraph] The witness-language hierarchy with minimal order κ is introduced without an explicit inductive definition or base case; a short formal definition of κ(x) and the ordering would clarify how κ(x)>0 identifies the boundary.
  2. [LCEL schema / reflection family subsection] The six-step structural identity with Gödel 1931 is recovered as a specialization of the LCEL schema; a brief side-by-side comparison of the six steps would help readers see the claimed correspondence.
  3. [Canonical instance paragraph] Notation for the duplicator rules uses Z and S(n) without prior declaration; a single sentence fixing the signature and the meaning of the step argument y would remove ambiguity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and the recommendation of major revision. The comments highlight areas where explicit formulations will improve clarity and verifiability. We address each major comment below and will incorporate the requested details in the revised manuscript.

read point-by-point responses

  1. Referee: [Architectural necessity theorem / LCEL schema section] The architectural necessity theorem (stated in the abstract and presumably proved in the section developing the LCEL schema) asserts that any first-order step rule emitting a per-step record frame while preserving its generator must duplicate. The precise statement of the theorem, the exact hypotheses on 'record frame' and 'preserving its generator', and the key inference step that forces duplication should be exhibited explicitly so that the load-bearing claim can be verified against the term-rewriting rules given for the duplicator.

    Authors: We agree that the architectural necessity theorem should be stated with full precision to allow direct verification. In the revised version we will insert a formal theorem statement (with numbered hypotheses) that defines a 'per-step record frame' as the auxiliary structure emitted by the rule at each successor step and 'preserving its generator' as the requirement that the original generator term remains syntactically intact in the right-hand side. The key inference step, which proceeds by contradiction from the first-order restriction and the requirement to emit the frame without altering the generator, will be spelled out explicitly and cross-referenced to the duplicator rules F(x,y,Z)→x and F(x,y,S(n))→G(y,F(x,y,n)). revision: yes

  2. Referee: [Separation argument / boundary operator subsection] The claim that the boundary operator's channel-preservation axiom plus dependency-pair soundness separates the recursor's mass profile from that of a true circular reference (abstract, paragraph 1) is central to the operational-inexpressibility distinction. The manuscript should supply the exact formulation of the channel-preservation axiom and the dependency-pair soundness lemma that licenses the separation, together with the direct whole-term measure under which the profiles otherwise coincide.

    Authors: We accept that the separation argument requires the supporting axioms and lemmas to be written out. In the revision we will state the channel-preservation axiom for the boundary operator in full, present the dependency-pair soundness lemma (including its hypotheses on the dependency relation), and specify the direct whole-term measure (a size function that counts all subterms without projection) under which the mass profiles of the duplicator and a circular reference coincide. The subsequent application of the axiom and lemma that yields the separation will then be shown step by step. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines operational inexpressibility directly from the structural property that no derivation depends on a specified input dimension while constraining the target question, using the duplicator recursor as a canonical instance. Separation from circular references relies on the boundary operator's channel-preservation axiom and dependency-pair soundness as external licenses, with the architectural necessity theorem and LCEL schema placement referencing established reflection families (Feferman-Beklemishev) and known soundness results (Arts-Giesl, Π⁰₂-combinatorial in IΣ₁) without reducing any central quantity to a self-referential definition, fitted parameter, or self-citation chain by construction. Growth distinctions (quadratic vs linear) and measure placements (ω³ in RCA₀) are presented as independent observations against external benchmarks, rendering the derivation self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 3 invented entities

The abstract relies on several unproven background assumptions from proof theory and rewriting systems without providing independent evidence for them in the visible text.

axioms (3)
  • domain assumption channel-preservation axiom of the boundary operator
    Invoked to separate the recursor mass profile from circular references
  • domain assumption dependency-pair soundness
    Licenses the separation of duplicating behavior from circularity
  • domain assumption Arts-Giesl soundness is Π⁰₂-combinatorial and formalizable in IΣ₁
    Stated as background for the termination measure
invented entities (3)
  • operational inexpressibility no independent evidence
    purpose: Structural property capturing when no derivation depends on a specified input dimension while constraining the target
    Newly identified in the paper as the central concept
  • LCEL schema no independent evidence
    purpose: Places the confession method in the Feferman-Beklemishev reflection family
    Introduced to recover the structural identity with Gödel 1931
  • witness-language hierarchy with minimal order κ no independent evidence
    purpose: Identifies the boundary as κ(x)>0
    Defined to characterize the orientation boundary

pith-pipeline@v0.9.0 · 5867 in / 1613 out tokens · 40806 ms · 2026-05-22T11:11:28.172520+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages · 5 internal anchors

  1. [1]

    A Structural Approach to Reversible Computation

    Samson Abramsky. A structural approach to reversible computation.Theoretical Computer Science, 347(3):441–464, 2005. arXiv:1111.7154

    work page internal anchor Pith review Pith/arXiv arXiv 2005

  2. [2]

    Termination of term rewriting using dependency pairs.Theoret- ical Computer Science, 236(1–2):133–178, 2000

    Thomas Arts and J¨ urgen Giesl. Termination of term rewriting using dependency pairs.Theoret- ical Computer Science, 236(1–2):133–178, 2000

    work page 2000

  3. [3]

    What do reversible programs compute? InFoundations of Software Science and Computation Structures (FoSSaCS 2011), volume 6604 ofLecture Notes in Computer Science, pages 42–56

    Holger Bock Axelsen and Robert Gl¨ uck. What do reversible programs compute? InFoundations of Software Science and Computation Structures (FoSSaCS 2011), volume 6604 ofLecture Notes in Computer Science, pages 42–56. Springer, 2011. 65

    work page 2011

  4. [4]

    Cambridge University Press, 1998

    Franz Baader and Tobias Nipkow.Term Rewriting and All That. Cambridge University Press, 1998

    work page 1998

  5. [5]

    Beklemishev

    Lev D. Beklemishev. Iterated local reflection versus iterated consistency.Annals of Pure and Applied Logic, 75(1–2):25–48, 1995

    work page 1995

  6. [6]

    Beklemishev

    Lev D. Beklemishev. Reflection principles and provability algebras in formal arithmetic.Russian Mathematical Surveys, 60(2):197–268, 2005

    work page 2005

  7. [7]

    Reflection calculus and conservativity spectra

    Lev D. Beklemishev. Reflection calculus and conservativity spectra.Russian Mathematical Surveys, 73(4):569–613, 2018. arXiv:1703.09314

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  8. [8]

    Charles H. Bennett. Logical reversibility of computation.IBM Journal of Research and Devel- opment, 17(6):525–532, 1973

    work page 1973

  9. [9]

    Proof-theoretic analysis of termination proofs.Annals of Pure and Applied Logic, 75(1-2):57–65, 1995

    Wilfried Buchholz. Proof-theoretic analysis of termination proofs.Annals of Pure and Applied Logic, 75(1-2):57–65, 1995

    work page 1995

  10. [10]

    A Curry–Howard correspondence for linear, reversible computation

    Kostia Chardonnet, Alexis Saurin, and Benoˆ ıt Valiron. A Curry–Howard correspondence for linear, reversible computation. InComputer Science Logic (CSL 2023), volume 252 ofLIPIcs, pages 13:1–13:18, 2023

    work page 2023

  11. [11]

    Transfinite recursive progressions of axiomatic theories.Journal of Symbolic Logic, 27(3):259–316, 1962

    Solomon Feferman. Transfinite recursive progressions of axiomatic theories.Journal of Symbolic Logic, 27(3):259–316, 1962

    work page 1962

  12. [12]

    Transfinite progressions: a second look at completeness.Bulletin of Symbolic Logic, 10(3):367–389, 2004

    Torkel Franz´ en. Transfinite progressions: a second look at completeness.Bulletin of Symbolic Logic, 10(3):367–389, 2004

    work page 2004

  13. [13]

    The strength of SCT soundness

    Emanuele Frittaion, Florian Pelupessy, Silvia Steila, and Keita Yokoyama. The strength of sct soundness.Journal of Logic and Computation, 28(6):1217–1242, 2018. arXiv:1709.09036

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  14. [14]

    Linear logic.Theoretical Computer Science, 50(1):1–101, 1987

    Jean-Yves Girard. Linear logic.Theoretical Computer Science, 50(1):1–101, 1987

    work page 1987

  15. [15]

    ¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und verwandter Systeme I.Monatshefte f¨ ur Mathematik und Physik, 38:173–198, 1931

    Kurt G¨ odel. ¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und verwandter Systeme I.Monatshefte f¨ ur Mathematik und Physik, 38:173–198, 1931

    work page 1931

  16. [16]

    Kurt G¨ odel.¨Uber eine bisher noch nicht ben¨ utzte erweiterung des finiten standpunktes.Dialec- tica, 12(3–4):280–287, 1958

    work page 1958

  17. [17]

    Termination proofs by multiset path orderings imply primitive recursive deriva- tion lengths.Theoretical Computer Science, 105(1):129–140, 1992

    Dieter Hofbauer. Termination proofs by multiset path orderings imply primitive recursive deriva- tion lengths.Theoretical Computer Science, 105(1):129–140, 1992

    work page 1992

  18. [18]

    Termination proofs and the length of derivations

    Dieter Hofbauer and Clemens Lautemann. Termination proofs and the length of derivations. In Rewriting Techniques and Applications (RTA 1989), volume 355 ofLecture Notes in Computer Science, pages 167–177. Springer, 1989

    work page 1989

  19. [19]

    Confluent reductions: abstract properties and applications to term rewriting systems.Journal of the ACM, 27(4):797–821, 1980

    G´ erard Huet. Confluent reductions: abstract properties and applications to term rewriting systems.Journal of the ACM, 27(4):797–821, 1980

    work page 1980

  20. [20]

    Richard Kennaway, Jan Willem Klop, M

    J. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. On the adequacy of graph rewriting for simulating term rewriting.ACM Transactions on Programming Languages and Systems, 16(3):493–523, 1994

    work page 1994

  21. [21]

    CWI, Amsterdam, 1980

    Jan Willem Klop.Combinatory Reduction Systems, volume 127 ofMathematical Centre Tracts. CWI, Amsterdam, 1980

    work page 1980

  22. [22]

    Reflection principles and their use for establishing the complexity of axiomatic systems.Zeitschrift f¨ ur mathematische Logik und Grundlagen der Mathematik, 14:97–142, 1968

    Georg Kreisel and Azriel L´ evy. Reflection principles and their use for establishing the complexity of axiomatic systems.Zeitschrift f¨ ur mathematische Logik und Grundlagen der Mathematik, 14:97–142, 1968

    work page 1968

  23. [23]

    William Lawvere

    F. William Lawvere. Diagonal arguments and cartesian closed categories. InCategory Theory, Homology Theory and Their Applications, II, volume 92 ofLecture Notes in Mathematics, pages 134–145. Springer, 1969. 66

    work page 1969

  24. [24]

    Springer, 4 edition, 2019

    Ming Li and Paul Vit´ anyi.An Introduction to Kolmogorov Complexity and Its Applications. Springer, 4 edition, 2019

    work page 2019

  25. [25]

    Proof Theory at Work: Complexity Analysis of Term Rewrite Systems

    Georg Moser. Proof theory at work: Complexity analysis of term rewrite systems, 2009. Habili- tation thesis, arXiv:0907.5527

    work page internal anchor Pith review Pith/arXiv arXiv 2009

  26. [26]

    The derivational complexity induced by the dependency pair method.Logical Methods in Computer Science, 7(3:1), 2011

    Georg Moser and Andreas Schnabl. The derivational complexity induced by the dependency pair method.Logical Methods in Computer Science, 7(3:1), 2011

    work page 2011

  27. [27]

    Reversible Computation in Term Rewriting

    Naoki Nishida, Adri´ an Palacios, and Germ´ an Vidal. Reversible computation in term rewriting. Journal of Logical and Algebraic Methods in Programming, 94:128–149, 2018. arXiv:1710.02804; online 2017, journal issue 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  28. [28]

    A class of reversible primitive recursive functions

    Luca Paolini, Mauro Piccolo, and Luca Roversi. A class of reversible primitive recursive functions. Electronic Notes in Theoretical Computer Science, 322:227–242, 2016

    work page 2016

  29. [29]

    Christopher P. Porter. Revisiting Chaitin’s incompleteness theorem.Notre Dame Journal of Formal Logic, 62(1):147–171, 2021

    work page 2021

  30. [30]

    On interpreting Chaitin’s incompleteness theorem.Journal of Philosophical Logic, 27(6):569–586, 1998

    Panu Raatikainen. On interpreting Chaitin’s incompleteness theorem.Journal of Philosophical Logic, 27(6):569–586, 1998

    work page 1998

  31. [31]

    The orientation boundary for step-duplicating recursors: Mechanized im- possibility, escape, and certification, 2025

    Moses Rahnama. The orientation boundary for step-duplicating recursors: Mechanized im- possibility, escape, and certification, 2025. Lean 4 mechanization:https : / / github . com / MosesRahnama/OperatorKO7

    work page 2025

  32. [32]

    Universitext

    Craig Smory´ nski.Self-Reference and Modal Logic. Universitext. Springer, 1985

    work page 1985

  33. [33]

    Cambridge University Press, 2003

    Terese.Term Rewriting Systems. Cambridge University Press, 2003

    work page 2003

  34. [34]

    Counterexamples to termination for the direct sum of term rewriting systems

    Yoshihito Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(3):141–143, 1987

    work page 1987

  35. [35]

    Termination proofs for term rewriting systems by lexicographic path order- ings imply multiply recursive derivation lengths.Theoretical Computer Science, 139(1-2):355–362, 1995

    Andreas Weiermann. Termination proofs for term rewriting systems by lexicographic path order- ings imply multiply recursive derivation lengths.Theoretical Computer Science, 139(1-2):355–362, 1995

    work page 1995

  36. [36]

    Yanofsky

    Noson S. Yanofsky. A universal approach to self-referential paradoxes, incompleteness and fixed points.Bulletin of Symbolic Logic, 9(3):362–386, 2003. 67

    work page 2003