Proof Complexity of the Cut-free Calculus of Structures
Emil Jeřábek · Journal of Logic and Computation · 2008
We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i↑) of SKSg corresponds to the ¬-left rule in the sequent calculus, we establish that the ‘analytic'system KSg+c↑ has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSg+c↑ quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.