Proof by Contradiction

I spent one morning at the JMMs this week in a session on the Introduction-To-Proofs course (aka the Bridge course). I enjoyed the session; it contained some good techniques to include, some good warnings of things to avoid, etc. Such a course always includes learning about proof by contradiction.

Now, I have a bit of a thing about proof by contradiction. It's not that it's invalid; it's that, at least in classical logic, you can always transform a proof by contradiction into a proof by contraposition; in any case, while I'm not a constructivist and think that intuitionistic logic is mostly a curiosity, it's nice to have a proof which provides an implicit algorithm, when such a thing exists.

So today on the train I was puzzling over a little bit of boolean-algebra arithmetic which Tom Jech uses in his exposition of forcing. (I'm supervising an undergrad who wants to learn forcing, and the boolean-valued-model approach is so much nicer than the poset-only approach.) I tried to prove it forwards six ways to Sunday, and nothing seemed to work. So, remembering what we all tell students in Bridge courses, I turned it around and tried to prove it by contradiction, and that took all of six lines. I still don't see a direct proof that's not an artificial translation of the contradiction/contraposition result; if you know one, put it in the comments!

Theorem: Recall that in boolean algebras, the implication operation $v_1 \Rightarrow v_2$ is defined as $v_2 \lor \neg v_1$. If $x,y,z$ belong to a boolean algebra $\mathbf{B}$ and $x \land y = x \land z$, then $x \leq ( y \Leftrightarrow z)$.

Proof: Suppose otherwise. Then we can find elements $x, y, z$ in a boolean algebra $\mathbf{B}$ so that
$$x > y \Rightarrow z = x \land ( z \lor (\neg y))$$
Now observe that
$$x \land ( z \lor (\neg y)) = (x \land z) \lor (x \land \neg y) = (x \land z) \lor (x \land y) \lor (x \land \neg y) = (x \land z) \lor x \geq x$$
Overall, $x > x$, a contradiction.