On the Proof Complexity of Deep Inference

TL;DR

This paper explores the proof complexity of deep inference, showing its equivalence to Frege systems even with extensions, and demonstrating exponential speed-ups over Gentzen systems in certain cases.

Contribution

It proves deep inference systems are as powerful as Frege systems with extensions and identifies exponential speed-ups over Gentzen systems.

Findings

Deep inference systems match Frege proof power with extensions.

Existence of analytic deep inference systems with exponential speed-up.

Polynomial simulation of Gentzen systems by deep inference.

Abstract

We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.