Herbrand's theorem and term induction (Q2491080)

The authors consider a cut-free proof system TIND, an extension of Gentzen's LK by the following purely logical inference rule of term-induction \[ \frac{A(c),\Gamma\vdash\Delta,A(S(c))}{A(0),\Gamma\vdash\Delta,A(S^n(c))} \] where \(A\) is quantifier-free and \(c\) an eigenvariable. This (tind-)rule, formalizing a restricted induction principle and deriving numerals instead of arbitrary terms, can be considered a logical image of full induction. The context of system TIND makes it possible to study a reversion of Herbrand's theorem. In fact, a generalized Herbrand's theorem for TIND is proved: if an existential formula \(A\) is provable in TIND, then there exists a Herbrand disjunction \(H\) in matrix form such that (a) the length of the corresponding matrix is uniformly bounded by a primitive recursive function depending on the length of the proof of \(A\) and logical complexity of \(A\), (b) the number of `big' disjunctions is uniformly bounded by a primitive recursive function depending on the maximal iteration of (tind)-rules in the proof of \(A\) and logical complexity of \(A\), and (c) the term-complexity of the reduct of \(H\) is uniformly bounded by a primitive recursive function depending on the length of the proof and the size of the reduct of \(A\). Consequently, Herbrand disjunctions in matrix form are conceived as natural characterization of theorems of TIND.