Two more FAQ entries

Hi,

it's me again. Two more entries for the FAQ, please comment. In 
general, do you have any complaint or suggestion for the FAQ page?

-Alessio


*** Question   Aren't proof nets top-down symmetric objects, not 
differently than proofs in the calculus of structures?

*** Answer   No, proof nets are top-down asymmetric: they consist of 
trees with some links on top (in the simplest case of multiplicative 
linear logic). If you flip a proof net upside-down, you don't get a 
dual proof net, just an upside-down one.


*** Question   There is more bureaucracy in the calculus of 
structures than in the sequent calculus, and this is why you get more 
properties: simply because you have more stuff to work with, right?

*** Answer   Wrong, and the answer doesn't even depend on the notion 
of bureaucracy you use. Since you can design systems in the calculus 
of structures which completely and faithfully mimic systems in the 
sequent calculus, the bureaucracy is at worse the same as in the 
sequent calculus, no matter which notions you use. However, since in 
the calculus of structures you have access to deep inference, you can 
design inference rules which are much more efficient than what is 
possible in shallow inference, and this reduces bureaucracy. This is 
most prominently testified by the fact that in the calculus of 
structures there are classes of proofs which are exponentially 
shorter than proofs of the same sentences in the sequent calculus.