Re: contraction is not admissible for co-contraction

Hello,

there was this old discussion about complete 
contraction-free deep-inference systems. I think 
I have a (very simple-minded) idea for settling 
it.

At 16:29 +0100 3.12.03, Kai Brünnler wrote:
>>The main question now is whether there could 
>>exist a complete system for classical logic 
>>without *any* kind of replication going up. In 
>>other words, does your counterexample rely on 
>>some `deficiency' of KS which is possible to 
>>overcome?
>
>Yes, that's the question. I don't know. Could 
>be. If so, then that would likely involve rules 
>that take deepness to a new level, in the sense 
>that the redex itself will involve contexts, I 
>conjecture.

I tend to believe that it is impossible under 
very broad assumptions. Let's assume inference 
rule schemes are the usual ones, made from 
schematic formulae or structures.

To prove the claim of impossibility, one could 
proceed as follows: given a maximum number of 
variables in a (deep, let's say CoS) rule scheme, 
there is only a finite number of sound possible 
rules if duplication is forbidden. Let's call I_h 
the set of sound inference rules with at most h 
variables.

Suppose we have an infinite class of provable 
formulae and suppose it's possible to partition 
it in subclasses C_i with the following property 
P:

    every premise of each formula in C_i under any 
rule in I_h is unprovable, if h<i.

Clearly, if this is the case then any system 
without duplication must be incomplete: it 
suffices to exhibit a sufficiently large formula 
in some C_i, with i big enough to be larger than 
the maximum number of variables in some rule of 
the system.

Is there a suitable candidate class of formulae? 
I believe the propositional pigeonhole principle 
could be such class, but I have to admit that I 
don't know it very well, so I could be very 
mistaken here. I just exhibit the pigeonhole 
principle for three pigeons and two holes, in 
case somebody wants to play with this idea. 
Generalising it is straightforward, as soon as 
you understand how it works.

3 pigeons, 2 holes:

    [(-p11,-p12),(-p21,-p22),(-p31,-p32),
     (p11,p21),(p11,p31),(p21,p31),(p12,p22),(p12,p32),(p22,p32)] .

Now, it's not necessarily easy to prove that the 
pigeonhole class possesses the property P. I 
believe it would be nice to use relation webs for 
doing so. This entire thing is very similar to 
the proof of Alwen's counterexample, and he also 
uses relation webs (aka traces).

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

-Alessio