Re:Proof nets and bureaucracy

>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.

I forgot to say one thing. There's another case in which syntax 
behaves unnaturally from a semantic point of view: when too much 
complexity is introduced.

* Example 3: Take Statman's tautologies (see an earlier post): they 
can be proved polynomially in their size by a semantic argument, but 
several deduction systems only yield exponential proofs, for example 
the cut-free sequent calculus.

CoS behaves very well in this respect, it's probably the best 
formalism. Truth tables are of course very bad.

If we consider complexity a bureaucratic problem and adopt the moral 
definition of proof nets that I suggested yesterday, I believe that 
there is no need to state that they should be graphical objects. This 
is simply because in order to beat complexity, one is naturally led 
to use `data structures' much richer than trees.

Ciao,

-Alessio