Proof Complexity of the Cut-free Calculus of Structures
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 analyticsystem KSgc has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSgc quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.
proof complexity calculus of structures cut rule monotone sequent calculus