Re: How to use `deep inference'?

On Monday 26 April 2004 16:29, Alessio Guglielmi wrote:
> 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.

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.

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. 
(not to speak of all those fragments of linear logic that we did never 
consider, but that other people find interesting: IMELL, polarised MELL, ALL, 
etc.)

> 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 model theory it is boolean algebra, I think in proof theory it is 
*-autonomous category (By the way, this is also true for classical logic!). I 
agree with all the rest.

-Lutz