<p>You could have a look at McDowell and Miller's <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs00.pdf">Cut-Elimination for a Logic with Definitions and Induction</a>, which shows how to adopt Tait's method to a first-order intuitionistic sequent calculus with an inductively-defined natural numbers predicate.</p>

CC BY-SA 2.5
2010-12-23T15:04:05.727Z
Thanks -- I read this paper a while back, but forgot about it. I'll take another look.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-23T12:00:01.833Z
2010-12-23T12:00:01.833Z
Noam Zeilberger
<p>How about Ulrich Berger's work? For example <a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=64&amp;layout=abstract">Strong normalization for applied lambda calculi</a>. 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.</p>

CC BY-SA 2.5
2010-12-23T15:03:09.517Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-22T18:30:02.447Z
2010-12-22T18:30:02.447Z
Andrej Bauer
<p>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&#39;$. I am not very interested in quantifiers over natural numbers or predicates indexed by natural numbers. </p>

<p>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. </p>

<p>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. </p>

<lo.logic><pl.programming-languages><sequent-calculus>
Cut-elimination for calculus with nats or other inductive datatype?
Neel Krishnaswami
# Cut-elimination for calculus with nats or other inductive datatype?

(Asked by: username_0 on 2010-12-22)

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.

**Tags:** lo.logic, pl.programming-languages, sequent-calculus

---

## 2 answers

### Answer by username_2 on 2010-12-22. Score: 10 | Accepted answer

How about Ulrich Berger's work? For example [Strong normalization for applied lambda calculi](http://www.lmcs-online.org/ojs/viewarticle.php?id=64&layout=abstract). 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.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_1 on 2010-12-23. Score: 10

You could have a look at McDowell and Miller's [Cut-Elimination for a Logic with Definitions and Induction](http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs00.pdf), which shows how to adopt Tait's method to a first-order intuitionistic sequent calculus with an inductively-defined natural numbers predicate.

> **Comments:**
> **username_0**: Thanks -- I read this paper a while back, but forgot about it. I'll take another look.  

---

