Proof Complexity of Monotone Branching Programs

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dagstructure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT(+) is obtained by restricting their systems to a positive syntax, similarly to how the `monotone sequent calculus' MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT(+) polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudl ' ak, that was recently improved to a bona fide polynomial simulation via works of Je.r ' abek and Buss, Kabanets, Kolokolova and Kouck ' y. Along the way we formalise several properties of counting functions within eLNDT(+) by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.