Integrating a Global Induction Mechanism into a Sequent Calculus

摘要

Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi contain a separate rule or axiom which reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e. every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a generalization of LK-proofs able to simulate induction by linking proofs, indexed by a natural number, together. Using a global cut-elimination method a normal form can be reached which allows a schema of Herbrand Sequents to be produced, an essential step for proof analysis in the presence of induction. However, proof schema have only been studied in a limited context and are currently defined for a very particular proof structure based on a slight extension of the LK-calculus. The result is an opaque and complex formalization. In this paper, we introduce a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism.