# Cut-elimination for calculus with nats or other inductive datatype?

Does anyone direct me to a paper detailing a cut-elimination theorem for propositional intuitionistic logic, including an inductive datatype such as the natural numbers (lists or trees would be fine, too)? An example of the kind of system I am interested in is Godel's T, which has types given by the grammar $A ::= \mathbb{N} \;\;|\;\; A \to A'$. I am not very interested in quantifiers over natural numbers or predicates indexed by natural numbers.

I know how to prove beta-normalization for natural deduction version of these systems using a logical relations argument (or related techniques such as NbE), but would like to know if there are standard references on how to adapt these methods to sequent calculi.

The reason I ask is that I am studying adding fixed point operators for guarded recursion to a language. The denotational idea is a rather old one -- interpret types as ultrametric spaces and fixed points via Banach's theorem -- but the purely syntactic techniques I know for proving cut-elimination don't seem to adapt that well.

## 2 Answers

How about Ulrich Berger's work? For example Strong normalization for applied lambda calculi. The "recursively defined constants" part gets you inductive types, more or less. And don't be put off by the word "untyped", he gets results for typed systems too.

• This is a very interesting idea! I am interested in adding (eg) constants for fixed points which are not necessarily left- or right-rules, so this looks like a good place to look. Dec 23, 2010 at 15:03

You could have a look at McDowell and Miller's Cut-Elimination for a Logic with Definitions and Induction, which shows how to adopt Tait's method to a first-order intuitionistic sequent calculus with an inductively-defined natural numbers predicate.

• Thanks -- I read this paper a while back, but forgot about it. I'll take another look. Dec 23, 2010 at 15:04