Clarification on rule schemes

Hello,

I was asked to clarify what Lutz and I were talking about. I'll 
attempt to do so very briefly.

The problem is to design deductive systems, i.e., given a logic, to 
design inference rules for that logic with some proof theoretical 
properties, like cut elimination, some form of the subformula 
property, locality, etc. This is of course more an art than an 
exercise in engineering, but a few principles of good design still 
help a lot.

In the sequent calculus, the most important principle is of course 
`to define connectives in isolation', meaning that you ask yourself 
how can you introduce the main connective of a formula, and then you 
try to come up with appropriate premises from which to conclude the 
desired conclusion. This works well for classical and intuitionistic 
logic, but not so well for linear and modal logics, and it doesn't 
work at all for some other logics like pomset logic. In linear logic, 
for example, the promotion rule does not obey this principle, because 
you define the `!' but you need to check for `?'s, so the `!' is not 
in isolation.

Even better than having principles, and this is what Lutz and I are 
discussing, is to have schemes that *generate* good inference rules. 
If we find a scheme that generates most (or all) inference rules of 
important logics, then we have a very good starting point for 
generating rules for other logics.

It turns out that in the calculus of structures we have found such a 
scheme, which progressively became more and more comprehensive. In 
the beginning we had what we call the `recipe', a scheme that 
generates the so-called `core' rules. These are rules which 
approximately correspond to the multiplicative fragment of a logic. 
For example, multiplicative linear logic is all made by core rules 
(just one) plus identity and cut. By using the recipe, we can easily 
design, for example, a system for non-commutative logic that can not 
be done in the sequent calculus (called BV, which we conjecture is 
equivalent to pomset logic).

This is already an important achievement, because, just to make an 
example, people spent years trying to get a deductive system for 
pomset logic, and now we can generate a very good candidate in just a 
few seconds.

The same recipe produces a wonderful rule for promotion (which Lutz 
found before the recipe, in fact the recipe was found a posteriori), 
which has none of the problems of the corresponding rule in the 
sequent calculus. The recipe also produces excellent rules for many 
modal logics, and we all know that getting good deductive systems for 
modal logics is very tricky.

A natural ambition is then to extend the recipe to take into account 
more than just the core, which means contraction and weakening (if we 
insist in thinking in sequent calculus terms), and also identity and 
cut. Of course, one can say that we have a pretty clear idea of how 
we want to design all these rules (and especially identity and cut). 
On the other hand, things can get quite messy easily, for example in 
linear logic `contraction' has different manifestations: one 
contracts on ?-modalised formulae, but also the additive context can 
be thought of as subject to contraction.

In this respect, Lutz made a really impressive achievement by 
expressing all of linear logic in an extremely regular way: all rules 
different than identity and cut, (with a very slight exception) 
clearly are generated by a very simple scheme.

Again a posteriori, I found a super-scheme which generates all these 
rules, plus identity and cut. It is (admittedly) a weird object, 
because it entails the idea that atoms are not primitive, but they 
are binary logical relations as any other, operating on units. This 
is what I call `subatomic thing'. I still don't know whether it's a 
logic, I think it is, and if it is, then all other logics are just 
*observations* made on this object, and their proof theoretical 
properties would follow from a unified theory we can make on the 
subatomic thing.

This is a very ambitious project I'm working on, and at this stage I 
cannot claim it works. But, for sure, I can claim that it works just 
as a *scheme* for generating rules: one just prints my note, 
available on the web at 
<http://www.ki.inf.tu-dresden.de/%7eguglielm/res/notes/AG8.pdf>, and 
mechanically produces inference rules. This scheme encompasses all of 
classical and all of linear logic, at the exception of a single rule 
(which I take as further evidence that something is wrong with linear 
logic).

There is nothing comparable anywhere else in proof theory: I mean, we 
are in a very, very tidy and regular situation in CoS regarding the 
principled design of deductive systems. I might not be a good samurai 
but I'll manage to chop off some piece to whomever disagrees with me.

-Alessio