Re: Re: Frogs and Pigeons

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