Speaker
Stella Mahler
TU Vienna
Talks at this conference:
Tuesday, 16:30, J431 
Herbrand's theorem for inductive proofs 
Authors: Alexander Leitsch and Stella Mahler Herbrand’s theorem, an important characteristic of formal proofs, bridges propositional and firstorder logic by stating that any valid firstorder 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 firstorder statement, typically obtained through cutelimination. 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 cutelimination 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 cutelimination method CERES (schematic CERES) to firstorder proof schemata [1]. These schemata are parameterized sequences of firstorder 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
