Re: Splitting and cut elimination

> > The induction rule is not substitution-invariant.
>
>
> Can you elaborate? How comes?? I mean, once one is careful with 
> variables...
Your definition talks about atoms and thus treats the two occurrences of 
the propositional variable a in [a,a] as being the same but in [a,-a] as 
different. This makes perfect sense, for otherwise either contraction 
would not be substitution invariant (which it should be) or identity 
would be substitution invariant (which it shouldn't be).

Now, induction, here on an atomic formula, is something like this:

(a0, forall x [-ax,asx])
--------------------------  .
    forall x ax

It's clearly not substitution invariant according to your definition, 
just as cut and identity aren't. This has nothing to do with variables, 
terms or the like but just with the fact that a occurs positively and 
negatively: the exact same problem also occurs in propositional temporal 
logics.

It seems easy to avoid breaking the induction rule: when substituting 
for a, then simply also substitute for -a. However, that's no solution: 
once you break an identity above by substituting for -a then how do you 
fix it?

Well, that's my naive take on why cut elimination in the presence of any 
form of induction is challenging.

Good night everybody.

-Kai