Re: Proof nets and bureaucracy

At 0:09 +0000 3.9.04, Charles Stewart wrote:
>  > 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.
>
>By "difficult" do you mean the same sense as it being difficult to
>read back a Hilbert-style proof from a natural deduction one?

Perhaps; in general, I just mean `computationally expensive'. I don't 
know whether emphasising so much computational complexity is the 
right thing to do.

On the other hand, what is a deductive formalism? I certainly don't 
think it's appropriate, when dealing with proof nets, trying to 
define deduction in the usual, operational style.

There is one thing that this complexity view doesn't require, namely 
the kind of compositionality which is usually associated to 
deduction. In fact, the definition of deductive proof net I gave 
allows for nets which can be verified in linear time in a global 
fashion, without necessarily being able to make the checking by 
decomposing the net into subnets.

Perhaps, a better moral definition of deductive proof net should try 
to include some kind of compositionality. In this case, one could 
move outside of the scope of this definition traditional MLL proof 
nets, which is probably a good thing to do (unless somebody found a 
compositional, linear correctness criterion for them).

Any ideas?

-Alessio