pith. sign in

arxiv: 2604.27787 · v1 · submitted 2026-04-30 · 💻 cs.CC · math.LO

Toward a Characterization of Simulation Between Arithmetic Theories

Hunter Monroe This is my paper

Pith reviewed 2026-05-07 06:10 UTC · model grok-4.3

classification 💻 cs.CC math.LO
keywords arithmetic theoriesconsistency statementspolynomial simulationproof systemsBusy Beaver functionrelative consistencybounded consistencyinterpretability
0
0 comments X

The pith

If EA cannot prove that consistency of S implies consistency of S plus a true sentence, then S cannot prove the bounded consistency statements in polynomial time.

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

The paper examines when a sound arithmetic theory S containing S^1_2 can efficiently simulate the extension S plus a true sentence phi by proving the bounded consistency statements Con_{S+phi}(n). It proves two unconditional results that constrain possible characterizations: if EA proves the consistency implication Con_S to Con_{S+phi}, then for finitely axiomatized sequential theories S interprets S+phi and provides polynomial-size proofs of the relevant consistency statements; and if S fails to simulate S+phi for any true phi, then it fails for certain Busy Beaver value statements phi_BB(k) for large k. The central conjecture asserts the converse direction, that absence of an EA-provable consistency implication implies no polynomial simulation for any fixed exponent c. If correct, this would mean relative consistency strength governs when one theory can efficiently establish the consistency of another.

Core claim

The paper proposes that relative consistency strength governs simulation: if EA does not prove Con_S implies Con_{S+phi}, then for every c greater than 0, S does not prove Con_{S+phi}(n) in n^c steps. For finitely axiomatized sequential theories, the converse holds unconditionally via interpretability, yielding polynomial simulation when the implication is provable in EA. Any simulation failure for a true phi also produces unprovable phi_BB(k) witnessing the same obstruction. This conjecture would imply hardness for canonical extensions such as phi equal to Con_S or a Kolmogorov-randomness axiom.

What carries the argument

The bounded consistency statement Con_{S+phi}(n), which asserts that the theory S plus phi has no proof of contradiction of length at most n; this statement measures efficient simulation between the theories viewed as proof systems.

If this is right

  • When phi is Con_S itself, the conjecture implies S cannot prove its own bounded consistency statements with polynomial size.
  • Similar polynomial hardness follows when phi is a Kolmogorov-randomness axiom.
  • Any argument that S fails to simulate some S+phi must also yield specific unprovable Busy Beaver values phi_BB(k) for large k as witnesses.
  • For finitely axiomatized sequential theories, an EA-provable consistency implication yields both interpretability and polynomial simulation of the consistency statements.

Where Pith is reading between the lines

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

  • The criterion may extend to characterize simulation for other classes of true sentences or for stronger consistency notions beyond bounded statements.
  • Simulation failures linked to Busy Beaver values suggest that proof-complexity obstructions can be translated into explicit computability bounds.
  • If the conjecture holds, it would imply that true but unprovable statements cannot be efficiently internalized in weaker theories without increasing proof size superpolynomially.
  • The unconditional results already rule out characterizations that ignore consistency implications entirely.

Load-bearing premise

The conjecture that an EA-provable consistency implication is necessary for any polynomial simulation between the theories.

What would settle it

A specific true sentence phi and theory S where EA does not prove Con_S implies Con_{S+phi} yet S proves Con_{S+phi}(n) with proof size at most n^c for some fixed c and all sufficiently large n.

read the original abstract

We study when a sound arithmetic theory $\mathcal S{\supseteq}S^1_2$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Con_{\mathcal S{+}\phi}(n)$ for a true sentence $\phi$. Equivalently, we ask when $\mathcal S$, viewed as a proof system, simulates $\mathcal S{+}\phi$. The paper's two unconditional contributions constrain possible characterizations. First, for finitely axiomatized sequential $\mathcal S$, if $EA{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then $\mathcal S$ interprets $\mathcal S{+}\phi$, implying ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S}(p(n)){\rightarrow}Con_{\mathcal S{+}\phi}(n)$ for some polynomial $p$, and hence ${\mathcal S}{\vdash^{n^{O(1)}}}Con_{\mathcal S{+}\phi}(n)$. Second, if $\mathcal S$ fails to simulate $\mathcal S{+}\phi$ for some true $\phi$, then for all sufficiently large $k$ it also fails for $\phi_{BB}(k)$ asserting the exact value of the $k$-state Busy Beaver function. Informally, any argument showing that $\mathcal S$ fails to simulate some $\mathcal S{+}\phi$ also yields unprovable $\phi_{BB}(k)$ witnessing the same obstruction. These results suggest that relative consistency strength is a serious candidate for governing when simulation is possible, while leaving open whether it is the correct criterion. The paper's central conjectural proposal is that the above sufficient condition is also necessary: if $EA{\not\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then for every constant $c{>}0$, ${\mathcal S}{\not\vdash^{n^c}}Con_{\mathcal S{+}\phi}(n)$. Under this proposal, hardness follows in canonical cases where $\phi$ is $Con_{\mathcal S}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.

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

0 major / 3 minor

Summary. The paper studies when a sound arithmetic theory S ⊇ S¹₂ with polynomial-time decidable axioms efficiently proves bounded consistency statements Con_{S+φ}(n) for true φ, equivalently when S simulates S+φ as a proof system. It establishes two unconditional results: for finitely axiomatized sequential S, EA ⊢ Con_S → Con_{S+φ} implies S interprets S+φ and thus S ⊢^{n^{O(1)}} Con_{S+φ}(n); and if S fails to simulate S+φ for some true φ then it fails for a Busy Beaver sentence φ_BB(k) for large k. The central conjecture is that EA ⊬ Con_S → Con_{S+φ} implies S ⊬^{n^c} Con_{S+φ}(n) for every c>0, with consequences for φ = Con_S and Kolmogorov-randomness axioms.

Significance. The two unconditional results provide concrete constraints on simulation and reduce potential counterexamples to Busy Beaver functions, which is a useful contribution to proof complexity and the study of arithmetic theories. The conjecture, if true, would characterize polynomial simulation in terms of relative consistency strength provable in EA, with further implications for canonical hard cases. The manuscript is careful to separate proven results from the open conjecture and relies on standard assumptions for sequential theories without circularity.

minor comments (3)
  1. The abstract is information-dense; separating the two unconditional results into distinct sentences would improve readability for readers scanning the contribution.
  2. The Busy Beaver sentence φ_BB(k) is introduced informally in the abstract; a formal definition or reference to its standard construction should appear in the main text near its first use.
  3. Notation such as ⊢^{n^{O(1)}} and the precise meaning of 'polynomial simulation' via bounded consistency could be recalled or cross-referenced in the introduction for accessibility to complexity theorists.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, the recognition that the two unconditional results provide useful constraints on simulation between arithmetic theories, and the acknowledgment that the central conjecture would offer a clean characterization if established. We appreciate the note that the paper carefully separates proven results from the open conjecture and avoids circularity in its assumptions about sequential theories. We will incorporate minor revisions to improve exposition, add clarifying remarks where helpful, and ensure all citations and technical details are polished.

Circularity Check

0 steps flagged

No significant circularity; unconditional results independent of open conjecture

full rationale

The paper explicitly separates two unconditional theorems (EA-provability of relative consistency implies interpretability and polynomial simulation; failure for some true φ implies failure for Busy Beaver sentences) from its central proposal, which is labeled an open conjecture and is not invoked to derive any claims. Both unconditional results rest on standard properties of sequential theories, interpretability, and bounded consistency statements in arithmetic, without self-definitional reductions, fitted parameters renamed as predictions, or load-bearing self-citations. The conjecture itself is not derived but proposed as a characterization to be investigated, leaving the derivation chain self-contained against external benchmarks in proof theory.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard axioms of proof theory and bounded arithmetic with no free parameters or invented entities.

axioms (1)
  • standard math Standard properties of EA, S^1_2, and sequential theories including soundness and polynomial-time axiom decidability.
    Invoked as background for consistency statements and simulation.

pith-pipeline@v0.9.0 · 9650 in / 956 out tokens · 125080 ms · 2026-05-07T06:10:02.501948+00:00 · methodology

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

14 extracted references · 14 canonical work pages

  1. [1]

    3, 32–54

    Scott Aaronson,The busy beaver frontier, SIGACT News51(2020), no. 3, 32–54

    work page 2020

  2. [2]

    Buss,Bounded arithmetic, Lecture notes, Bibliopolis, 1986

    Samuel R. Buss,Bounded arithmetic, Lecture notes, Bibliopolis, 1986

    work page 1986

  3. [3]

    Chaitin,Information-theoretic limitations of formal systems, JACM21(1974), no

    Gregory J. Chaitin,Information-theoretic limitations of formal systems, JACM21(1974), no. 3, 403–424

    work page 1974

  4. [4]

    1, 31–49

    Anton Freund and Fedor Pakhomov,Short proofs for slow consistency, Notre Dame Journal of Formal Logic61(2020), no. 1, 31–49

    work page 2020

  5. [5]

    Petr H´ ajek and Pavel Pudl´ ak,Metamathematics of first-order arithmetic, Perspectives in Logic, Cambridge University Press, 1998

    work page 1998

  6. [6]

    Erfan Khaniki,Jump operators, interactive proofs and proof complexity generators, 2024 IEEE 65th Annual Symposium on Foundations of Computer Science (FOCS), 2024, pp. 573–593

    work page 2024

  7. [7]

    Jan Kraj´ ıˇ cek,Proof complexity, Cambridge University Press, New York, NY, 2019

    work page 2019

  8. [8]

    Jan Kraj´ ıˇ cek and Pavel Pudl´ ak,Propositional proof systems, the consistency of first order theories and the complexity of computations, J. Symb. Log.54(1989), 1063–79

    work page 1989

  9. [9]

    Ming Li and Paul M. B. Vit´ anyi,An introduction to Kolmogorov complexity and its applications, Texts in Computer Science, Springer, 2008

    work page 2008

  10. [10]

    120, Elsevier, 1986, pp

    Pavel Pudl´ ak,On the length of proofs of finitistic consistency statements in first order theories, Studies in Logic and the Foundations of Mathematics, vol. 120, Elsevier, 1986, pp. 165–196

    work page 1986

  11. [11]

    ,Logical foundations of mathematics and computational complexity: A gentle introduction, Springer, 2013

    work page 2013

  12. [12]

    ,Incompleteness in the finite domain, Bull. Symb. Log.23(2017), no. 4, 405–441

    work page 2017

  13. [13]

    3, 877–884

    Tibor Rado,On non-computable functions, The Bell System Technical Journal41(1962), no. 3, 877–884

    work page 1962

  14. [14]

    Albert Visser,The interpretation existence lemma, Feferman on Foundations: Logic, Mathematics, Philosophy (Gerhard J¨ ager and Wilfried Sieg, eds.), Springer International Publishing, Cham, 2017, pp. 101–144. 21

    work page 2017