{"id":"61fc5419-d49b-4bc8-8c90-d1f21f08660e","arxiv_id":"2507.13576","paper_version":4,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper's proposed characterization of p-simulation between theories is not established, because the right-to-left proof uses an invalid logical generalization step.","lead":"This logic paper claims that one theory can p-simulate its own extension exactly when it efficiently interprets that extension, and that this equivalence is provable inside the theory. If true it would connect proof length with interpretability, but the proof has a critical gap in the converse direction.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.3's right-to-left step is invalid: it infers 'S proves ∀b φ(b)' from 'for every b, S proves φ(b)', an ω-rule step that would let S prove its own consistency. The characterization is therefore unsupported.","rationale":"I agree with the reader's weakest assumption. The forward direction of Theorem 3.3 is plausible, but the right-to-left inference is not justified: it quietly replaces a family of proofs indexed by bounds with a single proof of the universal statement. This is exactly the kind of step that would let a theory prove its own consistency from its finite-consistency facts. The concern is internal to the argument, not a matter of conflicting with consensus: the paper's own paragraph before Theorem 3.3 acknowledges the Π^b_1-to-Π_1 gap, and the proof does not bridge it. I also credit the paper for labeling Section 5 items as conjectures and for footnote 5's honest withdrawal of the earlier resolution claim, but those do not support the main characterization. Theorem 3.4's one-paragraph formalizability claim cannot substitute for the missing uniformity step. The reader's REJECT verdict is therefore unchanged.","tokens_in":8965,"tokens_out":13689,"duration_ms":173828,"concrete_test":"Formalize the right-to-left proof of Theorem 3.3 for S=PA and φ=Con_PA, with ψ(n) meaning 'n is not a PA-proof of 0=1'. PA proves every bounded instance ψ(bar n), so if the step from 'PA proves ∀n≤b ψ(n) for all b' to 'PA proves ∀b∀n≤b ψ(n)' were a valid first-order derivation, the formalized theorem would yield a PA proof of Con_PA. Since PA does not prove Con_PA, a successful formalization must fail precisely at that step; run the formalization in a proof assistant to locate which inference rule is used and verify that it is an ω-rule or reflection principle not available in S1_2.","verdict_should_be":"UNCHANGED","load_bearing_attack":"At the displayed five-arrow chain in the proof of Theorem 3.3, the step labeled 'S proves this for all b' moves from '∀b: S proves ∀n≤b ψ(n)' to 'S proves ∀b:∀n≤b ψ(n)' (then drops b). This is an external universal quantification over numerals, not an internal theorem. A consistent theory extending S1_2 does not satisfy the needed uniformity/ω-rule: PA proves Con(PA)(bar n) for each numeral n, but PA does not prove ∀n Con(PA)(n). The assumption that the p-simulation f is provable and polynomial-time does not repair the gap: f yields a separate S-proof for each bound b, and there is no operation that combines all those proofs into one finite proof of the unbounded Π1 statement. The paper itself notes that p-simulation concerns Π^b_1 sentences whereas the converse needs Π_1 sentences; the invalid step is exactly that bridge. Since the right-to-left direction of the iff is the part that would force S to prove all Π1 theorems of S+φ, Theorem 3.3's central characterization is not established. Footnote 5's withdrawal of the earlier resolution claim is consistent with this reading.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":9171,"tokens_out":11399,"duration_ms":119327,"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":[{"comment":"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.","section":"Section 3, Theorem 3.2"},{"comment":"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.","section":"Section 3, Theorem 3.3"},{"comment":"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.","section":"Section 3, Theorem 3.4"},{"comment":"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.","section":"Section 3, Theorem 3.2"},{"comment":"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.","section":"Section 4, Theorem 4.2"}],"minor_comments":[{"comment":"Reference [19] lists the author as \"Miciancio\"; the correct spelling is \"Micciancio\". Reference [4] contains the typo \"Relativizatons\".","section":"References"},{"comment":"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.","section":"Section 3, Theorem 3.3"},{"comment":"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.","section":"Section 3, Theorem 3.2"},{"comment":"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.","section":"Section 5"}],"recommendation":"reject","confidential_remarks":"The manuscript's central theorem is unsupported by an invalid ω-rule step; the author already retracts the strongest claim in footnote 5. In my view, the remaining result cannot be repaired within the current scope because the theorem as stated would imply S proves its own Π_1 consequences, which is too strong. The paper may contain useful survey material and plausible conjectures, but the technical core is not there. I recommend rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing to know: the paper's headline claim, Theorem 3.3, is not established, but there is a real and citable strengthening buried in it. Theorem 3.2 shows that an efficient interpretation of S+phi into S gives a p-simulation, not just a simulation as in Jerabek's earlier work. The proof rewrite argument is direct and, as far as I can tell, correct, though the remark that the image of a Pi^b_1 sentence under the interpretation need not itself be Pi^b_1 is a legitimate caveat that the paper handles honestly.\n\nThe right-to-left direction of Theorem 3.3 fails at the displayed five-arrow chain. The step 'S proves this for all b' moves from external universal quantification - for each standard b, S proves the bounded instance - to an internal universal statement inside S. That is exactly the kind of omega-rule inference that a consistent theory cannot generally perform. The analogy with Con(PA)(n) is exact: PA proves each finite consistency statement but not forall n Con(PA)(n). The assumption that the p-simulation is provable and polynomial-time does not repair the gap, because the simulation produces one S-proof per bound, and no finite proof in S can combine all of them. So the central equivalence, and with it the claim that S already proves the Pi_1 theorems of S+phi, is unsupported. Theorem 3.4 is a one-paragraph assertion with no real formalization details, and the footnote acknowledging that an earlier resolution claim was withdrawn is consistent with the picture.\n\nThe rest of the paper is an exploratory program. The conjectures in Section 5 are labeled as conjectures and are not used to prove anything load-bearing, which I respect. Still, the connection to Feige's Hypothesis and one-way functions is speculative. The paper would be improved by either repairing the right-to-left argument or clearly separating the proven forward direction from the unproven characterization.\n\nWho should read it: people working on proof complexity and interpretability, especially those interested in whether provable p-simulation and provable interpretability can coincide. The paper is honest and the forward direction deserves citation.\n\nRecommendation: send to peer review, but with a clear expectation that the central theorem needs substantial repair. The referee time is justified by the importance of the characterization if it can be made to work.","headline":"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.","tokens_in":9711,"tokens_out":2352,"would_cite":true,"duration_ms":25436,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["p-simulation","interpretability","proof complexity","bounded arithmetic","propositional proof systems","Feige's Hypothesis","one-way functions","circuit lower bounds"],"falsifier":"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.","tokens_in":8685,"feed_emoji":"🧮","tokens_out":6339,"duration_ms":68551,"temperature":0.7,"pith_summary":"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.","feed_headline":"Provable p-simulation equals provable interpretability","feed_subtitle":"If a theory can prove it simulates its own extension, it already proves the extension's universal theorems.","key_machinery":"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)$'.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies Jeřábek's theorem that interpretation implies simulation, which Theorem 3.2 strengthens to p-simulation.","marker":"[23]"},{"why":"Lindström's Theorem 6.6 equates interpretability with proving all Pi_1 theorems, the step Theorem 3.3 tries to formalize.","marker":"[18]"},{"why":"Defines $S_2^1$, the weak arithmetic in which the paper formalizes its metatheorems.","marker":"[6]"},{"why":"Introduces propositional proof systems and p-simulation, the paper's basic objects.","marker":"[10]"},{"why":"Sets out the open problem of p-optimal proof systems and the proof-complexity terminology used throughout.","marker":"[15]"},{"why":"Provides the background impossibility result relating consistency hardness to the absence of optimal proof systems.","marker":"[22]"}],"fun_headline_variants":["Provable p-simulation iff provable interpretability","Theories equate provable simulation and interpretability","Proof of simulation equivalent to proof of interpretability","Proving simulation equals proving interpretability"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Provable p-simulation iff provable interpretability","Theories equate provable simulation and interpretability","Proof of simulation equivalent to proof of interpretability","Proving simulation equals proving interpretability"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000577,"raw_usage":{"total_tokens":2721,"prompt_tokens":944,"completion_tokens":1777,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":560,"completion_tokens_details":{"reasoning_tokens":1719}},"tokens_in":560,"tokens_out":1777,"duration_ms":15469,"temperature":1.0,"reasoning_tokens":1719,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T16:22:32.408068+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies Jeřábek's theorem that interpretation implies simulation, which Theorem 3.2 strengthens to p-simulation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Lindström's Theorem 6.6 equates interpretability with proving all Pi_1 theorems, the step Theorem 3.3 tries to formalize."},{"cited_title":"Buss, Bounded arithmetic, Lecture notes, Bibliopolis, 1986","cited_arxiv_id":null,"evidence_quote":"Defines $S_2^1$, the weak arithmetic in which the paper formalizes its metatheorems."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces propositional proof systems and p-simulation, the paper's basic objects."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Sets out the open problem of p-optimal proof systems and the proof-complexity terminology used throughout."}],"review_version":1}