Re: Proof nets and bureaucracy

Hello,

since Alessio explicitely asked me, I will give some comments on his mail on 
proof nets. I essentialy agree with him on most points, so there is not much 
to add.

On Thursday 02 September 2004 18:13, Alessio Guglielmi wrote:

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

I think the problem with that definition is, that it is in general not at all 
clear, what the semantics actually is. Or, in other words, what the 
denotation of a proof is. The case of MLL is now well understood. Any 
*-autonomous category can be used as semantics (eg coherence spaces), and 
proof nets for MLL form the free *-autonomous category.

But what actually is the denotation of a proof in classical logic? What is 
the semantic point of view? All we can say so far is when syntax behaves 
unnaturally wrt to our personal aesthetical feeling (I agree with all your 
examples). Of course, eventually we want to arrive at the right semtantic 
point of view. And I agree with you that Formalisms A and B and proof 
nets/derivation nets are the right way to go.

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

Well, I think that multiplicative linear logic itself is quite simple. And I 
don't think you can expect much more from proof nets for MLL. They pretty 
much capture the essence of an MLL proofs, and I do not see how one could 
make some improvement (except the trivial step to derivation nets that I 
discussed in a previous mail).

But I agree with you that all the extensions of proof nets to other logics 
lack appeal.

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

I think they are.

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

Yes

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

Exactly.
Let me repeat that for MLL this is a triviality.

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

Yes. For classical logic I have two different sorts of nets. For the simple 
ones it is true what you say, for the more complicated ones, where we keep 
track of the number of axiom links, the net is no longer polynomial in the 
size of A and B. So, there is hope for a non-exponential checking. But I have 
no clue how this could be done.

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

Exactly.

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

Here you have to be careful! We have to redefine what "cut-free" actually 
means. In the case above it could be that the proof of A v B v C contains an 
identity link killing two atoms coming from A. Then the corresponding 
derivation from -A to B v C must contain a cut that melts away these two 
atoms.

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

I agree. But I also think that in the beginning it is easier to look only at 
proof nets. I claim that the step from the right proof nets towards 
derivation nets (be it deductive or not) is rather simple.

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

Great.
Let me start from the other side, i.e., the proof nets. And I'll add more and 
more information about the deduction. Let's see where we meet.

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

I believe the *reasonable* solution is somewhere in between. Of course, the 
proof nets I have right now can easily be used as normal form for CoS 
derivations (It already works). However, I think there are too many 
identifications right now. 

But at least, I think I can make the following claim: My proof nets make as 
much identifications as possible, without getting the collapse into a boolean 
algebra.

On the other extreme, system SKS makes as little identifications as possible, 
provided all the equation are removed and made into rules. (I know that the 
formulation of the sentence is too strong because you can always invent weird 
formalisms and systems. But we can agree that making less identifications 
than SKS is not *reasonable*.)

We have therefore a partial order of formalisms, ordered wrt the 
identifications they make. Note that this order is only partial, and not 
total, i.e. there might be formalisms which cannot be compared wrt to the 
proof identifications they make. Take for example two different sequent 
systems. (All sequent systems are in between the two extremes, and I think 
they are all wrong wrt the identification they make.)

I think, we can safely state that formalism A is strictly greater than the 
right formalism, i.e., it makes not enough identifications, but it makes no 
"false" identifications. However, I have no clue about formalism B. 

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

Yes. It is almost trivial.

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

I do not understand what you mean here.

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

the simplest example is 
a ^ -a  -->  b v -b 
where you get three different "derivation nets". They correspond to the three 
different proof nets for the sequent 
|- a, -a, b, -b
(link a to -a, link b to -b, or make both links)  

-Lutz