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 s ome forms of induction and some principle for reasoning about the ways in w hich terms are built and the ways in which computations can progress. The l iterature contains many approaches to formally adding these reasoning princ iples with logic specifications. We choose an approach based on the sequent calculus and design an intuitionistic logic FO lambda(Delta N) that includ es natural number induction and a notion of definition. We have detailed el sewhere that this logic has a number of applications. In this paper we prov e the cut-elimination theorem for FO lambda(Delta N), adapting a technique due to Tait and Martin-Laf. This cut-elimination proof is technically inter esting and significantly extends previous results of this kind. (C) 2000 El sevier Science B.V. All rights reserved.