“A mathematical proof should resemble a simple and clear-cut constellation, not a scattered cluster in the Milky Way.” - G. H. Hardy
Although there are many ways to structure proofs, the “default” (and most common) approach is to have the structure of the proof exactly match the structure of the formula being proved. In this section, we consider common patterns for proofs of formulas involving implications and equivalences. ## Proving Implications
By far the most common way to prove an assertion of the form \(A\to B\) is to present a proof that starts by assuming \(A\) is true and then use step-by-step reasoning to conclude that \(B\) must be true as well (akin to the \(\to I\) rule of Natural Deducation). Exact wording (e.g., the way introduce \(A\) as an assumption, or the choice of connecting words like “then”, “thus”, and “so”) can vary.
Example
Theorem: \(A\to B\) > >Proof: Assume \(A\). >⋮ >Thus, \(B\). > >— > >Theorem: \(A\to B\) > >Proof: Suppose \(A\). >⋮ >and so \(B\). ### Proof by Contraposition
Another strategy to prove a statement of the form \(A\to B\) is to give a direct proof of the logically equivalent contrapositive \(\lnot B\to \lnot A\). In this case, it is polite to leave a note to warn the reader that this is not the usual “assume \(A\) and then prove \(B\)” proof.
Example
Theorem: \(A\to B\)
Proof (by contraposition): Suppose \(\lnot B\). ⋮ Therefore, \(\lnot A\)
Theorem: \(A\to B\)
Proof: We show the contrapositive. Assume \(\lnot B\). ⋮ and then \(\lnot A\)
Since we officially defined \(A\leftrightarrow B\) as an abbreviation for \((A\to B)\land(B\to A)\), it suffices to verify both implications. Each can be done either directly or by checking the contrapositive.
Example
Theorem: \(A\leftrightarrow B\)
Proof: \((\to)\) Assume \(A\). ⋮ Thus \(B\).
\((\leftarrow)\) Assume \(B\). ⋮ Thus \(A\).
Theorem: \(A\leftrightarrow B\)
Proof: Assume \(A\). ⋮ Thus \(B\).
Conversely, assume \(\lnot A\). ⋮ Thus \(\lnot B\).
Just be careful that we you don’t try to prove an equivalence by showing \(A\to B\) and its contrapositive \(\lnot B\to \lnot A\)! That would check one direction twice, without verifying the other direction at all.
Previous: 3.3 Bounded Quantifiers