Subject: Re: Frogs and Pigeons
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-03-08 13:29:49 GMT (1 year, 9 weeks, 2 days, 3 hours and 30 minutes ago)
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