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}

Raj