Of monotone formulas and same ones satisfying certain properties There is the following theoretical computer science, namely:


  For a particular monotone formula $M$ of size $n$, there's an equivalent formula of depth $\text{O}(\text{ln}\,n)$.


(I am reading the original paper in my library, if I have time later I will scan it and add scans of it to this post. My apologies for being unable to find a copy online.)

However, I'm finding myself going from step to step in the proof without really understanding what's going on, lacking intuition, as the paper is quite short and condensing quite a bit of reasoning and motivation, at least I feel. I was wondering if somebody could offer me their explanation of the proof of this result, hopefully with lots of their intuition thrown in so I and others reading can have a greater understanding of a proof?
Spira's result uses the technique of formula balancing. For simplicity, I describe the non-monotone case, the monotone case being similar.

Let $\phi$ be a formula of size $n$. We can think of $\phi$ as a binary tree. In general, $\phi$ need not be balanced. It is not hard to show that $\phi$ always has a vertex $\psi$ corresponding to a subformula of size between $n/3$ and $2n/3$ (proof: descend from the root until you reach a subformula of size smaller than $2n/3$). Replace $\psi$ with a new formal variable $x$. The original formula is equivalent to the formula
$$
(\psi \land \phi|_{x=1}) \lor (\lnot \psi \land \phi|_{x=0}).
$$
(If $\phi$ is monotone, we don't need $\lnot \psi$.) What have we accomplished? At the cost of slightly increasing the size of the formula, we managed to get the two top levels of the formula balanced: the subformulas at depth 2 all have size between $n/3$ and $2n/3$.

We continue this process recursively with all the subformulas at depth 2. The process stops after $O(\log n)$ steps, since the subformulas at depth 2 decrease at a constant rate. Hence the final formula has depth $O(\log n)$, and so size $n^{O(1)}$. At the cost of polynomially increasing the size, we have ensured that it is balanced.