Subject: Re: Re: Frogs and Pigeons
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-03-27 15:28:32 GMT (1 year, 6 weeks, 4 days, 6 hours and 29 minutes ago)
On Thu, 22 Mar 2007, Giorgi Japaridze wrote:
> Lutz,
>
>> 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".
>
> Would that proof involve (other than substitution) only analytical rules,
> or would it also have to use some non-analytical rules such as upward aw?
All you need is the down-fragment of SKS, and a pair of substitution rules
S{a} S{-a}
------ -------
S{A} S{-A}
for every substitution a <===> A that you fix in the beginning (clearly,
the a's must be fresh propositional variables)
Then you simulate the proof of the propositional PHP as it is for example
given by Haken in "The Intractability of Resolution", TCS 39,
1995,pp297-308
The only rule that introduces material while going up in the proof is the
atomic contraction rule
S[a,a]
------
S{a}
Ciao
Lutz