Re:deductive proof nets

Hello,

perhaps `deductive proof net' is not the right 
expression to describe a net whose checking is 
linear, and one should reserve the word for a net 
with some kind of modularity. What about 
`explicit proof net'? On the other hand: how can 
one define a modular, deductive proof net in 
general terms?

In any case, I believe that going for a linear 
criterion makes for a better perspective than 
asking for modularity. In general, 
implicit/semantic notions bring many more fruits 
than explicit/syntactic ones.

Moreover, the real point with proof nets, I 
believe, is not much checking them, or using them 
as deductive tools, rather it should be their 
being objects intermediate between syntax and 
semantics, i.e. not too abstract but not too 
concrete. The question is whether asking for 
linearity is enough to expose just the `right' 
amount of concreteness. I don't know, of course.

What could happen is that if somebody simply goes 
for a correctness criterion of moderate 
complexity, then afterwards a modular 
understanding might become possible. It seems to 
have happened already with MLL proof nets. Have a 
look at this paper by Dominic Hughes: 
<http://boole.stanford.edu/~dominic/papers/seq/seq.pdf>.

-Alessio


At 10:17 +0200 7.9.04, Kai Brünnler wrote:
>>I don't know whether emphasising so much 
>>computational complexity is the right thing to 
>>do.
>>[...] There is one thing that this complexity 
>>view doesn't require, namely the kind of 
>>compositionality which is usually associated to 
>>deduction.
>
>Compositionality seems central to me. While I 
>would certainly expect that the task of 
>verifying a proof is computationally easy, I 
>think that I expect something more.
>
>When I have to check a proof and in the middle 
>of it I have to pop out for lunch then I can put 
>a check mark on the lemmas that I've already 
>checked such that when I come back I can resume 
>where I left, without having to do anything 
>twice. Of course there's a way to do the same 
>thing with proof nets. But the question is: what 
>does that mean, logically, to have checked half 
>of the correctness criterion?
>
>Shouldn't this be the difference between 
>deductive, compositional (say sequent calculus) 
>and non-deductive, global (say proof nets, 
>connection method)? In the first case you do 
>half of the work and you get some intermediate 
>theorem from which the original theorem follows 
>once you've done the other half. In the second 
>case doing half the work doesn't get you that 
>intermediate theorem, as far as I can see.