Re: Quasipolynomial cut-elimination in CoS

Dear Giorgi,

On Fri, Aug 3, 2012 at 8:18 AM, Giorgi Japaridze
<[email protected]> wrote:
> Does KSg+cocontraction or KS+cocontraction allow quasipolynomial cut
> elimination? (I know that SKS does, but it is not "analytic" because of
> coweakening.)

A cut-free SKS proof can be transformed to a KS+cocontraction proof
without increasing it's size. Simply permute all coweakenings "up" in
the proof. What will happen is:
1) coweakenings simply pass through linear rules
2) coweakening meeting a weakening or a cocontraction erase both rules
3) coweakening meeting a contraction removes the contraction and puts
two coweakenings in its place
4) coweakening meeting an axiom will erase the coweakening and the
axiom and replace them with a weakening

> If yes, any detailed references, including page and/or theorem numbers, will
> be greatly appreciated.

Proposition 7.3.1 on page 78 of
<http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf>;
alternatively
Theorem 4.12 on page 19 of
<http://www.lmcs-online.org/ojs/viewarticle.php?id=341>.

Cheers,

Tom