Pith. sign in

REVIEW 3 major objections 4 minor 12 references

Towards an Analysis of Proofs in Arithmetic

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Proof schemata simulate primitive recursive arithmetic, with a restriction on quantified induction parameters.

desk verdict 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. read the letter →

arxiv 2506.05837 v1 pith:5TM6E7JC submitted 2025-06-06 cs.LO

Alexander Leitsch , Anela Lolić , Stella Mahler This is my paper
classification cs.LO MSC 03F0303F0503F30
keywords proofschemataprimitiverecursivearithmeticPRAinductiveproofsHerbrandschemaschematiccut-eliminationquantifier-freeinductionanalysis
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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)$.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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

3 major / 4 minor

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.

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 (3)
  1. [Section 4, Lemma 1] 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].
  2. [Section 4, Lemma 1] 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.
  3. [Abstract and Conclusion] 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.
minor comments (4)
  1. [Section 1, Example 1] 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'.
  2. [Section 2, Definition 2] In the evaluation clauses for function symbols, the expression 'g(⃗t, ¯k, f (⃗t, ¯k)↓))↓' has an unmatched parenthesis; this should be corrected.
  3. [Section 4, Lemma 2] 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.
  4. [Section 4, Example 5] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the claimed schema/PRA translations rest on explicit constructions; the reuse of [8] is independent prior work and is not a definitional reduction.

full rationale

The paper's central claims are the two translations in Lemma 1 (proof schema to PRA) and Lemma 2 (PRA to proof schema). Neither reduces to its inputs. Lemma 1 gives an explicit inductive construction of a PRA derivation of the disjunctive formula F(Sγ) from the schema's base and step derivations. Although the proof applies the PRA ind rule to a possibly quantified F(Sγ), which conflicts with Section 2's restriction that induction formulas are quantifier-free and is a genuine correctness gap for quantified end-sequents, this is a soundness problem, not a circularity: it does not assume the desired conclusion. Lemma 2 is presented as 'the proof from [8]', a self-citation with overlapping authors, but the text also sketches the actual transformation replacing induction inferences by proof calls, and [8] is a separate published derivation for the quantifier-free fragment. The current extension to quantifier introduction is explicitly scoped by the stated condition that the inductive parameter is not strongly quantified; this is a limitation, not a hidden equation of output with input. No fitted parameters or predicted quantities are involved. The Conclusion's remark, 'with the condition that the inductive parameter is not quantified', honestly restricts the result rather than smuggling the conclusion into the definitions. Accordingly, no circular step can be quoted with a specific reduction, and the appropriate finding is no circularity.

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

The paper introduces no fitted parameters or invented entities. The formal machinery of proof schemata is inherited from prior work. The central axioms are standard proof-theoretic facts plus the paper-specific structural claim used in Lemma 1.

assumptions (4)
  • standard math Cut-elimination for the sequent calculus LK.
    Used in Lemma 1 to eliminate strong quantifier introductions in branches of ρ1.
  • domain assumption PRA as defined by Girard with quantifier-free induction formulas.
    Defines the target system; the paper's Lemma 1 later relies on induction on a formula that may contain quantifiers.
  • domain assumption Proof schema evaluation by double induction is well-founded.
    Definition 10 assumes the recursive evaluation terminates according to the ordering of proof symbols and parameter values.
  • ad hoc to paper In any proof schema, strong quantifier introductions in branches leading to a self-referencing proof call are always cut and never reach the end-sequent.
    Asserted in Lemma 1's proof without demonstration; the paper calls them violations of 'proof call conditions' if they occur.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards an Analysis of Proofs in Arithmetic." pith.science (2026). https://pith.science/paper/5TM6E7JC

@misc{pith2026250605837,
  author       = {Pith},
  title        = {Pith review of: Towards an Analysis of Proofs in Arithmetic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5TM6E7JC}},
  note         = {Machine review of arXiv:2506.05837}
}
read the original abstract

Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata admit (schematic) cut-elimination and the construction of Herbrand systems. This work focuses on the expressivity of proof schemata. We show that proof schemata can simulate primitive recursive arithmetic. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs.

Figures

Figures reproduced from arXiv: 2506.05837 by the authors.

Figure 1
Figure 1. The rules for LK. In the rule Axiom, A is quantifier free. In the rules ∀r and ∃l the variable y, the eigenvariable, cannot occur free in the lower sequent. In the rules ∀l and ∃r t is an arbitrary term. Note that we use a restricted form of LK as we do not allow the application of ∀r and ∃l on induction variables. 2 Schematic Language and PRA In [10] and [3] schematic first-order languages were defined as a basis f… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

12 extracted references · 9 canonical work pages

  1. [8]

    In: LP AR 2024 Complementary V olume, Kalpa Publications in Computing 18, EasyChair, pp

    Alexander Leitsch, Anela Lolic & Stella Mahler (2024): On Proof Schemata and Primitive Recursive Arith- metic. In: LP AR 2024 Complementary V olume, Kalpa Publications in Computing 18, EasyChair, pp. 117– 130, doi:10.29007/4g2q

    work page doi:10.29007/4g2q 2024

  2. [1]

    Theoretical Computer Science 403(2-3), pp

    Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemen s Richter & Hendrik Spohr (2008): CERES: An analysis of F ¨urstenberg’s proof of the infinity of primes . Theoretical Computer Science 403(2-3), pp. 160– 175, doi:10.1016/j.tcs.2008.02.043

    work page doi:10.1016/j.tcs.2008.02.043 2008

  3. [2]

    Journal of Logic and Computation 21(6), pp

    James Brotherston & Alex Simpson (2011): Sequent calculi for induction and infinite descent . Journal of Logic and Computation 21(6), pp. 1177–1216, doi: 10.1093/logcom/exq052

    doi:10.1093/logcom/exq052 2011

  4. [3]

    Cerna, Alexander Leitsch & Anela Lolic (2021): Schematic Refutations of F ormula Schemata

    David M. Cerna, Alexander Leitsch & Anela Lolic (2021): Schematic Refutations of F ormula Schemata . Journal of Automated Reasoning 65(5), pp. 599–645, doi: 10.1007/s10817-020-09583-8

    work page doi:10.1007/s10817-020-09583-8 2021

  5. [4]

    In: International Tbilisi Symposium on Logic, Language, and Co mputation, Springer, pp

    Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia & Da niel Weller (2013): Cut-elimination and proof schemata. In: International Tbilisi Symposium on Logic, Language, and Co mputation, Springer, pp. 117– 136, doi:10.1007/978-3-662-46906-4_8

    work page doi:10.1007/978-3-662-46906-4_8 2013

  6. [5]

    American Mathematical Monthly 62(5), p

    Hillel F¨ urstenberg (1955): On the Infinitude of the Primes . American Mathematical Monthly 62(5), p. 353, doi:10.2307/2307043

    doi:10.2307/2307043 1955

  7. [6]

    1, Biblopolis

    Jean Yves Girard (Napoli,1987): Proof Theory and Logical Complexity . 1, Biblopolis

    work page 1987

  8. [7]

    In: Proceedings of 25th Conference on Logic for Programming, Artificial Intell igence and Reasoning, LP AR , EPiC Series in Computing 100, EasyChair, pp

    Alexander Leitsch & Anela Lolic (2024): Herbrand’s Theorem in Inductive Proofs . In: Proceedings of 25th Conference on Logic for Programming, Artificial Intell igence and Reasoning, LP AR , EPiC Series in Computing 100, EasyChair, pp. 295–310, doi: 10.29007/dwdf

    work page doi:10.29007/dwdf 2024

Show all 12 references
  1. [9]

    Journal of Logic and Computation 27(7), pp

    Alexander Leitsch, Nicolas Peltier & Daniel Weller (201 7): CERES for first-order schemata . Journal of Logic and Computation 27(7), pp. 1897–1954, doi: 10.1093/logcom/exx003

    1954 doi

  2. [10]

    Anela Lolic (2020): Automated Proof Analysis by CERES . Ph.D. thesis, Technical University of Vienna, doi:10.34726/hss.2020.47184

    2020

  3. [11]

    The- oretical Computer Science 232(1-2), pp

    Raymond McDowell & Dale Miller (2000): Cut-elimination for a logic with definitions and induction . The- oretical Computer Science 232(1-2), pp. 91–119, doi: 10.1016/S0304-3975(99)00171-1

    2000 doi

  4. [12]

    North Holland, second edition

    Gaisi Takeuti (1987): Proof Theory. North Holland, second edition

    1987

Pith tools

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