We give uniform versions of propositional logic deep inference systems in the setting of 'bounded arithmetic', relating the size of propositional proofs to forms of proof-theoretic strength in fragments of arithmetic.

This continues the recent program of studying the complexity of deep inference proofs by bringing it in line with the standards of mainstream proof complexity. It is also inspired by previous work where proofs of the propositional pigeonhole principle in the minimal deep inference system, KS, were constructed using rather abstract uniform templates, suggesting the need for such an approach.

To minimise prerequisites we work in the setting of monotone proofs represented as rewriting derivations, isolating fragments of so-called 'analytic' deep inference. For the same reason we construct our arithmetic theories by adapting the well studied IDelta_0 of Parikh, Paris, Wilkie and others, although similar theories could be designed using the more modern second-order setting of Zambella, Cook and Nguyen.

Along the way we require a blend of tools from bounded arithmetic (correspondence with propositional proofs), deep inference (efficient normalization of propositional translations), and descriptive complexity (taming the closure functions of least fixed point operators used to simulate deep inference).