[FOM] Mismatch

[Alessio Guglielmi]

Hello,

I'd like to receive comments on the following little exposition about 
a structural mismatch between meta and object level in deductive 
systems. I'll use this argument as motivation and introduction for a 
course on my work on deep inference.

In short, the argument goes as follows:
1   There is a mismatch between meta and object levels in many 
calculi, like the sequent calculus and natural deduction.
2   The mismatch has undesirable proof theoretical consequences, the 
most important being the inability to design deductive systems.
3   Since the object level is untouchable (it's the language you want 
to deal with), one can fix the problem by `improving' the meta level;
4   or one can also sort of *merge* object and meta level by using 
deep inference, and this is my favourite approach.

I'm not going to be particularly exhaustive or pedantic (I'll use 
plenty of `quotes'), I just hope that people who see things 
differently tell me so, and the same do people who know about ideas I 
didn't consider here. I'm sure there are many imprecisions and 
mistakes in what follows, please correct me and let me know of your 
work if you think it's relevant.

-Alessio


1   THERE IS A MISMATCH BETWEEN META AND OBJECT LEVEL IN MANY CALCULI

I will here make more precise what I mean by `mismatch'. It's not 
worth the effort to make this notion formal, because it has more of a 
moral value than a technical one. To make my point, looking at the 
sequent calculus suffices, because the reader can immediately make 
the analogue with natural deduction, proof nets, etc.

1.1   Let us first see a case of perfect match in Gentzen's one-sided 
sequent calculus, for propositional classical logic. Consider:

      |- A, Gamma   |- B, Delta       |- A, B, Gamma
    ^ ------------------------- ,   V --------------- ,
       |- A ^ B, Gamma, Delta         |- A V B, Gamma

where A and B are formulae and Gamma and Delta are multisets of 
formulae. In the first inference, the object level ^ in the 
conclusion corresponds to a meta level `and' between the two premises 
(branches of the derivation). In the second inference, the object 
level V corresponds to the meta level `or' expressed by commas in the 
premise sequent.

We can test the correspondence by `flattening down to object' the 
meta level and check whether inferences correspond to implications. 
They do, because

    ((A V Gamma) ^ (B V Delta)) => ((A ^ B) V Gamma V Delta) ,

and trivially so for the V rule.

There is no mismatch, because, when going bottom-up, the connectives 
at the object level (^, V) become corresponding structural relations 
at the meta level (resp. `branching' and `being in a multiset').

1.2   Let us now see a case of mismatch, in Gentzen's one-sided 
sequent calculus for linear logic. Consider:

      |- A, Gamma   |- B, Delta
    * ------------------------- ,
       |- A * B, Gamma, Delta

where * is multiplicative conjunction (`times' or `tensor'). Can we 
consider branching a meta-level *? We could, because

    ((A # Gamma) * (B # Delta)) -o ((A * B) # Gamma # Delta) ,

where # is multiplicative disjunction (`par') and -o is linear implication.

Now let's see additive conjunction & (`with'):

      |- A, Gamma   |- B, Gamma
    & ------------------------- .
           |- A & B, Gamma

We assumed that branching is *, and we find that

    ((A # Gamma) * (B # Gamma)) /-o ((A & B) # Gamma) ,

so we have a mismatch. If we assume that branching is &, instead of *, then

    ((A # Gamma) & (B # Gamma)) -o ((A & B) # Gamma) ,

so the mismatch disappears here, but it reappears in the previous 
case of *, because

    ((A # Gamma) & (B # Delta)) /-o ((A * B) # Gamma # Delta) .

We could go one step further by declaring that branching between 
sequents (or derivations) S and T corresponds to !S * !T, where ! is 
the `of course' modality. In this case, we have

    (!(A # Gamma) * !(B # Delta)) -o ((A * B) # Gamma # Delta)   and
    (!(A # Gamma) * !(B # Gamma)) -o ((A & B) # Gamma) .

But are we happy? No, because we still have a mismatch, since !(.) * 
!(.), i.e., the branching relation, doesn't correspond neither to *, 
nor to &, nor to any other connective in the language.

At this point you see how I could technically define my notion of 
mismatch, in the sequent calculus. Of course, the notion would be 
meaningful also in proof nets, but the definition for them would 
become more delicate (given that branching is rather different), so 
it's not worthy to get into this business for now.

What matters is that, for example, if one asks the question: `What 
does branching correspond to?' then the answer cannot be given simply 
and elegantly in terms of logical operators at the object level. I'm 
going to argue that this difficulty causes trouble in structural 
proof theory.


2   THE MISMATCH HAS UNDESIRABLE PROOF THEORETICAL CONSEQUENCES

My impression is that we can consider the sequent calculus perfect 
for classical logic, since there's no mismatch, but it gets less and 
less adequate the more we depart from classical logic.

2.1   If we move to linear logic, we see disturbing phenomena 
occurring already, even more disturbing than the mismatch observed 
above. Consider for example the promotion rule:

       |- A, ?B1, ..., ?Bh
    p -------------------- ,
      |- !A, ?B1, ..., ?Bh

where ? ('why not') is the dual modality of !. Contrary to legitimate 
expectation, applying the rule requires a global check on the entire 
context of !A, for making sure that all formulae are modalised by ?.

If one is only interested in certain technical aspects of deductive 
systems, like for example cut admissibility, then the sequent 
calculus, in this case, does its job, and we only have to pay a price 
in terms of elegance and conceptual clarity. In this sense, the rule 
above is disturbing, for example, because the `meaning' of ! requires 
a side condition on the context. As we will see later, pure 
aesthetics of this rule can also be improved in a different approach.

The promotion rule is not `difficult' only in the sequent calculus: 
proof nets for ! and ? are also unsatisfying, again for problems that 
one can reconduct to the mismatch.

2.2   What I find the most serious drawback of the mismatch is the 
impossibility, or at least the inability, or at the very least the 
difficulty, of designing deductive systems for many logics that are 
otherwise known:

- Impossibility: we know a logic, called BV, for which Alwen Tiu 
proved that it's impossible to express it in Gentzen's sequent 
calculus [1]. It's the only result I know of this kind. There is no 
room here to give the details, suffices to say that BV is extremely 
simple, and it's not a specially tailored pathological case.

- Inability and difficulty: probably the most common cases of 
inability are found in modal logics. For several modal logics, like 
S5, it is not known (if I'm not wrong) whether a (pure) Gentzen's 
sequent calculus presentation is achievable. For other modal logics 
one such presentation has been painfully found, often after 
significant departures from the pure form of Gentzen's sequents.

Typically, the context structure of sequents is enriched: they are no 
more just sets or multisets, but become order structures of varying, 
and sometimes very high, complexity. All of this is done of course 
for the sake of eliminating the mismatch.

2.3   There is a simple philosophy of Gentzen's sequent calculus, for 
which, grossly speaking, the `meaning' of connectives is defined by 
their rules, where connectives are `brought to the meta level' with 
no reference to the context, according to some harmony-preserving 
principles. Departing from pure sequents has a conceptual cost, which 
is not entirely repaid, in my opinion, by achieving technical results 
like cut elimination.

In fact, there is a value in having simple deductive systems, all 
designed according to the same methodology. Having to tailor the 
shape of sequents to each logic requires an effort, both for the 
proof theorist and for the user of the deductive system, who has to 
learn a new metalanguage for every system.

There is in addition a technological cost. `Exotic' logics are more 
and more used in computer science, in verification, for example. If 
one changes the metalanguage (of sequents, or of natural deduction, 
typically), then the corresponding verification system must be 
updated accordingly. In other words, it is difficult to design a 
universal framework in which all sorts of metalanguages for 
describing deductive systems are easily coded.


3   ONE CAN FIX THE PROBLEM BY `IMPROVING' THE META LEVEL

As I said above, the standard way of dealing with the mismatch is to 
enrich the structure of the meta level. The idea is simple: if 
branching and commas are not enough, let's supply some more structure.

Since doing this ad hoc, case by case, blurs the conceptual picture 
and has costs for the users of deductive systems, a general solution 
is desirable.

As far as I know (and please help me because I feel rather insecure 
here) one strong bid in this direction comes from Belnap's display 
calculus. The idea goes as follows:

3.1   Why does one need a meta level at all? Because, when looking 
for a proof, one has to get inside formulae to access the information 
lying there under several strata of connectives. To do so, one breaks 
formulae into pieces, but has to keep track carefully of the 
relations between pieces, whence the need of structure at the meta 
level.

The display calculus does this: it defines a rich notion of structure 
at the meta level, and makes sure that the various subformulae are 
accessible (`on display'). Then a general cut elimination theorem 
exists which is automatically inherited by all deductive systems 
presented in the display calculus. Since the display calculus is 
mainly studied by philosophers, I'm sure that a careful theory of 
meaning has been elaborated (I'm not knowledgeable enough to be more 
positive).

3.2   I'd be very much interested in listing all advantages and 
disadvantages of the display calculus. My provisory list goes as 
follows:

- Advantages: uniformity, for example many modal logics receive a 
uniform treatment here, as opposed to ad hoc presentations in 
variants of Gentzen's sequent calculus; generality, one cut 
elimination theorem suffices for all systems.

- Disadvantages: complexity, I find the definition of display 
calculus `very big'.

As a last remark, I have to say that I'm not entirely convinced of 
the display calculus approach because it goes in the direction of 
complexity instead of simplicity. There are two ways to reach 
generality: 1) to take into account all possibilities and then study 
them once and for all, 2) to try and find a simple principle 
underlying a vast class of phenomena. My impression is that the 
display calculus does 1, while I believe that in structural proof 
theory something like 2 can be discovered.


4   ONE CAN `BRING THE META LEVEL DOWN TO THE OBJECT ONE' BY USING 
DEEP INFERENCE

If the purpose of the meta level is to make subformulae accessible, 
why don't we just get in and take them, by inferring directly inside 
formulae, at any level of depth? Of course, one reason not to do so 
could be being unable to do proof theory (for example proving cut 
elimination)!

My colleagues and I, in the last few years, have developed a proof 
theory for deep inference (called the Calculus of Structures), so we 
claim to have a radical, good solution for the problem represented by 
the mismatch. This is the content of my course, but, to complete this 
email, I will explain here the main idea with a couple of examples, 
and will make a summary of the advantages I see in my approach.

4.1   All inference rules are of the form

    C{B}
    ---- ,
    C{A}

meaning that subformula A inside formula C{A} is replaced inside 
context C{ } by B, while going up in building a proof. There is no 
branching, no commas, no meta-level structure. The formula itself 
takes care of representing what used to be the meta-level structure. 
Gien this, rule V of classical logic immediately disappears. Let us 
just assume from now on that A and B, as above, do not occur in the 
scope of an odd number of negations (otherwise we could use dual 
rules to the ones we are going to see).

Rule ^ becomes what I call a `switch':

      C{(A V D) ^ (B V E)}
    s -------------------- ,
      C{(A ^ B) V (D V E)}

which is good also for the linear logic case,

      C{(A # D) * (B # E)}
    s -------------------- .
      C{(A * B) # (D # E)}

4.2   This was of course a triviality. The next step is looking at 
cut and cut elimination. Identity and cut look like this:

        C{true}              C{A ^ -A}
    id ---------   and   cut --------- .
       C{A V -A}             C{false}

It is easy to see how they correspond to their counterparts in the 
sequent calculus. What is not easy is proving cut elimination, 
because, in the presence of deep inference, the old methods are 
basically useless. One can find in [2, 3, 4] proofs of cut 
elimination for classical and linear logics. Many other papers are 
available at [5], one of which also deals with a uniform theory for 
modal logics [6].

4.3   Rules like promotion get important advantages from deep 
inference. Here is promotion in the Calculus of Structures:

      C{!(A # B)}
    p ----------- ;
      C{!A # ?B}

since there's more flexibility in managing the context than just 
branching, this promotion rule can check its context incrementally, 
one ?B at a time, this way removing the need for the global test that 
afflicted promotion in the sequent calculus. (Why this is so is not 
obvious, the reader can check [4] or [7] or [8] for details.)

More importantly, one can see that promotion is just a unary case of 
switch. More in general, rules in the Calculus of Structures can be 
derived from a more general, simple scheme, briefly described in [9]. 
(An even more dramatic simplification is speculated in [10].)

4.4   The biggest advantage that deep inference brings into the 
picture is top-down symmetry for derivations. A derivation can be 
flipped upside-down, and negated, and it remains a valid derivation. 
One can see our new symmetry in the identity and cut rules shown 
above. In the sequent calculus, this is impossible because there is a 
top-down asymmetry: while going up, one has less and less of object 
level and more and more of meta level.

The top-down symmetry has important proof theoretic consequences. For 
example, the cut rule can be equivalently replaced by its atomic 
version (the principal formula is an atom). This can be done without 
having to prove full-blown cut elimination, but just by a very simple 
inductive argument dual to the corresponding one for identity. This 
contributes to completely different, and in certain cases very 
simple, arguments for cut elimination (see [2]). In general, the 
entire analysis of proofs benefits from the symmetry, for example 
several interesting notions of normal forms can be studied which are 
provably impossible in the sequent calculus.

4.5   In conclusion, given that the mismatch causes trouble, it seems 
to me that the solution of eliminating the cause of the disease, by 
deep inference, looks better than the alternative of living with it 
by curing the symptoms. There are (at least) two serious objections 
one can make:

1) There is no `theory of meaning' for what we do with deep 
inference. My guess is that this might come one day, given that my 
formalism is very clean and regular, and it possesses interesting 
properties, that should stimulate the interest in studying it from a 
philosophical perspective.

2) There is no general cut elimination theorem, like for display 
logic. Again, I believe that this is a matter of time: I am 
especially confident in the kind of research started in [10] and in 
so-called splitting theorems (see [11] for an example), which appear 
to have the right kind of encompassing regularity needed for this 
task.


REFERENCES

[1] Alwen Fernanto Tiu. Properties of a logical system in the 
calculus of structures. Technical Report WV-01-06, Technische 
Universitaet Dresden, 2001. URL: 
<http://www.cse.psu.edu/~tiu/thesisc.pdf>.

[2] Kai Bruennler. Atomic cut elimination for classical logic. 
Technical Report WV-02-11, Technische Universitaet Dresden, 2002. 
URL: 
<http://www.ki.inf.tu-dresden.de/~kai/AtomicCutElimination-short.pdf>, 
accepted at CSL '03.

[3] Kai Bruennler. Deep Inference and Symmetry in Classical Proofs. 
PhD thesis, Technische Universitaet Dresden, 2003. URL: 
<http://www.ki.inf.tu-dresden.de/~kai/phd.pdf>.

[4] Lutz Strassburger. Linear Logic and Noncommutativity in the 
Calculus of Structures. PhD thesis, Technische Universitaet Dresden, 
2003. URL: <http://www.ki.inf.tu-dresden.de/~lutz/dissvonlutz.pdf>.

[5] Alessio Guglielmi, The Calculus of Structures. Web site. URL: 
<http://www.ki.inf.tu-dresden.de/~guglielm/Research>.

[6] Charles Stewart and Phiniki Stouppa. A systematic proof theory 
for several modal logics. Technical Report WV-03-08, Technische 
Universitaet Dresden, 2003, URL: 
<http://www.linearity.org/cas/papers/sysptf.pdf>.

[7] Alessio Guglielmi and Lutz Straßburger. Non-commutativity and 
MELL in the Calculus of Structures. CSL 2001, LNCS 2142, pp. 54-68. 
URL: 
<http://www.ki.inf.tu-dresden.de/~guglielm/Research/GugStra/GugStra.pdf>

[8] Lutz Straßburger. MELL in the Calculus of Structures. Technical 
Report WV-01-03, to appear in Theoretical Computer Science. URL: 
<http://www.ki.inf.tu-dresden.de/~lutz/els.pdf>.

[9] Alessio Guglielmi. Recipe. Manuscript, 2002, URL: 
<http://www.ki.inf.tu-dresden.de/~guglielm/Research/Notes/AG2.pdf>.

[10] Alessio Guglielmi. Subatomic logic. Manuscript, 2002, URL: 
<http://www.ki.inf.tu-dresden.de/~guglielm/Research/Notes/AG8.pdf>.

[11] Alessio Guglielmi. A system of interaction and structure. 
Technical Report WV-02-10, Technische Universitaet Dresden, 2002, URL:
<http://www.ki.inf.tu-dresden.de/~guglielm/Research/Gug/Gug.pdf>, submitted.

-- 

Alessio Guglielmi
Technische Universitaet Dresden
<http://www.ki.inf.tu-dresden.de/~guglielm/>