Re: Frogs and Pigeons

Kai and Giorgi,

Even for the system with cut it can considered to be open. As far as I 
know, the situation is the following:

The work by Paola and Alessio shows that SKS and Frege systems p-simulate 
each other. Hence, by the work of Samuel Buss, we know that we can produce 
a polynomial size proof with cut for the pidgeon-hole principle. However, 
nobody has worked out how this proof actually looks like. That's why, I 
consider it to be an open problem to exhibit polynomial size proof with 
cut in CoS for pidgeon-hole.

Then, there is a notion of "SKS with substitution" (see the work by Paola 
and Alessio), such that "SKS with substitution" and "Frege with 
substitution" p-simulate each other. The interesting point here is that 
for "SKS with substitution" one can have a version with cut and a cut-free 
version (which is not possible for Frege systems).

Now it is very easy to exhibit a polynomial size proof for the 
pidgeon-hole principle in the cut-free version of "SKS with substitution".

If you are interested in the cut-free version of ordinary SKS (without 
substitution), then the problem is open, but there is very strong 
evidence, that it is impossible. In fact, I've spent some time trying to 
prove that there is no polynomial size proof in KS for Pidgeon-hole, but I 
did not yet succeed.

Cheers,
Lutz