Re: contraction is not admissible for co-contraction

Hello,

I'd like to make a correction and further elaborate on the last part 
of my last message:

>But suppose I'm right and the pigeonhole principle makes for the 
>desired counterexample. Next question: would putting the pigeonhole 
>principle in the place of contraction leave system KS complete, 
>perhaps with the addition of cocontraction? (Note that the 
>pigeonhole principle is an infinitary rule whose premise is `true' 
>and conclusion an arbitrarily large formula scheme.)

First of all, as it stands this clearly cannot work, because, for 
example, it doesn't prove Kai's counterexample, posted last December:

    [ ( [a,b] , [-c,(a,b)] ) , (-a,-d) , ( [(c,d),-b] , [c,d] ) ] .

Actually, I meant this: to substitute contraction with something 
equivalent, which doesn't explicitly duplicate formulae, *derived* 
from the pigeonhole principle, in whatever contraction-free system 
(possibly not KS).

The rationale is the following: what is contraction good for, in a 
bottom-up reading of proofs? It makes possible to share subformulae, 
which are later annihilated in identity axioms (or weakening, if one 
is wasteful). Is it possible to find a universal sharing-destruction 
mechanism which hides contraction inside itself?

For example, if we adopt 3 pigeons-2 holes as an inference rule, we just state

                                      t
    p_3 ------------------------------------------------------------- .
        [(-A,-B),(-C,-D),(-E,-F),(A,C),(A,E),(C,E),(B,D),(B,F),(D,F)]

There is no apparent duplication in this rule, but we know that if we 
wanted to prove it in a system with contraction we would have to use 
a great deal of duplication.

Of course, the class of rules p_i is way too specific to possibly 
make a system complete. One might think of trying to distill from 
them the `essence of duplication' and cook it in some more universal 
rules that do the job, possibly helped by different rules in the rest 
of the system for classical logic.

Why the pigeonhole? Because it's the only *infinite* class of 
formulae I know with such a compact and uniform understanding of a 
very intricate use of contraction, and one which is known to yield 
exponential complexity.

If you look at it, you see that the trick for proving it is in making 
chains of dependencies based on sharing resources. Now, it's natural 
to believe that if you hide the mechanism for making the individual 
pieces in the chain (contraction), you need somehow to retain the 
ability of making chains of arbitrarily large size, whence the need 
for an infinite class of (possibly uniform) provable formulae.

OF COURSE, one shouldn't dream that pigeonhole-derived rules will 
hide exponential complexity by retaining completeness. In order not 
to prove P=NP by magic, we must compensate this with something else 
that *introduces* complexity. I believe that this could be some 
mechanism that greatly enhances applicability of rules to a given 
formula or structure.

In summary, I believe that it's possible to look at the pigeonhole 
principle (especially from the point of view of deep inference and 
CoS) and learn how to design rules in which creation/destruction is 
done at the same time with no loss of completeness.

(You can find something about the pigeonhole principle in the paper 
`Making Proofs Without Modus Ponens', by Carbone and Semmes, 
available on Groucho [l: groucho p: marx], 
<http://www.ki.inf.tu-dresden.de/%7eguglielm/Groucho/Carbone/MakingProofsWithoutModusPonens.pdf>.)

-Alessio