Re: How to use `deep inference'?

Lutz,

I agree with all the rest, but I think I disagree when you say that 
we still have to understand the `clever way' in which CoS rules are 
formed. I don't think there's still much to be understood (and anyway 
it wouldn't necessarily be our job to do so), because all what will 
come next will be non-core, meaning: proper axioms of mathematical 
theories, induction, etc.

In other words, the non-core will mostly remain wild, because it 
depends on nature more than on the language we use for speaking of 
nature, which is instead very civilised. We are just providing a 
syntactic formalism: this, by itself, cannot take into account and 
make possible to `understand' the infinite variety of possible 
inference rules. There's no way we can find a unified treatment for 
all the axioms used in the various mathematical theories.

I think the right perspective of what we are doing is as follows. 
There is a common source of tens of logics used today, which 
basically is boolean algebra. (By the way, this is also true for 
linear logic.) It happened that the deductive systems designed for it 
depended excessively on the syntax adopted for representing formulas, 
which is made of trees.

In principle, there should be no relation between `working with a 
boolean algebra' and `making inductions on trees', but in practice 
one such connection was found, because of convenience, historical 
accidents, etc. So we have natural deduction and the sequent 
calculus. Now we got more sophisticated and we see that these 
formalisms have severe shortcomings, and what we are doing (in my 
opinion, ca va sans dire) is nothing else than using a much better 
syntax in order to do justice to the boolean logical core we are 
dealing with.

The regularities we are observing are, in my opinion, generated by 
the common origin of all the logics. The unique rule of subatomic 
proof theory will never be able to take care of induction, for 
example, just of the purely logical component of the various logics.

All that said, I do think that `deep inference' is a very good short 
description of what we are doing. It's true that other formalisms 
(different than CoS, `A' and `B') have some flavour of deep 
inference, but they only have just a bit, because ultimately they 
still work by cutting branches out of trees. Some of them, like the 
display calculus, first cut branches and then glue them back in, but 
still...

-Alessio