Re: Frogs and Pigeons

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?

Giorgi