pith. sign in

arxiv: 2606.17275 · v1 · pith:67CJHNVRnew · submitted 2026-06-15 · 💻 cs.LO · cs.CR

Syntactic Systems Cannot See Semantic Invariants

Fabio F.G. Buono This is my paper

Pith reviewed 2026-06-27 02:04 UTC · model grok-4.3

classification 💻 cs.LO cs.CR
keywords syntactic systemssemantic invariantsclause set cyclesopen inductionaddition commutativitySkolem constantsinduction theories
0
0 comments X

The pith

Clause set cycles cannot prove that addition commutes when one argument is a Skolem constant.

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

The paper shows that clause set cycles and open induction are incomparable theories of induction. It does so by proving that clause set cycles have no way to rewrite the terms a plus b and b plus a when a is a Skolem constant, because addition rules only apply when the first argument is zero or a successor. This means the systems cannot reach the fact that addition is commutative, which is a property of the numbers rather than the symbols. A sympathetic reader would care because it identifies a precise limit on what purely syntactic rewriting systems can establish about arithmetic.

Core claim

The rules for addition can only fire when the first argument is 0 or a successor, a Skolem constant is neither, so the terms a+b and b+a can never be touched, and a machine that can never touch them can never prove they are equal. The thing that separates the two theories is the order of two constants, and that order is a fact about numbers, not about symbols.

What carries the argument

The restriction of addition rules in clause set cycles to cases where the first argument is 0 or a successor.

If this is right

  • Clause set cycles cannot prove a + b = b + a for Skolem constants a and b.
  • Open induction and clause set cycles are incomparable.
  • The separation between the theories rests on a semantic fact about numbers rather than syntactic properties of symbols.

Where Pith is reading between the lines

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

  • The shape of this argument may appear in the barriers to settling P versus NP.
  • A fast SAT algorithm might in some cases exist only as a function on numbers rather than as an explicit machine that can be written down.

Load-bearing premise

The addition rules in clause set cycles are restricted exactly to the cases where the first argument is 0 or a successor, without other mechanisms that could apply across Skolem constants.

What would settle it

A derivation within clause set cycles that proves a + b = b + a for distinct Skolem constants a and b.

read the original abstract

We start from a small open question, where Hetzl and Vierling asked whether two theories of induction, open induction and clause set cycles, are incomparable. They proved one direction and left the other open. Here we close it, and the proof is almost embarrassingly short, because the rules for addition can only fire when the first argument is $0$ or a successor, a Skolem constant is neither, so the terms $a{+}b$ and $b{+}a$ can never be touched, and a machine that can never touch them can never prove they are equal. The thing that separates the two theories is the order of two constants, and that order is a fact about numbers, not about symbols. We extract from this proof a small general principle, the Syntactic Invariance Principle, that names the shape of such arguments. We then close with a few speculative remarks on how this same shape appears, informally, in the known barriers to settling $\mathsf{P}$ versus $\mathsf{NP}$, where each barrier seems to point to a level of description that the techniques in the barrier cannot reach. We raise this as a suggestion rather than a theorem, since the analogy is real but we do not push it past the point where we can defend it. Along the way we raise an open question that the analogy suggests but does not settle, on whether a fast algorithm for $\SAT$, were it to exist, would always be exhibitable as a machine you can write down or whether it could be found, in some cases, only as a function on the numbers.

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

1 major / 2 minor

Summary. The manuscript resolves the open direction of an incomparability question posed by Hetzl and Vierling between open induction and clause set cycles. It does so via a short syntactic argument: with distinct Skolem constants a and b, the addition axioms (which apply only when the first argument is 0 or a successor) cannot reduce a+b or b+a, so neither system can derive their equality. The paper extracts a general 'Syntactic Invariance Principle' from this observation and offers speculative remarks on how analogous limitations appear in known barriers to P versus NP, including an open question on whether a fast SAT algorithm must always be exhibitable.

Significance. If the argument is correct, the result supplies a direct, parameter-free separation of the two induction theories that turns on a purely syntactic limitation with respect to semantic facts about the naturals. The Syntactic Invariance Principle is a cleanly stated abstraction that may be reusable in other settings. The P-versus-NP discussion is explicitly labeled as suggestive rather than proven and raises a concrete open question about exhibitable algorithms.

major comments (1)
  1. [Main proof] The central argument (abstract and main proof) asserts that addition rules fire only when the first argument is 0 or a successor and that the Hetzl-Vierling setup contains no additional mechanisms that would allow rewriting across Skolem constants. The manuscript should quote or reproduce the precise addition clauses and the definitions of open induction and clause-set cycles to permit direct verification that the rules indeed fail to apply to a and b.
minor comments (2)
  1. [Speculative remarks] The speculative section on P versus NP is clearly demarcated as non-theorem, but the open question about exhibitable SAT algorithms could be stated as a standalone, precisely formulated question at the end of the paper.
  2. A brief comparison table or diagram contrasting the two induction systems with respect to the Skolem-constant example would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment, the clear summary of the contribution, and the recommendation of minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: The central argument (abstract and main proof) asserts that addition rules fire only when the first argument is 0 or a successor and that the Hetzl-Vierling setup contains no additional mechanisms that would allow rewriting across Skolem constants. The manuscript should quote or reproduce the precise addition clauses and the definitions of open induction and clause-set cycles to permit direct verification that the rules indeed fail to apply to a and b.

    Authors: We agree that explicit quotation of the relevant clauses improves direct verifiability. In the revised version we will insert, immediately before the main argument, the standard definitions of open induction and clause-set cycles together with the precise addition clauses used in the Hetzl-Vierling framework (the two recursive equations that apply only when the first argument is 0 or a successor term). This addition is purely expository and leaves the short syntactic argument unchanged. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is direct syntactic observation

full rationale

The paper's central step shows that addition rules (from the Hetzl-Vierling axiomatization) apply only to 0 or successor arguments, so Skolem constants a and b leave a+b and b+a untouched and thus unprovably equal. This is a direct consequence of the external setup's rule conditions, with no reduction to self-definitions, fitted parameters renamed as predictions, or load-bearing self-citations. The author (Buono) does not overlap with Hetzl-Vierling, and the argument invokes no uniqueness theorems or ansatzes from prior work by the same authors. The Syntactic Invariance Principle is extracted post hoc as a naming of the observed shape rather than a renaming of a known result that bears the load. The P vs NP remarks are explicitly speculative and non-load-bearing. The derivation is therefore self-contained against the cited external benchmark.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the standard definitions of the two induction theories from the cited prior work and the syntactic restriction on addition rules; no new free parameters or invented entities are introduced beyond naming the extracted principle.

axioms (2)
  • domain assumption Addition rules in the systems apply only when the first argument is 0 or a successor term.
    Invoked directly in the proof sketch to show why Skolem-constant terms cannot be rewritten.
  • standard math A Skolem constant is neither 0 nor a successor.
    Standard property of Skolem constants in the logical setting.
invented entities (1)
  • Syntactic Invariance Principle no independent evidence
    purpose: Names the general shape of arguments where syntactic systems cannot reach semantic invariants such as commutativity.
    Extracted from the specific proof; no independent evidence supplied beyond the current argument.

pith-pipeline@v0.9.1-grok · 5810 in / 1326 out tokens · 34956 ms · 2026-06-27T02:04:20.521387+00:00 · methodology

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. The Observer World: A Cryptographic Extension of Impagliazzo's Five Worlds

    cs.CR 2026-06 unverdicted novelty 7.0

    Adding an observational axis to Impagliazzo's five worlds reveals unconditional collapses such as P^{O_prof} = NP^{O_prof} ⊂ P that hold in all five worlds, showing observational blindness and computational hardness a...

Reference graph

Works this paper leans on

21 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    Aaronson and A

    S. Aaronson and A. Wigderson. Algebrization: a new barrier in complex- ity theory.ACM Transactions on Computation Theory, 1(1), article 2, 2009. doi:10.1145/1490270.1490272

    work page doi:10.1145/1490270.1490272 2009

  2. [2]

    Baker and John Gill and Robert Solovay , title =

    T. Baker, J. Gill, and R. Solovay. Relativizations of theP=? NP question.SIAM Journal on Computing, 4(4):431–442, 1975. doi:10.1137/0204037

    work page doi:10.1137/0204037 1975

  3. [3]

    F. F. G. Buono. A new type of cipher. Preprint, arXiv:1202.2004, 2012. arXiv:1202.2004

    Pith/arXiv arXiv 2004

  4. [4]

    P. J. Cohen. The independence of the continuum hypothesis.Proceedings of the National Academy of Sciences, 50(6):1143–1148, 1963. doi:10.1073/pnas.50.6.1143

    work page doi:10.1073/pnas.50.6.1143 1963

  5. [5]

    S. A. Cook. The complexity of theorem proving procedures. InProceedings of STOC 1971, pp. 151–158. ACM, 1971. doi:10.1145/800157.805047

    work page doi:10.1145/800157.805047 1971

  6. [6]

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

    K. G¨ odel.¨Uber formal unentscheidbare S¨ atze der Principia Mathematica und ver- wandter Systeme I.Monatshefte f¨ ur Mathematik und Physik, 38:173–198, 1931. doi:10.1007/BF01700692

    work page doi:10.1007/bf01700692 1931

  7. [7]

    Hetzl and J

    S. Hetzl and J. Vierling. Clause set cycles and induction.Logical Methods in Computer Science, 16(4), 2020. doi:10.23638/LMCS-16(4:3)2020

    work page doi:10.23638/lmcs-16(4:3)2020 2020

  8. [8]

    Hetzl and J

    S. Hetzl and J. Vierling. Unprovability results for clause set cycles.Theoretical Computer Science, 935:21–46, 2022. doi:10.1016/j.tcs.2022.08.022

    work page doi:10.1016/j.tcs.2022.08.022 2022

  9. [9]

    Hetzl and J

    S. Hetzl and J. Weiser. Subsystems of open induction. Preprint, arXiv:2509.05653,

    arXiv

  10. [10]

    R. M. Karp. Reducibility among combinatorial problems. In R. E. Miller and J. W. Thatcher (eds.),Complexity of Computer Computations, pp. 85–103. Plenum Press, 1972. doi:10.1007/978-1-4684-2001-2 9

    work page doi:10.1007/978-1-4684-2001-2 1972

  11. [11]

    Kersani and N

    A. Kersani and N. Peltier. Combining superposition and induction: a practical realization. InFroCoS 2013, Lecture Notes in Computer Science, vol. 8152, pp. 70–86. Springer, 2013. doi:10.1007/978-3-642-40885-4 6

    work page doi:10.1007/978-3-642-40885-4 2013

  12. [12]

    Landauer

    R. Landauer. Irreversibility and heat generation in the computing process.IBM Journal of Research and Development, 5(3):183–191, 1961. doi:10.1147/rd.53.0183

    work page doi:10.1147/rd.53.0183 1961

  13. [13]

    Matiyasevich

    Y. Matiyasevich. Enumerable sets are Diophantine.Soviet Mathematics Doklady, 11:354–358, 1970

    1970

  14. [14]

    Mohsenipour

    S. Mohsenipour. Hierarchies of subsystems of weak arithmetic. In J. Kennedy and R. Kossak (eds.),Set Theory, Arithmetic, and Foundations of Mathematics, Lecture Notes in Logic, vol. 36, pp. 80–92. Cambridge University Press, 2011. arXiv:1003.2117

    Pith/arXiv arXiv 2011

  15. [15]

    K. D. Mulmuley and M. Sohoni. Geometric complexity theory I: an approach to the P vs. NP and related problems.SIAM Journal on Computing, 31(2):496–526, 2001. doi:10.1137/S009753970038715X

    work page doi:10.1137/s009753970038715x 2001

  16. [16]

    Montanari

    A. Montanari. Unification in linear time and space: a structured presentation. Internal report, Istituto di Scienze dell’Informazione, Universit` a di Pisa, 1976. https://hdl.handle.net/20.500.14243/382610

    1976

  17. [17]

    Razborov and S

    A. Razborov and S. Rudich. Natural proofs.Journal of Computer and System Sciences, 55(1):24–35, 1997. doi:10.1006/jcss.1997.1494

    work page doi:10.1006/jcss.1997.1494 1997

  18. [18]

    J. A. Robinson. A machine-oriented logic based on the resolution principle.Journal of the ACM, 12(1):23–41, 1965. doi:10.1145/321250.321253

    work page doi:10.1145/321250.321253 1965

  19. [19]

    J. C. Shepherdson. A non-standard model for a free variable fragment of number theory.Bulletin de l’Acad´ emie Polonaise des Sciences, 12:79–86, 1964

    1964

  20. [20]

    Williams

    R. Williams. Nonuniform ACC circuit lower bounds.Journal of the ACM, 61(1), article 2, 2014. doi:10.1145/2559903

    work page doi:10.1145/2559903 2014

  21. [21]

    F. F. G. Buono. New Ideas on a New Old Type of Cipher: The Mixed-Radix One-Time Pad. Zenodo, 2026. doi:10.5281/zenodo.20614326. 7

    work page doi:10.5281/zenodo.20614326 2026