Re: Wires and pipes

Hello,

before answering all Lutz's remarks and concerns, I'd like to make a 
bit clearer what I tried to propose in the previous message about 
wired deduction.

The proposal had two parts: 1) a formalism and 2) a deductive system.


THE FORMALISM

Wired deduction is the realisation of a formalism which:

1  gets rid of associativity- and commutativity-bureaucracy;
2  gets rid of type A and type B bureaucracy;
3  does not generate non-canonical derivations for these forms of bureaucracy;
4  it is deductive (in the sense that checking soundness is linear in 
the size of the proof, or, if you prefer, checking soundness is 
local);
5  it is geometric (in the sense that it relies on graphs and 
normalisation can be defined locally).

I would add that derivations seems to be typographically acceptable, 
what I was not able to do, for example, with the deductive definition 
of formalism B.

There is *one* very ideological choice in the design of wired 
deduction, namely the insistence on linearity. This is expressed by 
the idea that no wire is created or destroyed, and that everything in 
the derivation happens inside the rigid, predetermined amount of 
wires.

I have three mystical reasons for this choice:

1  it is conceptually pure, and so very appealing to me;
2  it sets the bar very high, but (apparently) not impossibly high;
3  it is perfectly in line with `subatomic proof theory'.

The best thing anybody can do about these opinions is to be 
skeptical, and maybe even consider them pure crap. This is better for 
me, too: I want to be challenged on this.

However, notice that it is possible to *trivially* modify wired 
inference in such a way that the linearity constraint is abandoned. 
If you do so, any system in CoS, and so any logic, can immediately be 
expressed in wired deduction in such a way that ass/comm-, A- and 
B-bureaucracy types are absent.

The whole thing would simply boil down to observations on the shape 
of CoS rules. As a matter of fact, this would make technical what I 
always said about CoS, namely, that it *reduces* bureaucracy, and not 
the other way around.

One word about different kinds of bureaucracy: it is not fair to 
consider type A and type B on the same level as bureaucracy of the 
kind `order-of-contractions', for example (see below). In fact, in 
order to get rid of bureaucracy of type A or B, one has to have a 
*global* vision of a given derivation, what is not the case for 
order-of-contractions.

In other words: you cannot get rid of type A or B bureaucracy by 
simply adding rule schemes to a deductive system. On the contrary, it 
is possible to do so in order-of-contractions bureaucracy (see below 
for more details).


THE DEDUCTIVE SYSTEM

The deductive system KSw that I presented is admittedly provocative, 
and in fact it provoked all of Lutz's reactions.

Perhaps I haven't been clear enough on one important point: it is 
possible to present regular KS in wired deduction in the obvious way: 
just translate all rules into rules and all unit equations into 
rules. This would cure all of Lutz's criticism except for the one on 
contraction. Going for a `nonlinear' wired deduction would be a cure 
for that, too (we just would be back into CoS, but without the 
bureaucracy).

However, the problem with contraction's bureaucracy is deeper than 
Lutz suggests, and the only real cure is to fix it in the deductive 
system, what is possible also in wired deduction without any 
modification.


Contraction
-----------

In the derivation

        ([A a] [B  a])
     s   =|==\==|  |==\=
       [( |    [|  |]) a]
     s   =|=====|==|=  |  ,
       [( |     |) a   a]
   wc_    |     | -|---|-
       [( A     B) a   f]

the two a's will always be distinguished by any permutation of wires, 
given their distinct provenance, so Lutz is correct in saying that if 
one wants to identify the two cases, system KSw doesn't help.

We can put the blame on wired deduction, because if we drop the 
linearity condition, in, say, `nonlinear' wired deduction, then the 
problem is solved:

        ([A a] [B  a])
     s   =|==\==|  |==\=
       [( |    [|  |]) a]
     s   =|=====|==|=  |  .
       [( |     |) a   a]
   wc_    |     |  -\-/-
       [( A     B)   a  ]

(Notice that, in order to identify the two possible derivations 
obtained by changing the switches order, one has to use a double 
switch rule, but this doesn't matter here.)

However, I claim that the problem with contraction bureaucracy is a 
deeper one, and moving to nonlinear wired deduction wouldn't help. 
The only real cure is fixing the problem in the deductive system: 
this is a deductive-system-level bureaucracy! Fixing the deductive 
system *can* be done in wired deduction.

The problem is simply one of associativity: take, in *any* deductive formalism,

       a   a
        \ /          a   a a   a
     a   a            \ /   \ /
      \ /      and     a     a    .
   a   a                \   /
    \ /                  \ /
     a                    a

How do you equate these derivations? The only solution is to use an 
n-ary atomic contraction rule:

   a a a a
   ------- .
      a

(The right attitude towards trees is that of the lumberjack.)

This is perfectly possible also in wired deduction:

       ( ([A a] [B    a])    t  )
     s    =|==\==|    |==\=  |
       ([( |    [|    |]) a] |  )
     s    =|=====|====|=  |  |
       ([( |     |)   |   |] |  ) .
     s    =|     |====|   |==|=
        [( |     |) ([a   a] t)]
   2c_     |     |   -|---|--|-
        [( A     B)   f   f  a ]


Weakening
---------

Yes: the ww_ rule is completely wacky! As I said above, it would be 
perfectly possible in wired deduction to substitute it with the 
innocuous one:

        f
   aw_ -|- .
        a

This would eliminate all problems of `horrible duplications' that 
Lutz points out.

However: there are two things to consider:

1  The ww_ rule is always permutable with any other rule: it uses two 
wires, but it behaves like if it used just one. So, it is perfectly 
conceivable to use some shortcut notation to deal with it, and one 
would never really notice the difference with aw_. So: until you 
really want to get into some fine details of unit behaviour, it's 
pure cosmetics, nothing deep.

2  I'm using ww_ in KSw because it allows me to *get rid of all unit 
equations* (i.e., of all equations that have no direct relevance to 
bureaucracy) and still simulate KS. Maybe there is a better way of 
doing so, but I couldn't find one (it's an interesting Rubik's kind 
of puzzle, if you have an hour in the dentist's waiting room.).

3  The rule ww_ comes straight from subatomic proof theory, and it 
magically works. (I don't count this one among the things you should 
consider.)


Now, let's see the remaining points:

At 14:10 +0100 16.3.05, Lutz Strassburger wrote:
> > So, what are derivations? Derivations are nets of the kind seen 
> > above, whose general shape is
> >
> >   ( <R> t ... t)
> >     \|| |    /
> >       <net>      .
> >     /|| |    \
> >   [ <T> f ... f]
> >
> > In other words, the premiss R is in the middle of any number of t 
> > wires in conjunction and the conclusion T is in the middle of any 
> > number of f wires in a disjunction. *No wires are created or 
> > destroyed*: in this sense, this formalism is always *linear*. A 
> > proof, of course, is a derivation with all t's in the premiss.
>
> I believe that this would work only for multiplicative linear logic. 
> As soon as you have contraction and weakening, you must duplicate or 
> create/destroy wires.

You might be right, of course, and this is why I'm saying that I'm 
setting the bar high: the case when you have more than two logical 
units might be tricky. However, you might also be wrong!

Anyway, if you're right, then one would still be able to do linear 
logic in *nonlinear* wired deduction. This would be the right 
punishment for linear logic: in the end classical logic would shine 
in pure linearity and linear logic would rotten in the nonlinear 
slums.

> > So, this is propositional classical logic's system KSw; notice that 
> > there are *no equations*:
>
> What do you mean by *no equations*? In the technical section you 
> have equations for associativity and commutativity.

I mean no equations apart from those necessary to control bureaucracy.

> ww_ is weird in several ways:
> 1) Having a t above wired to an f below is weird.

I'm glad you noticed. I actually tried a bit getting rid of the 
anomaly, but didn't insist too much. In any case the rule is sound, 
so, who cares?

> 2) In order to simulate an ordinary weakening in KS, you have to do a
>    horrible lot of duplications via additional contractions (I just had a
>    quick look at the technicalities because I couldn't believe it)
>    In my opinion this is "morally wrong" because you lose a lot of
>    information about the proof and introduce bureaucracy which is worse
>    that A and B.

Why would you want to `simulate' w_? If you want it, just throw it in.

I'm not sure I understand what you mean by `losing information'.

> I think completeness should not be the issue. Getting all 
> tautologies is not the interesting task of proof theory. We should 
> ask for all proofs of a tautology. And figure out what that actually 
> means.

Do you have any clue about what (the hell) this question could mean? 
Should we ask for all the possible fathers of a child and figure out 
what that actually means?

> > However, I also want to check that the complexity of proofs does 
> > not grow wrt KS, which is the place where we mostly study it. So, 
> > in the technicalities, you will find a complete proof of the 
> > admissibility of KS equations for KSw.
>
> Well, I think you do increase the size simply because you need Thm 
> <PP> for getting r7, which you need for an ordinary weakening.

Yes, whenever you simulate anything into anything else, the size 
increases, but the question is whether it grows polynomially or not, 
and it looks to me that everything here behaves well.

-Alessio