Monotone simulations of non-monotone proofs

摘要

We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis ∧,∨) can be turned into a proof containing only monotone formulas of size mO(logm) and with the number of proof lines polynomial in m. Also we show that some interesting special cases, namely the functional and the onto versions of Pigeonhole Principle and a version of the Matching Principle, have polynomial size monotone proofs. We prove that LK is polynomially bounded if and only if its monotone fragment is.