Cancellation of negations and the length of formulas

Question

Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. We are given a formula $\phi$. Cancel all cancellable negations in $\phi$ by applying all possible valid biconditionals such as the following to get $\phi'$. Are there examples where $\phi'$ must grow exponentially, or is the length of $\phi'$ bounded by a polynomial? If there's an example of exponential growth, please show it. $$\alpha \land (\lnot \alpha \lor \beta) \iff \alpha \land \beta$$ $$\lnot \lnot \alpha \iff \alpha$$

Answer 1

Possible approach / too long for a comment

This is NOT an answer for (at least) two reasons: (1) I modify the OP question with my own "treatment" (the OP author said they're open to the idea), and (2) Even under my treatment, there are gaps in my argument.

My treatment: Instead of worrying about transformation rules, we deal with equivalent formulas. Define the length of a formula in some natural way (e.g. no. of instances of atomic variables (i.e. counting multiple occurrences as multiple), or no. of total symbols used). Any formula implements a function $\{0,1\}^n \to \{0,1\}$, and there are many equivalent formulas implementing the same function. For a given function, let $X$ be the shortest formula, and $Y$ be the shortest formula among those that minimize the no. of negation symbols. The main feature of this treatment is that we don't have to worry about whether a set of (local) transformation rules can transform $X$ to $Y$.

The analogous question becomes: Is there a function where $length(Y)$ is exponential in $length(X)$? Here is a possible candidate.

Take $n$ atomic variables $x_1, \dots, x_n$, treat them as $0/1$ variables in $\mathbb{N}$, and the function is $\sum_{i=1}^n x_i \ge n/2$.

Length of $X$: Obviously, with negation we can implement addition-with-carry. I don't recall the exact details but my guess is that a formula implementing sequential addition and then comparing to $n/2$ might have a length polynomial (in fact probably linear) in $n$. However I cannot prove this fact, i.e. this is a gap. (My main worry is that the normal way to implement sequential addition would have "intermediate" variables e.g. the running sum $y_j = \sum_{i=1}^j x_i$, and when we expand each intermediate variable back into original variables the size would blow up.)

Length of $Y$: the function is monotone (which I learned about when I asked this question) which means it has a formula with no negation. One such formula is this function's Disjunctive Normal Form:

$$\bigcup_{\,\,S \subset [n] \\ |S| = n/2} \,\,\,\,\,\, \bigcap_{i \in S} x_i$$

In this case, each clause would be a subset $S$ containing $n/2$ of the variables. There are ${n \choose n/2}$ such subsets which is exponential is $n$. The big gap in my argument is that I do not know that any other formula without negation would also have exponential length. (In fact, I cannot think of any other substantially different way to implement this function without negation.)

Sorry about the gaps... hope this is of interest anyway!