Complexity of negation cancellation

Question

Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. Notation: $| \alpha |$ is the length of formula $\alpha$.

We are given a formula $\phi$. Cancel all cancellable negations in $\phi$ by applying all possible valid biconditionals (EDIT: such as the examples below) to get $\phi'$; for clarity we note that $\phi \leftrightarrow \phi'$. We are also given that $\phi'$ is monotonic. Are there examples where $| \phi' |$ must grow exponentially, or is $| \phi' |$ bounded by a polynomial? If there's an example of exponential growth, please show it.

EDIT: The following biconditionals are examples of what I'm trying to get at, formulas which can be used to cancel negations while preserving equivalence. The procedure would presumably be to unify the left-hand side of the formula with $\phi$ via unification and substitute the right-hand side as appropriate per unification.

$$\alpha \land (\lnot \alpha \lor \beta) \leftrightarrow \alpha \land \beta$$ $$\lnot \lnot \alpha \leftrightarrow \alpha$$

Answer 1

I suspect the answer is that in general $\phi'$ might need to be of exponential size, but I am not certain. There are known examples of a boolean circuit $C$ (with negations) of polynomial size that computes a monotone function, while the smallest monotone boolean circuit $C'$ (with no negations) has exponential size. See http://www.cs.cornell.edu/~eva/Gap.Between.Monotone.NonMonotone.Circuit.Complexity.is.Exponential.pdf and Simple example of exponential gap between monotone and non-monotone circuits. It's possible that perhaps this could be extended to an argument that covers your case as well: if there is a polynomial-size formula $\phi$ corresponding to $C$ (this would need to be checked), the results above imply that any monotone formula $\phi'$ computing the same function would need to be of exponential size, so there would necessarily be an exponential gap for some functions, no matter what set of substitution rules ("biconditionals") you use. The gap in this argument is verifying whether Tardos's example can indeed be computed by a polynomial-size circuit; it's not clear whether it can, as circuits are more powerful than formulas, and I haven't verified this, but perhaps you can do so.