3.1 Direct Proof, Contrapositive, and Case Analysis: Building Verifiable Reasoning Chains

In code reviews, a statement like "this can't be null" isn't a proof. To make that conclusion checkable by others, you must specify the scope of the object, the known premises, and the basis for each step, whether it follows from a definition, a theorem, or a prior assumption.

The value of a proof isn't in writing it like a math paper. It explains why the conclusion follows, with steps that others can inspect, challenge, and reuse.

Write the Statement Completely

A theorem typically consists of quantifiers, premises, and a conclusion:

For any integer n, if n is even, then n² is even.

Formally expressed as:

∀n∈ℤ (Even(n) → Even(n²))

When beginning a proof, you must fix an arbitrary object that satisfies the premise, rather than picking a convenient example:

Let n ∈ ℤ be arbitrary, and assume n is even.

Since n has no additional special properties, any conclusion derived from it applies to all even integers.

Direct Proof: Expand Definitions and Move Toward the Goal

Even number definition:

Even(n) ⇔ ∃k∈ℤ, n=2k

Thus:

Let n = 2k, where k ∈ ℤ.
n² = (2k)² = 4k² = 2(2k²).
Since 2k² ∈ ℤ, n² is even.

Every step in this proof traces back to a source: the definition of even numbers, algebraic operations, and the closure of integers under multiplication. The final statement must restate the conclusion in the form of the target definition, rather than stop at “obvious.”

General template for direct proof:

1. Pick an object from within the scope of the quantifier;
2. Assume the premise;
3. Expand relevant definitions;
4. Apply known facts to transform the expression step by step;
5. Reach the conclusion in the form of the target definition.

Contrapositive Proof: A Different Equivalent Direction

Statement: If p → q, then its contrapositive is:

¬q → ¬p

The two statements are logically equivalent. If it's difficult to directly derive q from p, we can instead prove the contrapositive.

Theorem: For an integer n, if n² is even, then n is even.

Contrapositive: If n is not even (that is, n is odd) then n² is odd.

Let n = 2k + 1, where k ∈ ℤ.
n² = (2k + 1)² = 4k² + 4k + 1 = 2(2k² + 2k) + 1.
Thus, n² is odd.

Contrapositive proof differs from proof by contradiction. Contrapositive proof directly establishes an equivalent implication; proof by contradiction assumes the negation of the conclusion and derives a contradiction.

It's also important to distinguish:

Original statement: p → q
Converse: q → p
Inverse: ¬p → ¬q
Contrapositive: ¬q → ¬p

The original statement is equivalent to its contrapositive, and the converse is equivalent to the inverse. The two pairs are not generally equivalent: with p=F,q=T, the original and contrapositive are true while the other two are false. “Successful login requires a token” does not imply that a token guarantees successful login.

Case Analysis: Covering All Possibilities

If an object naturally divides into a finite and mutually exclusive set of cases, then each case can be proven separately.

Theorem: For any integer n, n(n+1) is even.

The integer n is either even or odd:

• If n is even, then the product contains an even factor n;
• If n is odd, then n+1 is even, and the product contains an even factor n+1.

Two cases cover all integers, so the conclusion holds.

Proof by cases has two obligations:

1. The cases collectively cover all possibilities;
2. The conclusion holds in each case.

Scenarios don't have to be mutually exclusive, but exclusivity usually makes proofs clearer. Overlap does not invalidate the proof, though it may duplicate work.

Software cases often come from state enumerations, input symbols, tree node types, or protocol messages. A default branch may handle a new state syntactically while the old proof says nothing about its required behavior. Recheck the argument when states are added; having a branch to execute does not establish proof coverage.

Prove Both Directions

To prove p ↔ q, it is necessary to prove both:

p → q
q → p

Theorem: An integer n is even if and only if n² is even.

• The forward direction has already been established by direct proof;
• The reverse direction can be proven using contrapositive reasoning.

Proving only one direction is a common flaw in specification reviews. "Data is valid when a cache hit occurs" does not imply "a cache hit must occur when data is valid."

Set Equality Is Proven by Bidirectional Inclusion

Proof:

A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)

This equality can be proven via bidirectional inclusion, or directly by considering an arbitrary element and establishing an equivalence chain:

x ∈ A ∩ (B ∪ C)
⇔ x ∈ A ∧ (x ∈ B ∨ x ∈ C)
⇔ (x ∈ A ∧ x ∈ B) ∨ (x ∈ A ∧ x ∈ C)
⇔ x ∈ (A ∩ B) ∪ (A ∩ C)

The middle step applies the distributive law of propositional logic. A well-written proof clearly labels key transformations, rather than leaving readers to guess them.

The Minimum Standards for Proof Writing

• Quantifier scope is clearly defined;
• New variables must be introduced with their type and source;
• When using a definition, include the key expansion;
• When referencing a prior theorem, state its name;
• Do not substitute a few examples for a full universal proof;
• The conclusion must explicitly align with the original goal.

Formal notation should not be used merely for complexity. If natural language can clearly express a step, there's no need to symbolize every connecting word. However, any point that could alter scope, conditions, or the order of quantifiers must be expressed with precision.

Completion Check

1. Direct proof: The sum of two even numbers is even.
2. Contrapositive proof: If ab is odd, then both a and b are odd.
3. Case-based proof: The remainder when the square of any integer is divided by 4 is either 0 or 1.
4. Prove both directions separately: A⊆B if and only if A∩B=A.
5. Identify a real API constraint and write it such that only one direction holds, yet it is easily misread as a bidirectional condition.

References

• Open Logic Project