14
$\begingroup$

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.

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Neel Krishnaswami Dec 23 '10 at 15:03
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks -- I read this paper a while back, but forgot about it. I'll take another look. $\endgroup$ – Neel Krishnaswami Dec 23 '10 at 15:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.