Proof Complexity of the Cut-free Calculus of Structures

We investigate the proof complexity of analytic subsystems ofthe deep inference proof system SKSg (the calculus of structures).Exploiting the fact that the cut rule (i) of SKSg correspondsto the ¬-left rule in the sequent calculus, we establishthat the ‘analytic'system KSg+c has essentially the samecomplexity as the monotone Gentzen calculus MLK. In particular,KSg+c quasipolynomially simulates SKSg, and admits polynomial-sizeproofs of some variants of the pigeonhole principle.