Re: Wires and pipes

Alessio,

On Tue, 15 Mar 2005, Alessio Guglielmi wrote:

> This email has three parts: Motivations, Intuition and Technicalities. 
> Reading up to Intuition should be enough to get a good idea, if you know 
> already about CoS and KS.
>
> I would be very grateful if somebody checks the technicalities, though. They 
> are nontrivial and unfortunately very combinatorial. Clearly, they might be 
> wrong, but it should be possible to fix any mistake without changing the 
> general picture.

I did not read the technicalities, because I somehow disagree on the 
intuition. But I perfectly agree on the motivation.

> INTUITION
> =========
>
> ...
>
> The main idea goes as follows: there is a denumerable set of wires. Wires are 
> neither created nor destroyed. To wires we associate atoms, and the 
> association may vary in the course of the derivation.

So far, I agree.

> Moreover, at any given time bunches of wires are organised into a tree of 
> logical relations, which also can change over time. For example, the 
> following is a derivation of a from (a V a) (so, it's a contraction):
>
>   [a a]
>    | |
>   [a f] .
>
>    1 2
>
> There are two wires, 1 and 2, vertically disposed, and we assume that time 
> flows vertically going upwards. In the beginning, a is associated to 1 and f 
> is associated to 2. In traditional logic, a would be a propositional variable 
> and f would be the `false' unit; both are atoms for us. Wires 1 and 2 are in 
> a disjunction relation (indicated as usual in CoS). After some time wire 2 
> gets the value a, but the logical relation between wires does not change.

My critisicism regards the way you deal with contraction. In my opinion, 
"morally" both atoms upstairs should be wired to the a downstairs. In your 
way, you have to make a choice and prefer one of the two. this introduces 
new bureaucracy that is not even there in CoS or the Sequent Calculus.
Consider for example

     ([A,a],[B,a])
s,s ---------------
     [(A,B),a,a]
 c_ -------------
      [(A,B),a]

In your wired formalism one of the a upstairs is wired to the a 
downstairs, and the other a is wired to an artificial f.
There two ways of doing it, and they cannot be identified by your wired 
formalism, or am I missing something?


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

> This setup clearly works for classical logic, and all our results with CoS, 
> and my preliminary work with subatomic proof theory, tell us that this should 
> work for *any* logic. Of course, in general f and t are simply the units of 
> whatever disjunction and conjunction one has, for example they would be 
> bottom and one for linear logic.

That depends on what you mean by "work".

> The general geometry is given by the wires: we *always* assume that they live 
> under a commutative and associative equivalence. In the case of 
> non-commutative logic, the non-commutativity will be represented by the 
> logical relation between wires, not by their geometry. In other words: if you 
> take the horizontal section of any derivation like the ones above, you always 
> have a relation web (back to the origins).

Nonetheless, I think that this picture is the right starting point.

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

>       (t  t)         [a a]         (f t)
>   wi_ -|--|- ,   wc_ -|-|- ,   ww_ -|-|- ,
>       [a -a]         [a f]         [a f]
>
>      (A [B  C])       [(A B) (C D)]
>   s  =|==|==|=  ,   m  =|===X===|=  .
>     [(A  B) C]        ([A C] [B D])

ww_ is weird in several ways:
1) Having a t above wired to an f below is weird.
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.

> Of course, I have to show that this system is complete for classical logic 
> (soundness is trivial). I could do it semantically, for example by showing 
> how to get disjunctive normal forms and then realising resolution and appeal 
> to its completeness.

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.

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

-Lutz