Re: Proof nets and bureaucracy

At 17:28 +0200 7.9.04, Lutz Strassburger wrote:
>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.

Yes, formal semantics is actually one of the goals of the project. 
However, what I mean with the moral definition of bureaucracy is a 
bit more than just aesthetics.

For example, even if we don't know precisely what the technical 
semantics of a proof is, we might decide to distinguish two classes 
of proofs that differ in their complexity with respect to a class of 
tautologies they prove. In such a situation, we might also decide 
that the higher complexity proofs are complex because of bureaucracy. 
This would tell us that we want to remove this bureaucracy from our 
notion of proof net.

Another example: we could to try to disallow in nets proofs that 
introduce formulae that are not used later on in the proof. I mean, 
making a weakening immediately followed by a contraction, on the same 
formula, is of course very questionable and bureaucratic under every 
conceivable semantics.

So, one needs not to know everything about semantics for being able 
to use some semantics criteria.

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

Cut-free in the usual sense: what I meant with the parentheses is 
that there are two cases: a general case involving derivations where 
cut is allowed, and a special (more challenging) case involving 
cut-free derivations. The interest here is, for example, for theories 
like arithmetic. One is interested in transforming cut-free proofs 
involving non-logical axioms.

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

Actually, I think that distinguishing formulae by their internal 
associativity and commutativity is already perverse.

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

I think this is a very important point.

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

As you said, we can consider an order of formalisms, where

    CoS > `A' > `B' > deductive proof nets > your proof nets .

There will be transformations that take a derivation in a bigger 
formalism and transform it into a proof in the formalism immediately 
following in the order. For example, a proof in CoS can be 
transformed into a proof in `A', a proof in `A' into a proof in `B', 
etc.

It would be nice to have since the beginning another transformation 
that transforms every proof in CoS, `A', `B', etc. into one of your 
proof nets, and then check that this is invariant wrt the other 
transformation; example:

    CoS -> `A'
      \    /
       \  / .
        \/
       ypn

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

Sure, OK. I meant something different than `Lafont's counterexample'. 
I mean, two really different proofs of the same propositional 
formula, not just a juxtaposition of independent proofs.

-Alessio