# Integrating a Global Induction Mechanism into a Sequent Calculus

## TL;DR

This paper introduces a new sequent calculus that integrates a global induction mechanism, enabling cut-elimination with the subformula property for proofs involving induction, which was not possible with previous calculi.

## Contribution

The paper presents the first calculus for proof schemata that supports induction, soundness, and completeness, extending proof theoretic capabilities for inductive proofs.

## Key findings

- Established a calculus for proof schemata with induction
- Proved soundness and completeness for a fragment of Peano arithmetic
- Enabled cut-elimination with the subformula property in inductive proofs

## Abstract

Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi for induction contain a separate rule or axiom which reduces the valid proof theoretic properties of the calculus. To the best of our knowledge, there are no such calculi which allow cut-elimination to a normal form with the subformula property, i.e. every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a variant of LK-proofs able to simulate induction by linking proofs together. There exists a schematic normal form which has comparable proof theoretic behaviour to normal forms with the subformula property. However, a calculus for the construction of proof schemata does not exist. In this paper, we introduce a calculus for proof schemata and prove soundness and completeness with respect to a fragment of the inductive arguments formalizable in Peano arithmetic.