Cut-elimination for a logic with definitions and induction

In order to reason about specifications of computations that are given via the proof search or logic programming paradigm one needs to have at least some forms of induction and some principle for reasoning about the ways in which terms are built and the ways in which computations can progress. The literature contains many approaches to formally adding these reasoning principles with logic specifications. We choose an approach based on the sequent calculus and design an intuitionistic logic FOλ^Δℕ that includes natural number induction and a notion of definition. We have detailed elsewhere that this logic has a number of applications. In this paper we prove the cut-elimination theorem for FOλ^Δℕ, adapting a technique due to Tait and Martin-Löf. This cut-elimination proof is technically interesting and significantly extends previous results of this kind.