Proof nets and bureaucracy

Hello,

perhaps it doesn't hurt if I try to summarise the situation about 
proof nets and bureaucracy. I should say that I'm no expert at all 
and I didn't actually make up my mind about this. So, I'd like to 
share my thoughts on this subject and I would very much appreciate 
any feedback on these.

Let me attempt a few *moral* definitions first:


BUREAUCRACY   We have bureaucracy in all cases in which syntax 
behaves unnaturally from a semantic point of view.

* Example 1: par-right rules in MLL permute, so that the following 
two derivations are morally the same but bureaucracy forces a 
distinction:

    a,  b, c,  d         a,  b, c,  d
    ------------         ------------
    a,  b, c P d         a P b, c,  d
    ------------   and   ------------ .
    a P b, c P d         a P b, c P d

* Example 2: it would be natural to move all contraction rules at the 
bottom of a derivation, but, for example in the multiplicative 
sequent calculus for propositional logic, this is impossible, as 
shown by Kai's counterexample: try to prove the sequent

    |- a ^ a, -a ^ -a

without using any other rule below contractions.


So, bureaucracy is a bad thing, and one of our goals should be to get 
rid of it. Regarding the two examples above, in CoS we make the 
situation worse than in the sequent calculus wrt the kind of 
bureaucracy of Example 1, while we improve it a lot wrt the kind of 
bureaucracy of example 2.

The improvements come from the finer granularity of our inference 
rules and then the existence of powerful decomposition theorems. 
Regarding making the situation better for permutability: formalisms 
`A' and `B' address the problem, and getting rid of the last remains 
of bureaucracy is the main reason to develop them. (Note that it 
would be impossible to develop `A' and `B' starting from any other 
formalism than CoS!)

* * *

Proof nets were invented, I guess, exactly for the purpose of getting 
rid of bureaucracy, and so, hopefully, providing canonical 
representatives of equivalence classes of identical of proofs. They 
are a brilliant idea, in principle, but I believe that the state of 
the art of proof nets derived from the linear logic ones has very 
little appeal.

Now, the following assessment might be just an embarrassing sign of 
my ignorance, but it looks to me that the field became just a 
playground for technical prowess more than an inspiring and useful 
part of proof theory. It also lacks a clear direction and strong 
ideas. Try to convince me that I'm wrong (but be polite, I admitted 
my ignorance!).

Anyway, it's uncontroversial that proof nets as they are commonly 
conceived are not deductive, in the sense that reading back a 
deductive proof is `difficult'. This is neither a good or a bad 
thing: it's just a fact, and this prompts me to define the following 
two moral notions.


PROOF NET (1)   A proof net is a bureaucracy-free (graphical) 
validity certificate whose correctness is decidable.


DEDUCTIVE PROOF NET   A deductive proof net is a bureaucracy-free 
(graphical) validity certificate whose correctness is decidable in 
linear time (wrt the size of the net).


Clearly, both definitions require a previous understanding of what is 
bureaucracy, and this is usually understood inside a deduction 
system. The first definition could then probably be given as:


PROOF NET (2)   A proof net is a bureaucracy-free (graphical) 
representative for a class of proofs whose correctness is decidable.


Here, we assume to know already what proofs are, probably inside 
another deductive system, like the sequent calculus or CoS. In this 
case, a sequentialisation theorem doesn't hurt.

Are these moral definitions reasonable?

Anyway, let's say that a deductive proof net is a proof net whose 
correctness criterion doesn't cost much. In some sense, checking the 
correctness of the net corresponds to checking deduction steps, 
whence the insistence on the complexity of the criterion to be linear.

Remark: If we adopt these definitions, then proof nets for 
multiplicative linear logic are deductive, thanks to Guerrini's 
result. They still don't look very deductive to me, but I'm not sure 
one should change the definition just for this. However, if we found 
a concise definition which is also better in this respect, that would 
be nice.

I believe that both notions of proof nets need to be developed. 
Generic, non-deductive proof nets can clearly be very compact 
objects, where much information is implicit. They might even be 
adopted as semantics in lucky circumstances.

On the other hand, a proof net is first and foremost syntax, I 
believe, and I'm still reluctant to see syntax entirely distinct from 
deduction. I mean, I believe that if syntax is around, in most cases 
it should correspond to deduction, possibly in an explicit way!

* * *

Orthogonally to all this, I think that another direction should be 
explored, namely the generalisation of the idea of proof net towards 
that of `derivation net'. This is what I think Lutz was explaining in 
previous emails.

I'm using the word `derivation' of conclusion B from hypothesis A in 
the sense of a validity certificate for the implication A -> B, such 
that a `proof' is a derivation for t -> B and a `refutation' is a 
derivation for A -> f.

So, the previous two definitions can be generalised in a 
straightforward way to DERIVATION NET and DEDUCTIVE DERIVATION NET.

If I didn't misunderstand, Lutz proposes a notion of derivation net 
for classical logic where a certain class of derivations for A -> B 
is represented as a net

       ^
      / \
     /-A \
    +-----+
    | X X | ,
    +-----+
     \ B /
      \ /
       V

such that the tree B is a formula tree for B and the tree -A is the 
formula tree for A upside-down and De Morgan-dualised. Between the 
two trees, several links are drawn between occurrences of atoms.

The trick is, of course, to check the net with a correctness 
criterion in order to see that the net really corresponds to a 
derivation. Since the net is polynomial in the size of A and B, this 
checking will likely require an exponential time, unless coNP = NP, 
which is, of course, unlikely. Lutz claims to be able to do this by 
using a splitting theorem in CoS (this looks entirely reasonable to 
me).

Am I right, Lutz?

Why is it important to study derivation nets? My take of this is the 
following. If we understand derivation nets, then we are able to take 
any proof of a given statement and to turn it around any subformula 
we might choose. For example, if we have a proof for A V B V C, we 
can study it as a derivation of B V C from -A, or of A V C from -B, 
and so on.

In some sense, this means capturing the essential symmetry of logics 
with involutive negation. On the other hand, it seems to me that 
derivation nets don't make real justice to this symmetry, unless we 
find *deductive* derivation nets.

In fact, if we know that A V B V C is provable, we know *already* (by 
semantics) that B V C is derivable from -A. The correctness criterion 
is not going to tell us anything more than this. What is more 
interesting is transforming (cut-free) *deductions* of A V B V C 
(from t) into (cut-free) *deductions* of B V C from -A.

Am I missing something here, Lutz? So, what I claim is that the 
top-down symmetry is mostly useful in the syntax only in presence of 
deductive derivation nets.

Of course, it looks like finding the correct notion of deductive 
derivation net is going to be a hard task.

* * *

In view of the objective of getting to deductive derivation nets, my 
personal research program is as follows: instead of starting from the 
most abstract objects, i.e., proof nets, let's start from the most 
concrete ones that show a top-down symmetry, i.e., CoS derivations, 
and then let's get rid of bureaucracy.

In CoS, bureaucracy consists (exclusively, I guess) in permutability 
of rules. Without getting into the details here (I posted some of 
these ideas already), I intend to proceed towards the goal in two 
steps, by first developing formalism `A' and then formalism `B'.

Formalism `B' is going to be CoS without any bureaucracy in the sense 
of permutability of rules. Whether this can induce some reasonable 
notion of proof net is an open problem. Every time I try to see `B' 
in graphical form I get motion sickness. Anyway, I do think that with 
the appropriate amount of effort one can arrive to a decent graphical 
syntax, at least so I hope.

I'd like to know Lutz's opinion on an idea I've got after reading his 
email. Lutz, do you think that your proof nets for propositional 
logic could be a *reasonable* normal form for CoS derivations?

In other words: is it possible to transform any given CoS derivation 
in, say, SKS, and transform it *by a very simple induction on its 
length* into one of your derivation nets? If so, we might think of 
using your derivation nets as an invariant and to check the behaviour 
of the systems we produce wrt it. Of course, `A' and `B' are meant to 
retain all the good properties of CoS, and I hope that a simple 
distillation of derivation nets would not break when moving from CoS 
to `A' and then to `B'.

By the way, just out of curiosity, can you show two *different* 
derivation nets for the same implication A -> B?.

OK, I guess I stop here. I'd very much appreciate the comments of 
those with the patience to read some of this huge email. You know, I 
don't write to be read, just to clarify things to myself...

(We are in a phase in which we have to write at least one survey 
about our past four frenetic years, so it's also a good time to 
assess the situation and make plans for the future.)

Ciao,

-Alessio