ALCOMFT-TR-02-131

Albert Atserias, Nicola Galesi and Pavel Pudlák
Monotone Simulations of Nonmonotone Proofs
Barcelona. Work package 4. May 2002.

Abstract: We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis \wedge,\vee) can be turned into a proof containing only monotone formulas of size m^{O(log m)} 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 PHP 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.

Postscript file: ALCOMFT-TR-02-131.ps.gz (60 kb).