Herbrand's theorem for inductive proofs
Stella Mahler
Authors: Alexander Leitsch and Stella Mahler
Herbrand’s theorem, an important characteristic of formal proofs, bridges propositional and first-order logic by stating that any valid first-order formula can be expressed as a finite disjunction of propositional formulas. Translated to sequent calculus, it asserts the existence of a propositionally valid sequent (the Herbrand sequent) for each proof of a first-order statement, typically obtained through cut-elimination.
In presence of mathematical induction Herbrand’s theorem fails, as a side effect of handling the implicit infinity. While the infinite is never needed for arguing by mathematical induction, it is implicit in its construction.
Yet, methods exist for cut-elimination in the presence of induction, albeit yielding proofs lacking the subformula property and Herbrand’s theorem cannot be realized.
Despite the absence of Herbrand’s theorem for inductive proofs, we demonstrate the construction of a finite representation (the Herbrand system) of an infinite sequence of sequents representing the Herbrand sequent of a proof. This is achieved through a generalization of the cut-elimination method CERES (schematic CERES) to first-order proof schemata [1]. These schemata are parameterized sequences of first-order proofs constructed using primitive recursive definitions.
Additionally, our presentation will delve into an initial exploration of the characterization of inductive proofs analyzable by schematic CERES, with a particular focus on examining the relationship between our formalism of proof schemata and primitive recursive arithmetic.
Bibliography
- Leitsch, Alexander, Nicolas Peltier, and Daniel Weller,CERES for first-order schemata,Journal of Logic and Computation,vol. 27 (2017), no. 7, pp. 1897–1954.