Re: How to use `deep inference'?

At 17:02 +0200 26.4.04, Lutz Strassburger wrote:
>Maybe I did not make myself clear enough. With "non-core" I did not mean
>proper axioms of mathematical theories, induction, etc., although it
>certainly belongs to the non-core, once it is added to the system.

Ah, OK. Anyway, there would be nothing wrong in thinking that a good 
formalism should also provide a methodology for finding the `right' 
syntax of proper mathematical axioms. I just happen not to believe 
much in that, but I might be very wrong.

>What I was refering to is the non-core of the logics we are already
>considering. These are: linear logic and its fragments, intuitionistic logic
>and classical logic (propositional as well as first order)
>
>Right now we somehow understand the non-core of classical propositional and
>multiplicative additive linear logic (and I think this is what you capture
>with subatomic logic). If it comes to the exponentials, the quantifiers, or
>intuitionistic logic, it is getting quite messy.

I agree only to a very, very limited extent, let's say I disagree: 
for example, in the full system of linear logic, including 
exponentials, there is only one rule that escapes unified 
understanding, z_, all the others fit the one-rule-for-all scheme.

In predicate logic, only instantiation, n_, falls outside of the 
scheme, but then, this is the minimum that has to be expected. In 
fact, (terms-in-)predicates have *nothing* to do with the 
propositional behaviour. On the contrary, I find it extremely 
remarkable that instantiation is the *only* rule that falls outside 
of the scheme!

About intuitionistic logic: there is there a rather strong deviation 
from the boolean algebra source, so again, nothing unexpected. Add to 
this that we didn't really study it much.

It looks like you're downplaying what I consider our (and also your) 
biggest conceptual achievement, i.e., the fact that we took logics 
with a bunch of rules of totally different shapes and we shaped them 
into extremely regular objects.

Actually, speaking of marketing, I'm considering to stress this fact 
much more in the future, at least in front of mathematically inclined 
audiences.

-Alessio