{"id":"cdc2f5ae-e421-454f-b377-e0860f0f25bb","arxiv_id":"2506.05837","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Proof schemata simulate primitive recursive arithmetic only when the induction variable is not strongly quantified, so the abstract's unqualified claim is not supported by the paper's own results.","lead":"This paper studies whether proof schemata, finite descriptions of infinite proof families, can represent every proof in primitive recursive arithmetic. A full simulation would help automate the analysis of inductive proofs, but the paper only delivers a restricted version.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 1 applies PRA's induction rule to the quantified formula F(Sγ); as PRA in Section 2 restricts ind to quantifier-free formulas, the schema-to-PRA direction is unproved for quantified end-sequents.","rationale":"The paper's positive contributions are real: the quantifier-free simulation from [8] is carried over, and Example 5 shows a meaningful class of proofs with strongly quantified induction variables that can still be translated by instantiating proof-schema parameters with the cut terms. However, the central new claim that proof schemata and PRA proofs with quantifiers correspond relies on Lemma 1. The gap is not a matter of disagreement with external consensus; it is an internal mismatch between the induction rule as defined in Section 2 and the induction formula used in the proof of Lemma 1. The reader's weakest assumption identifies exactly this issue. Because the paper already qualifies the main result in the Conclusion, the appropriate disposition is a conditional acceptance pending a repair of Lemma 1 or an explicit restriction of the theorem to quantifier-free end-sequents. I therefore recommend keeping the reader's CONDITIONAL verdict.","tokens_in":14743,"tokens_out":5627,"duration_ms":54036,"concrete_test":"Formalize the PRA calculus of Section 2 in a proof assistant (with ind restricted to quantifier-free F) and run Lemma 1's construction on the proof schema of Example 3. When the construction reaches the final ind inference on F(S(δ')){m←y} ⊢ F(S(δ')){m←y+1}, check whether the induction formula F(S(δ')) is quantifier-free. It contains the subformula ∀x(P(x)→P(s(x))) and the quantified succedent ∀x((P( f (x,n))→P(g(x,n)))→(P(x)→P(g(x,n)))), so the rule application is rejected. This demonstrates that the lemma's proof does not go through for quantified end-sequents; a repair would require either generalizing the PRA induction rule or explicitly restricting Lemma 1 to quantifier-free end-sequents.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 1 is the schema-to-PRA half of the claimed equivalence, and its final step uses the induction rule on F(Sγ), the disjunctive formula equivalent to the schematic end-sequent Sγ. Section 2 defines the PRA induction rule with the explicit side condition that F is quantifier-free. For any end-sequent containing quantifiers, such as Example 3, the formula F(Sγ) is not quantifier-free. The text of Lemma 1 eliminates strong quantifiers only in branches that lead to self-referencing proof calls, not in the end-sequent itself. The Conclusion's restriction that the inductive parameter is not quantified does not remove the outer quantifiers in Sγ, so it does not repair the gap. Hence the construction does not, as written, produce a PRA proof for the quantified schemata that motivate the paper. The prior quantifier-free result from [8] and the technique in Example 5 for strongly quantified cut formulas remain intact, but the general bidirectional claim is only established for the case where F(Sγ) is quantifier-free.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the expressive power of proof schemata, which are parameterized sequences of LK-proofs defined primitive recursively, and compares them with proofs in primitive recursive arithmetic (PRA). Section 2 presents PRA as LK plus an equational theory and an induction rule restricted to quantifier-free induction formulas. Section 3 defines proof schemata with proof symbols, parameters, and recursive proof calls. Section 4 states Lemma 1 (every proof schema has a corresponding PRA proof) and Lemma 2 (every PRA proof has a corresponding proof schema), and illustrates a case of a strongly quantified induction variable that is subsequently cut (Example 5). The Conclusion restricts the claimed translation to the condition that the inductive parameter is not quantified.","tokens_in":14987,"tokens_out":7994,"duration_ms":78436,"significance":"The paper addresses a natural and relevant question: whether proof schemata and PRA proofs are mutually translatable, which would strengthen the foundations of schematic proof analysis and Herbrand-schema extraction. The concrete worked example (Example 3) and the treatment of a strongly quantified induction variable cut in a later proof (Example 5) are useful illustrations. The authors are also honest in the Conclusion about the restriction that the inductive parameter must not be quantified. However, the main positive result is not established as written: Lemma 1, the schema-to-PRA direction, relies on two unjustified proof steps that concern the core of the claim. The abstract's unqualified statement that proof schemata can simulate PRA is therefore too strong relative to what is proven.","major_comments":[{"comment":"The induction step at the end of the proof of Lemma 1 applies the PRA induction rule to the formula F(Sγ), the disjunctive formula corresponding to the schematic end-sequent Sγ. Section 2 explicitly restricts the PRA induction rule to quantifier-free induction formulas. If Sγ contains quantifiers, as it does in Example 3 (e.g., the end-sequent of the outer schema contains ∀x quantifiers), then F(Sγ) is not quantifier-free and the displayed inference is not an admissible PRA rule. The conclusion's condition that the inductive parameter is not quantified does not repair the gap, because the quantifiers in Sγ range over other variables. Thus Lemma 1 as stated is only supported for cases in which F(Sγ) is quantifier-free, which essentially reduces to the previous result from [8].","section":"Section 4, Lemma 1"},{"comment":"The proof of Lemma 1 also invokes cut-elimination on ρ(δγ,⃗nγ,mγ+1) merely because it is an LK derivation, and then replaces a self-referencing proof call by the sequent F(S(δγ))⊢F(S(δγ)) treated as an axiom. This is not justified: the derivation contains proof calls as initial sequents, which are arbitrary schematic sequents rather than atomic axioms, and standard cut-elimination for LK does not extend to derivations with non-atomic initial sequents. Moreover, F(S(δγ)) may be a compound or quantified formula, so the replacement is not even an instance of the Axiom rule as defined in Figure 1. Consequently the claimed elimination of strong quantifiers in the relevant branches is unsupported.","section":"Section 4, Lemma 1"},{"comment":"The abstract states that proof schemata can simulate primitive recursive arithmetic, while the Conclusion only claims the translation works 'with the condition that the inductive parameter is not quantified.' This discrepancy is not merely a presentation issue: given the flaws in Lemma 1, even the restricted claim is not established for schemata whose end-sequents contain quantifiers. The abstract should be revised to state the actually proved fragment, and the conditions under which Lemma 1 is valid should be made explicit.","section":"Abstract and Conclusion"}],"minor_comments":[{"comment":"The sentence 'Note that also in d cannot be eliminated as i is a variable' appears to contain a typo; it should presumably read 'ind' rather than 'in d'.","section":"Section 1, Example 1"},{"comment":"In the evaluation clauses for function symbols, the expression 'g(⃗t, ¯k, f (⃗t, ¯k)↓))↓' has an unmatched parenthesis; this should be corrected.","section":"Section 2, Definition 2"},{"comment":"The proof of Lemma 2 is presented as a direct reuse of the prior work [8], but [8] was limited to the quantifier-free case, while the present claim concerns quantifiers. The proof sketch given in the paper does not make fully explicit how the transformation T treats quantifier rules occurring above the induction inferences, beyond the acknowledged restriction on strong quantification of induction variables. A more self-contained argument would help.","section":"Section 4, Lemma 2"},{"comment":"The notation D = {(δ1, ρ(δi,⃗n,0), ρ(δi,⃗n,mi+1)) | i∈{0,1,2}} appears to mix the subscript 1 with the ranging index i; this should be fixed for readability.","section":"Section 4, Example 5"}],"recommendation":"major_revision","confidential_remarks":"The paper has a promising direction and the concrete examples are instructive, but the main theorem's proof currently contains a load-bearing gap in Lemma 1 that is not a matter of exposition. If the authors can either repair the proof by a genuinely different argument or restrict the theorem to the fragment that is actually supported (e.g., end-sequents for which F(Sγ) is quantifier-free, plus the Example 5 extension), the paper could become acceptable. Given the workshop-proceedings context, the strictness of the referee report should be weighed against the useful illustration of the method and the honest discussion of limitations in the Conclusion."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear [Colleague],\n\nThe paper makes a genuine extension to the authors' earlier quantifier-free work: it attempts a two-way translation between proof schemata and PRA with quantifiers, and Example 5 shows a clever way to handle strongly quantified induction variables that are later cut, by instantiating the schema parameter with the cut terms. That example is new and likely correct. The framework is clearly presented, and the authors are honest about the restriction in the conclusion (inductive parameter not quantified).\n\nThe soft spot is in Lemma 1, the schema-to-PRA direction. The construction builds a PRA proof of F(Sγ) by applying the ind rule to F(Sγ) as the induction formula. But Section 2 defines PRA's induction rule with quantifier-free induction formulas, and F(Sγ) for any end-sequent with quantifiers (e.g., Example 3) is not quantifier-free. The text eliminates strong quantifiers only in branches leading to self-referencing proof calls, not in the end-sequent itself. The conclusion's restriction that the inductive parameter is not quantified doesn't fix this—the outer quantifiers in Sγ remain. So the general bidirectional claim is only proved for the case where F(Sγ) is quantifier-free, which is essentially the old result plus some bookkeeping.\n\nThe reader's stress-test note is accurate; I don't see a way around it from the text. The restricted claim may well be repairable—perhaps by a more careful induction on a quantifier-free skeleton or by working with Herbrand expansions—but that repair is not in the paper.\n\nOverall: this is a real contribution to an open problem, but as written the main lemma has a load-bearing gap. Worth sending to a serious referee, but I would condition acceptance on fixing the quantifier issue in Lemma 1.\n\nBest,\n[You]","headline":"A genuine extension of the authors' quantifier-free translation, but Lemma 1 applies PRA's induction rule to a quantified formula, leaving the central claim unproved for quantified end-sequents.","tokens_in":15428,"tokens_out":3250,"would_cite":false,"duration_ms":28895,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F03","03F05","03F30"],"pacs":[],"model":"deepseek-v4-flash","headline":"Proof schemata simulate primitive recursive arithmetic, with a restriction on quantified induction parameters.","keywords":["proof schemata","primitive recursive arithmetic","PRA","inductive proofs","Herbrand schema","schematic cut-elimination","quantifier-free induction","proof analysis"],"falsifier":"Apply Lemma 1 to the proof schema of Example 3. The construction ends with an ind inference on $F(S_\\gamma)$, the disjunctive formula of the quantified end-sequent, which contains universal quantifiers; because PRA's induction rule requires $F$ to be quantifier-free, the displayed transition from $\\xi^B_\\gamma$ and $\\xi^S_\\gamma$ to $\\xi_\\gamma$ is not a PRA derivation under the paper's own definition. The claim would be settled by exhibiting any proof schema with a quantified end-sequent for which the constructed $\\xi_\\gamma$ is a genuine PRA proof, or, conversely, by finding a PRA proof with a strongly quantified induction variable not later cut that Lemma 2 cannot translate.","tokens_in":14576,"feed_emoji":"🧮","tokens_out":9647,"duration_ms":94842,"temperature":0.7,"pith_summary":"Inductive proofs in arithmetic resist classical cut-elimination and Herbrand analysis because cuts cannot be shifted across induction rules. This paper's strategy is to represent such proofs as proof schemata: parameterized, primitive-recursively defined families of induction-free proofs whose finite description can be analyzed instead. The central claim is that proof schemata and primitive recursive arithmetic (PRA) simulate one another: every PRA proof whose induction variables are not strongly quantified translates into a proof schema with the same end-sequent, and every proof schema translates back into a PRA proof. Quantifiers are admitted under the condition that they do not bind the inductive parameter, and the paper shows that even some strongly quantified induction variables can be handled when the quantified formula is later cut. If correct, this makes an expressive fragment of formal number theory accessible to schematic cut-elimination and Herbrand-schema extraction.","feed_headline":"Proof schemata simulate primitive recursive arithmetic","feed_subtitle":"Two-way translation works when the induction parameter is not quantified, enabling Herbrand analysis.","key_machinery":"The load-bearing object is the proof schema: a finite tuple of proof symbols, each with passive parameter tuples and one active parameter, together with a base-case derivation and a step-case derivation. The step case is allowed to contain a labeled leaf referring to its own end-sequent at the predecessor parameter, and this self-reference is what encodes induction without an explicit induction rule. Evaluating a proof schema under a parameter assignment expands the self-reference recursively until the base case is reached, producing an ordinary LK proof with no induction inferences. On the arithmetic side, the corresponding machinery is PRA's induction rule, $\\Gamma \\vdash \\Delta, F(0)$ and $\\Gamma, F(y) \\vdash \\Delta, F(y{+}1)$ imply $\\Gamma \\vdash \\Delta, F(n)$, with $F$ required to be quantifier-free, together with an equational theory of primitive recursive function definitions. The translations connect the two formalisms: induction inferences become schema self-calls, and schema recursion collapses into a single PRA induction, followed by cuts to recover the original end-sequent.","core_discovery":"The paper argues for a two-way correspondence between proof schemata and proofs of primitive recursive arithmetic, subject to the stated restriction. In one direction (Lemma 2), a PRA proof becomes a proof schema by replacing each induction inference with a proof symbol whose base case is the left premise of the induction and whose step case is the right premise, with the step case allowed to call the same symbol at the predecessor parameter. In the other direction (Lemma 1), a proof schema is collapsed into a PRA proof by unfolding recursive calls into PRA derivations and applying a single PRA induction on the end-sequent formula $F(S) = \\bigvee \\neg\\Gamma \\cup \\Delta$. Quantifier rules do not destroy the translation as long as the inductive parameter is not strongly quantified; when a strongly quantified induction formula is used only in a cut, the translation can still succeed by shifting the cut upward and instantiating the schema parameter with the terms supplied by weak quantifier applications. The paper demonstrates this on the running example by taking $n$ as the schema parameter, obtaining the schematic Herbrand instance $\\{x \\leftarrow f(c,n)\\}$, which unfolds to $c, s(c), \\dots, s^{\\alpha-1}(c)$.","pith_inferences":["Editorial inference: the cut-shifting trick used for the strongly quantified induction variable is likely general: any strongly quantified induction formula that is used only as a cut formula can be unfolded into finitely many instantiations, postponing strong quantification until after the schematic analysis.","Editorial inference: the pattern $c, s(c), \\dots, s^{\\alpha-1}(c)$ suggests a shape theorem for proof schemata: Herbrand instances are primitive recursive in the active parameter, which is exactly what allows a finite Herbrand schema to encode an infinite set of instances.","Editorial inference: the quantifier-free restriction on PRA's induction rule is the real boundary of the equivalence; extending the formalism to an induction rule with quantified induction formulas, or proving that such an extension is impossible, would settle how far the correspondence can be pushed."],"forward_implications":["PRA proofs whose induction variables are not strongly quantified can be subjected to the schematic analysis pipeline: cut-elimination and Herbrand-schema extraction are applied to the proof schema rather than to the induction-containing proof itself.","If the outstanding completeness result for the schematic proof-analysis method is obtained, the paper's correspondence yields a realization of Herbrand's theorem for an expressive fragment of formal number theory.","Proofs that strongly quantify an induction variable and then cut the quantified formula can still be represented schematically by instantiating the schema parameter with the terms from the weak quantifier applications and moving the cut upward.","For the running example, the schematic Herbrand instance $\\{x \\leftarrow f(c,n)\\}$ unfolds to $c, s(c), \\dots, s^{\\alpha-1}(c)$, giving a finite description of an infinite sequence of instances.","Quantifying over the induction parameter is in general outside the simulation; the paper's condition is essential unless the quantified formula is later cut."],"supporting_citations":[{"why":"Establishes the earlier quantifier-free simulation between PRA proofs and proof schemata that this paper extends to proofs with quantifiers.","marker":"[8]"},{"why":"Supplies the definition of primitive recursive arithmetic used here, with the quantifier-free induction rule and the equational theory of primitive recursive function symbols.","marker":"[6]"},{"why":"Defines schematic sequents, proof labels, proof schemata, and the Herbrand-schema extraction that motivates the simulation.","marker":"[10]"},{"why":"Provides the schematic first-order language and the schematic refutation calculus used in analyzing characteristic formula schemata.","marker":"[3]"},{"why":"Earlier work showing proof schemata equivalent to a fragment of arithmetic called k-simple induction and introducing the schematic CERES method.","marker":"[9]"},{"why":"Gives the quantifier-free definition of primitive recursive arithmetic used in the prior translation result.","marker":"[12]"}],"fun_headline_variants":["Schemata simulate primitive recursive arithmetic","Proof schemata simulate PRA","PRA simulated by proof schemata","Arithmetic proofs simulated via schemata"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof of Lemma 1 applies PRA's induction rule to the formula $F(S_\\gamma)$ formed from the disjunction of the negated antecedent and the succedent of the schematic end-sequent, even though that formula may contain quantifiers; PRA's induction rule is defined only for quantifier-free formulas, so for end-sequents such as Example 3 the induction step is not an admissible PRA inference.","fun_headline_variants_meta":{"raw":{"variants":["Schemata simulate primitive recursive arithmetic","Proof schemata simulate PRA","PRA simulated by proof schemata","Arithmetic proofs simulated via schemata"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001215,"raw_usage":{"total_tokens":4963,"prompt_tokens":873,"completion_tokens":4090,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":489,"completion_tokens_details":{"reasoning_tokens":4037}},"tokens_in":489,"tokens_out":4090,"duration_ms":35586,"temperature":1.0,"reasoning_tokens":4037,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T10:12:42.046824+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Apply Lemma 1 to the proof schema of Example 3. The construction ends with an ind inference on $F(S_\\gamma)$, the disjunctive formula of the quantified end-sequent, which contains universal quantifiers; because PRA's induction rule requires $F$ to be quantifier-free, the displayed transition from $\\xi^B_\\gamma$ and $\\xi^S_\\gamma$ to $\\xi_\\gamma$ is not a PRA derivation under the paper's own definition. The claim would be settled by exhibiting any proof schema with a quantified end-sequent for which the constructed $\\xi_\\gamma$ is a genuine PRA proof, or, conversely, by finding a PRA proof with a strongly quantified induction variable not later cut that Lemma 2 cannot translate.","supporting_citations":[{"cited_title":"In: LP AR 2024 Complementary V olume, Kalpa Publications in Computing 18, EasyChair, pp","cited_arxiv_id":null,"evidence_quote":"Establishes the earlier quantifier-free simulation between PRA proofs and proof schemata that this paper extends to proofs with quantifiers."},{"cited_title":"1, Biblopolis","cited_arxiv_id":null,"evidence_quote":"Supplies the definition of primitive recursive arithmetic used here, with the quantifier-free induction rule and the equational theory of primitive recursive function symbols."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines schematic sequents, proof labels, proof schemata, and the Herbrand-schema extraction that motivates the simulation."},{"cited_title":"Cerna, Alexander Leitsch & Anela Lolic (2021): Schematic Refutations of F ormula Schemata","cited_arxiv_id":null,"evidence_quote":"Provides the schematic first-order language and the schematic refutation calculus used in analyzing characteristic formula schemata."},{"cited_title":"Journal of Logic and Computation 27(7), pp","cited_arxiv_id":null,"evidence_quote":"Earlier work showing proof schemata equivalent to a fragment of arithmetic called k-simple induction and introducing the schematic CERES method."},{"cited_title":"North Holland, second edition","cited_arxiv_id":null,"evidence_quote":"Gives the quantifier-free definition of primitive recursive arithmetic used in the prior translation result."}],"review_version":1}