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.