Re: Splitting and cut elimination

> \begin{speculation}
>  The problems with the induction rules are caused by their
>  second-order nature. That is, locality, substitution invariance etc
>  are all able to handle essentially first-order rules, but not
>  second-order ones. We know for example that display logic cannot
>  handle induction rules. Stephane Demri and I have shown that
>  we can handle some second-order logics like Grz in display logic, but
>  only by fiddling with the introduction rules.
> \end{speculation}

Three points:

1. System F and related systems (with equivalent SN strength: Leivant's dependently
 typed AF2) have cut-elimination for their sequent calculus formulations; is
 there a problem with giving characterisations of these logics in display logic?
 I would guess not.

2. Girard attributes the observation that inductive types can be systematically
 characterised in system F to Martin-Loef.  So capturing system-F-like formalisms
 means capturing induction.

3. Note, however, that induction does not give recursion: the PA induction axiom,
 which can only be given for dependently typed extensions of system F, is not a
 theorem of the calculus of constructions.  Thus it may be worth refining your 
 speculation to say display logic can handle raw induction but not recursion.

Charles