Pith. sign in

REVIEW 5 major objections 4 minor 24 references

A Proposed Characterization of p-Simulation Between Theories

T0 review · 5 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that, provably within a theory, p-simulation between theories coincides with efficient interpretability, so a theory that proves it can p-simulate an extension also proves that extension's Pi_1 theorems.

desk verdict Theorem 3.2 is a genuine strengthening; Theorem 3.3's converse is invalid at the omega-rule step, so the characterization is unsupported but worth a referee. read the letter →

arxiv 2507.13576 v4 pith:R336WXI5 submitted 2025-07-17 cs.CC math.LO

Hunter Monroe This is my paper · ORCID
classification cs.CCmath.LO MSC 03F2068Q15
keywords p-simulationinterpretabilityproofcomplexityboundedarithmeticpropositionalsystemsFeige'sHypothesisone-wayfunctionscircuitlowerbounds
topics P versus NP
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to characterize when one axiomatic theory, viewed as a proof system for tautologies, is polynomially as fast as another. Its central proposal is that provable p-simulation and provable efficient interpretability coincide: S proves that S p-simulates S+phi exactly when S proves that S efficiently interprets S+phi. If correct, a theory that proves it can simulate an extension also proves all Pi_1 theorems of that extension, collapsing two previously separate hierarchies. The paper also shows that plain simulation follows from a weaker consistency-strength assumption, and connects simulation to the hardness of P-uniform tautology families.

What carries the argument

The carrying object is an efficient interpretation, a polynomial-time computable map $i()$ from formulas of $S+\phi$ to formulas of $S$ that commutes with logical connectives and sends theorems to theorems. The proof of Theorem 3.2 rewrites a $k$-line proof into a proof whose every line is itself a theorem, with a quadratic triangular-number blow-up, so applying $i()$ yields an $S$-proof of $i(\forall n\le b\,\psi(n))$. Theorem 3.3 internalizes this argument in $S_2^1$ together with Lindström's Theorem 6.6, which equates interpretability with proving all $\Pi_1$ theorems; the key step is the uniformity inference from '$S$ proves $\forall n\le b\,\psi(n)$ for every standard $b$' to '$S$ proves $\forall b\,\forall n\le b\,\psi(n)$'.

What would settle it

Find a c.e. theory $S$ extending $S_2^1$, a sentence $\phi$, and a $\Pi_1$ formula $\psi(n)$ such that $S$ proves that $S$ p-simulates $S+\phi$, $S$ proves $\forall n\le b\,\psi(n)$ for each standard $b$, but $S$ does not prove $\forall n\,\psi(n)$; then the right-to-left direction of Theorem 3.3 fails.

Watch

Extended reading notes

Core claim

The central claim is Theorem 3.3: for computably enumerable theories extending $S_2^1$, $S$ proves that $S$ efficiently interprets $S+\phi$ if and only if $S$ proves that $S$ p-simulates $S+\phi$. The forward direction formalizes a strengthened version of Jeřábek's simulation theorem (Theorem 3.2), which rewrites any proof so every line is itself a theorem and then applies the interpretation, giving a polynomial-time map from $S+\phi$-proofs to $S$-proofs. The reverse direction argues that p-simulation on bounded $\Pi^b_1$ sentences lets $S$ prove each bounded instance $\forall n\le b\,\psi(n)$, and then, by a uniformity step that is the paper's load-bearing premise, concludes that $S$ proves the unbounded $\forall n\,\psi(n)$, which by Lindström's theorem gives interpretability.

Load-bearing premise

The reverse direction of Theorem 3.3 assumes that if $S$ proves each bounded statement $\forall n\le b\,\psi(n)$ for every standard natural number $b$, then $S$ proves the single unbounded statement $\forall n\,\psi(n)$; $S$ itself provides no such uniformity principle.

Editorial extensions

If this is right

  • If Theorem 3.3 is right, the provable p-simulation hierarchy and the provable efficient-interpretability hierarchy coincide, so one can study proof speed by studying interpretations.
  • Whenever $S$ proves that it efficiently interprets $S+\phi$, $S$ already proves every $\Pi_1$ theorem of $S+\phi$, making the extension proof-theoretically conservative at the $\Pi_1$ level from $S$'s own provable viewpoint.
  • A p-optimal proof system would, by contraposition, sit at the top of these coinciding hierarchies; the paper notes that if some theory $S$ provably p-simulates all theories, such facts are infinitely often unprovable.
  • Theorem 4.3 gives a direct corollary: characterizing when $S$ simulates $S+\phi$ would fully characterize which P-uniform families of tautologies are hard to prove in $S$.
  • The paper's Busy Beaver and Kolmogorov-random-string conjectures are offered as strengthenings of 'no optimal proof system exists' that would imply Feige's Hypothesis, the existence of one-way functions, and exponential circuit lower bounds.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • My inference: the uniformity gap in the reverse direction could be closed by adding a reflection principle to $S$; if $S$ can prove its own uniform $\Pi_1$ reflection, the equivalence between provable p-simulation and provable interpretability would hold more broadly.
  • My inference: if the equivalence holds, then relative proof speed between theories is governed by how much $\Pi_1$ truth a theory can internalize, which suggests that proving non-simulation may be as hard as proving the corresponding independence.
  • My inference: the same template may extend beyond the $\Pi_1/\Pi^b_1$ level, as the paper's relativized Theorem 3.5 already pushes the argument to $\Pi_2$ with a truth predicate, so the method could form a ladder through the polynomial hierarchy.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 4 minor

Summary. This manuscript proposes a characterization of p-simulation between axiomatic theories. It claims that if a c.e. theory S efficiently interprets S+φ, then S p-simulates S+φ (Theorem 3.2); that S proves this interpretability claim iff S proves the corresponding p-simulation claim (Theorem 3.3), with the consequence that in this case S already proves all Π_1 theorems of S+φ; and that an analogous characterization holds for simulation (Theorem 4.2). It also formulates conjectures about busy-beaver and Kolmogorov-random axioms intended to imply Feige's Hypothesis, the existence of one-way functions, and circuit lower bounds, and it includes a footnote retracting an earlier claim that the main theorem resolves the p-optimal proof system problem.

Significance. If the characterization were correct, it would be a substantive contribution connecting interpretability, provable p-simulation, and the Π_1 consequences of extensions, with potential applications to proof complexity and the optimal proof system problem. The paper also honestly acknowledges a limitation in footnote 5 and is careful to label its conjectures. However, the central results are not established: Theorem 3.2 does not produce a p-simulation with respect to the standard definition, and Theorem 3.3 relies on an invalid external-to-internal universal quantification step. Because these issues are load-bearing, the significance claim is currently unsupported.

major comments (5)
  1. [Section 3, Theorem 3.2] The proof does not establish a p-simulation under the definition in Section 2. The definition requires P(f(w)) = Q(w), so the input and output proofs must be proofs of the same tautology. The interpretation i is a translation between languages, and the proof only produces an S-proof of i(∀n≤b:ψ(n)), which is not shown to be the same sentence as ∀n≤b:ψ(n); the paragraph after the proof concedes that i(∀n≤b:ψ(n)) need not be Π^b_1. The claim that this is "consistent with the definition of p-simulation" is incorrect for the standard Cook–Reckhow definition quoted in Section 2. To make the argument work, either the definition of p-simulation between theories must be changed to allow translated theorems, or the interpretation must be required to fix Π^b_1 sentences; neither is stated.
  2. [Section 3, Theorem 3.3] The right-to-left direction of the proof contains an invalid step in the displayed chain of implications. The step labeled "S proves this for all b" moves from "for every b, S proves ∀n≤b:ψ(n)" to "S proves ∀b:∀n≤b:ψ(n)" and then to "S proves ∀n:ψ(n)". This is an inference from external universal quantification over numerals to an internal universal statement, which is exactly the ω-rule. A consistent theory extending S_2^1 does not admit this inference: PA proves Con(PA)(bar n) for each numeral n but does not prove ∀n Con(PA)(n). The polynomial-time p-simulation function f provides a separate S-proof for each bound b; no operation on those infinitely many proofs produces a single finite S-proof of the unbounded statement, and the fact that f is provable and polynomial-time does not supply such an operation. This gap is precisely the bridge from Π^b_1 to Π_1 that the paper itself identifies as needed. Therefore the right-to-left direction of Theorem 3.3 is not established, and the derived statements in Section 5 (Theorems 5.3 and 5.6) are also unsupported.
  3. [Section 3, Theorem 3.4] The claim that S_2^1 can formalize Lindström's Theorem 6.6 is asserted, not demonstrated. The proof lists dependencies and ends with "and so on", but does not specify the arithmetization of interpretability, the induction principles used, or the axioms of S_2^1 that are needed. Since Theorem 3.3's right-to-left direction uses this formalization to pass from "S proves the Π_1 theorems of S+φ" to "S proves that S interprets S+φ", the formalizability claim is load-bearing and must be proved in detail or replaced by a precise citation to a published formalization. The same concern applies to the modified Lindström theorem used in Theorem 3.5.
  4. [Section 3, Theorem 3.2] Even if the translation issue is set aside, the displayed rewritten sequence "(1), (1)→(2), (2), (1,2)→(3), (3), ..." is not automatically a proof in the Cook–Reckhow sense. A proof is a sequence of formulas each of which is an axiom or follows by an inference rule from earlier formulas; the fact that each displayed formula is a theorem does not make the sequence a proof. The paper must show that the added conditional formulas can be derived in polynomial size in the underlying proof system. As written, the construction produces a list of theorem statements rather than a proof string.
  5. [Section 4, Theorem 4.2] The right-to-left direction of Theorem 4.2 again moves from "S efficiently proves Con_{S+φ}(n)" for each n to "S proves Con_{S+φ}", i.e., from a family of bounded consistency statements to the unbounded consistency statement. This is the same external-to-internal universal quantification gap as in Theorem 3.3. If the hypothesis means only that for every standard n there is a short S-proof of the bounded statement, no finite proof of the unbounded statement follows; if it already means that S proves the unbounded universal statement, then the conclusion is assumed rather than proved. Thus the right-to-left direction of Theorem 4.2 is not supported.
minor comments (4)
  1. [References] Reference [19] lists the author as "Miciancio"; the correct spelling is "Micciancio". Reference [4] contains the typo "Relativizatons".
  2. [Section 3, Theorem 3.3] The quotation marks around formulas in the proof are not a substitute for a precise arithmetization; please define the formal predicates for proof, p-simulation, and efficient interpretability, and state in which theory the equivalence is proved.
  3. [Section 3, Theorem 3.2] The paragraph after the proof, which says that "i(∀n≤b:ψ(n)) is the encoding of tautologies in S rather than ∀n≤b:ψ(n)", is unclear and appears to change the theorem being proved; this should be clarified or removed, especially in light of the issue raised in the corresponding major comment.
  4. [Section 5] The statements of Theorems 5.3 and 5.6 should explicitly note that they depend on Theorem 3.3 and hence inherit its unproved status.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity; main results depend on external theorems, with only peripheral self-citations.

full rationale

The paper's central derivation chain is not circular. Theorem 3.3's left-to-right direction formalizes Theorem 3.2, whose argument is an explicit proof-rewriting construction, and the right-to-left direction invokes Lindstrom's Theorem 6.6 as an external interpretability criterion; neither step is justified by the author's own prior work. The self-citations to Monroe [20] appear only in Sections 5.1-5.3, supporting side conjectures, e.g., the implication from Conjecture 5.4 to Conjecture 5.7 cites Monroe [20] Theorem 1.1(iii), and the main p-simulation theorem does not depend on them. The one substantive concern in the proof is not circularity: in the five-arrow chain of Theorem 3.3, the step labeled 'S proves this for all b' moves from external universal quantification over numerals to an internal theorem, an omega-rule/reflection step that S does not supply; this is a soundness gap, not a definitional reduction of the conclusion to the assumption. The paper itself flags in footnote 5 that the earlier claimed resolution of the optimal-proof-system problem is withdrawn. No fitted parameters, renamed data, or author-imported uniqueness results appear. Hence no circularity steps are exhibited.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No new mathematical objects are postulated. The paper introduces theories S(k) and conjectures, but these are syntactic constructions and unproven statements, not entities with independent evidential weight.

assumptions (4)
  • domain assumption S is a c.e. theory extending S1_2, and efficient interpretation means a polynomial-time computable, length-bounded map preserving logical connectives.
    Sets the framework for all results; the definitions in Section 2 determine what Theorem 3.3 claims.
  • standard math Lindstrom's Theorem 6.6: S interprets S+phi iff S proves all Pi_1 theorems of S+phi, and this theorem is formalizable in S1_2.
    Used in the right-to-left proof of Theorem 3.3; Theorem 3.4 asserts formalizability but supplies no proof.
  • ad hoc to paper From 'for every standard b, S proves the bounded formula' one can conclude 'S proves the unbounded universal formula'.
    This inference is used in the proof of Theorem 3.3 and is not generally valid; it needs a reflection or uniformity principle not stated.
  • standard math Aaronson's busy beaver result that S(k) proves Con(S') for sufficiently large k, where S(k)=S+phi_BB(k).
    Used in Theorem 5.2 to show S does not simulate S(k) under no optimal proof system; the result is cited, not proved here.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Proposed Characterization of p-Simulation Between Theories." pith.science (2026). https://pith.science/paper/R336WXI5

@misc{pith2026250713576,
  author       = {Pith},
  title        = {Pith review of: A Proposed Characterization of p-Simulation Between Theories},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/R336WXI5}},
  note         = {Machine review of arXiv:2507.13576}
}
abstract

This paper proposes a characterization of when one axiomatic theory, as a proof system for tautologies, $p$-simulates another, by showing: (i)~if c.e. theory $\mathcal{S}$ efficiently interprets $\mathcal{S}{+}\phi$, then $\mathcal{S}$ $p$-simulates $\mathcal{S}{+}\phi$ (Je\v{r}\'abek in Pudl\'ak17 proved simulation), since the interpretation maps an $\mathcal{S}{+}\phi$-proof whose lines are all theorems into an $\mathcal{S}$-proof; (ii)~$\mathcal{S}$ proves ``$\mathcal{S}$ efficiently interprets $\mathcal{S}{+}\phi$'' iff $\mathcal{S}$ proves ``$\mathcal{S}$ $p$-simulates $\mathcal{S}{+}\phi$'' (if so, $\mathcal{S}$ already proves the $\Pi_1$ theorems of $\mathcal{S}{+}\phi$). To explore whether this framework conceivably resolves other open questions, the paper formulates conjectures stronger than ``no optimal proof system exists'' that imply Feige's Hypothesis, the existence of one-way functions, and circuit lower bounds.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 23 canonical work pages

  1. [1]

    3, 32–54

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

    work page 2020

  2. [2]

    Razborov, and Avi Wigderson, Pseu- dorandom generators in propositional proof complexity , SIAM Journal on Computing 34 (2004), no

    Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson, Pseu- dorandom generators in propositional proof complexity , SIAM Journal on Computing 34 (2004), no. 1, 67–88

    work page 2004

  3. [3]

    Sanjeev Arora and Boaz Barak, Computational complexity: A modern approach , Cam- bridge University Press, 2006

    work page 2006

  4. [4]

    Baker, John Gill, and Robert Solovay, Relativizatons of the P=?NP question, SIAM J

    Theodore P. Baker, John Gill, and Robert Solovay, Relativizatons of the P=?NP question, SIAM J. Comput. 4 (1975), 431–442

    work page 1975

  5. [5]

    1, 37–61

    Huck Bennett, The complexity of the shortest vector problem , SIGACT News 54 (2023), no. 1, 37–61

    work page 2023

  6. [6]

    Buss, Bounded arithmetic, Lecture notes, Bibliopolis, 1986

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

    work page 1986

  7. [7]

    Calude and Helmut J¨ urgensen, Is complexity a source of incompleteness? , Advances in Applied Mathematics 35 (2005), no

    Cristian S. Calude and Helmut J¨ urgensen, Is complexity a source of incompleteness? , Advances in Applied Mathematics 35 (2005), no. 1, 1–15

    work page 2005

  8. [8]

    Lijie Chen, Ron D. Rothblum, Roei Tell, and Eylon Yogev, On exponential-time hy- potheses, derandomization, and circuit lower bounds: Extended abstract , 61st IEEE An- nual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020 (Sandy Irani, ed.), IEEE, 2020, pp. 13–23

    work page 2020

Show all 24 references
  1. [9]

    Barry Cooper, Anuj Dawar, and Benedikt L¨ owe, eds.), Springer Berlin Heidelberg, 2012, pp

    Yijia Chen, J¨ org Flum, and Moritz M¨ uller,Hard instances of algorithms and proof sys- tems, How the World Computes (Berlin, Heidelberg) (S. Barry Cooper, Anuj Dawar, and Benedikt L¨ owe, eds.), Springer Berlin Heidelberg, 2012, pp. 118–128

    2012

  2. [10]

    Stephen Cook and Robert Reckhow, The relative efficiency of propositional proof systems, J. Symb. Log. 44 (1979), 36–50

    1979

  3. [11]

    Reif, ed.), ACM, 2002, pp

    Uriel Feige, Relations between average case complexity and approximation complexity , Proceedings on 34th Annual ACM Symposium on Theory of Computing (John H. Reif, ed.), ACM, 2002, pp. 534–543

    2002

  4. [12]

    Russell Impagliazzo and Avi Wigderson, P=BPP if E requires exponential circuits: De- randomizing the XOR lemma , STOC, ACM, 1997, pp. 220–229. 11The truth predicate of Pudl´ ak[22] may be an example. 11

    1997

  5. [13]

    Richard Karp and Richard Lipton, Turing machines that take advice , Enseign. Math. 28 (1982), 191–209

    1982

  6. [14]

    Jan Kraj ´ ıcek,On the existence of strong proof complexity generators , Electronic Collo- quium on Computational Complexity TR22-120 (2022)

    2022

  7. [15]

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

    2019

  8. [16]

    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

    1989

  9. [17]

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

    2008

  10. [18]

    Per Lindstr¨ om,Aspects of incompleteness, Cambridge University Press, 2017

    2017

  11. [19]

    6, 2008–2035, Preliminary version in FOCS 1998

    Daniele Micciancio, The shortest vector problem is NP-hard to approximate to within some constant , SIAM Journal on Computing 30 (2001), no. 6, 2008–2035, Preliminary version in FOCS 1998

    2001

  12. [20]

    Collo- quium Comput

    Hunter Monroe, Ruling out short proofs of unprovable sentences is hard , Electron. Collo- quium Comput. Complex. TR23-047 (2023)

    2023

  13. [21]

    com/watch?v=-9hwU1HtfHM&t=1135s

    Toni Pitassi, Proof complexity and meta-complexity tutorial(2) , https://www.youtube. com/watch?v=-9hwU1HtfHM&t=1135s

  14. [22]

    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

    1986

  15. [23]

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

    2017

  16. [24]

    Razborov and Steven Rudich, Natural proofs, STOC ’94: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing,, (New York, NY: ACM Press), 1994, pp

    Alexander A. Razborov and Steven Rudich, Natural proofs, STOC ’94: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing,, (New York, NY: ACM Press), 1994, pp. 204–13. 12

    1994

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.