Proof Techniques Toolkit: The Methods Behind Every Theorem

Terminology

What & Why

Every theorem in mathematics and computer science rests on a proof, and every proof uses one or more standard techniques. Mastering these techniques is like learning the basic moves in chess: you cannot play the game without them. This post covers the core toolkit that appears in algorithm correctness proofs, complexity lower bounds, impossibility results, and formal verification.

Direct proof is the most straightforward: assume the hypothesis, derive the conclusion. Proof by contradiction assumes the opposite and finds an absurdity. The contrapositive flips the implication. Induction handles statements about all natural numbers (or all recursive structures). Well-ordering provides an alternative to induction. Constructive proofs build the object; non-constructive proofs merely show it must exist.

For programmers, these are not abstract exercises. Proving a loop terminates is induction. Proving a sorting algorithm is correct uses loop invariants (induction in disguise). Proving the halting problem is undecidable uses contradiction. Proving a lower bound on comparison sorting uses a counting argument. Every correctness proof, every complexity result, and every impossibility theorem uses these tools.

How It Works

1. Direct Proof

To prove P \implies Q: assume P is true, then show Q follows.

Example: "If n is even, then n^2 is even." Assume n = 2k. Then n^2 = 4k^2 = 2(2k^2), which is even.

2. Proof by Contradiction

To prove P: assume \neg P, then derive a contradiction.

Example: "There is no largest prime." Assume there is a largest prime p_k. Construct N = p_1 \cdot p_2 \cdots p_k + 1. No p_i divides N, so N has a prime factor larger than p_k. Contradiction.

3. Proof by Contrapositive

To prove P \implies Q: prove \neg Q \implies \neg P instead (logically equivalent).

Example: "If n^2 is odd, then n is odd." Contrapositive: "If n is even, then n^2 is even." This is easier to prove directly (shown above).

4. Mathematical Induction

To prove P(n) for all n \geq 0:

1. Base case: prove P(0).
2. Inductive step: assume P(k) (the inductive hypothesis), prove P(k+1).

Example: prove \sum_{i=0}^{n} i = \frac{n(n+1)}{2}. Base: \sum_{i=0}^{0} i = 0 = \frac{0 \cdot 1}{2}. Check. Step: assume \sum_{i=0}^{k} i = \frac{k(k+1)}{2}. Then \sum_{i=0}^{k+1} i = \frac{k(k+1)}{2} + (k+1) = \frac{(k+1)(k+2)}{2}. Check.

5. Strong Induction

Like weak induction, but the inductive step assumes P(0), P(1), \ldots, P(k) are all true to prove P(k+1). Useful when P(k+1) depends on cases earlier than P(k).

Example: every integer n \geq 2 has a prime factorization. Base: P(2) is true (2 is prime). Step: assume all integers from 2 to k have prime factorizations. For k+1: if k+1 is prime, done. If not, k+1 = a \cdot b where 2 \leq a, b \leq k. By the inductive hypothesis, a and b have prime factorizations, so k+1 does too.

6. Well-Ordering Principle

Every non-empty set of natural numbers has a smallest element. This is equivalent to induction and sometimes gives cleaner proofs.

7. Constructive vs Non-Constructive

A constructive proof exhibits the object. A non-constructive proof shows existence without construction. Euclid's proof of infinite primes is constructive (it builds a new prime). The proof that there exist two irrational numbers a, b such that a^b is rational is famously non-constructive: consider \sqrt{2}^{\sqrt{2}}. If it is rational, we are done (a = b = \sqrt{2}). If it is irrational, then (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^2 = 2, which is rational. Either way, such a, b exist, but we do not know which case holds.

Complexity Analysis

Induction on algorithm correctness typically mirrors the recursion structure:

The proof that this recurrence solves to O(n \log n) uses strong induction: assume the bound holds for all inputs smaller than n, then show it holds for n.

Implementation

ALGORITHM ProveByInduction(baseCase, inductiveStep, n)
INPUT: baseCase: proof that P(0) holds
       inductiveStep: proof that P(k) implies P(k+1)
       n: the target value
OUTPUT: proof that P(n) holds
BEGIN
  // Verify base case
  ASSERT baseCase proves P(0)

  // Chain the inductive step n times
  FOR k FROM 0 TO n - 1 DO
    // We know P(k) holds (from base case or previous step)
    // Apply inductive step to get P(k+1)
    APPLY inductiveStep TO GET P(k+1) FROM P(k)
  END FOR

  RETURN "P(n) proved"
END

ALGORITHM LoopInvariantProof(loop, invariant, precondition, postcondition)
INPUT: loop: a while loop with condition C and body B
       invariant: property I that should hold at each iteration
       precondition: what is true before the loop
       postcondition: what should be true after the loop
OUTPUT: proof of correctness
BEGIN
  // 1. Initialization (base case): show invariant holds before loop
  ASSERT precondition IMPLIES invariant

  // 2. Maintenance (inductive step): show invariant is preserved
  // Assume I holds and C is true at start of iteration
  // Show I holds after executing body B
  ASSERT (invariant AND C) AFTER_EXECUTING(B) IMPLIES invariant

  // 3. Termination: show loop eventually exits
  // Identify a variant (decreasing quantity bounded below)
  ASSERT variant DECREASES each iteration AND variant >= 0

  // 4. Postcondition: show invariant AND NOT C implies postcondition
  ASSERT (invariant AND NOT C) IMPLIES postcondition

  RETURN "Loop correctness proved by induction"
END

ALGORITHM ProveByContradiction(statement)
INPUT: statement: the proposition P to prove
OUTPUT: proof of P
BEGIN
  ASSUME NOT P

  // Derive logical consequences of NOT P
  consequences <- DERIVE_FROM(NOT P)

  // Find a contradiction: some Q and NOT Q both follow
  IF EXISTS Q IN consequences SUCH THAT (NOT Q) IN consequences THEN
    // Contradiction found
    RETURN "NOT P leads to contradiction, therefore P is true"
  END IF
END

ALGORITHM StrongInductionProof(property, baseValues, n)
INPUT: property: P(n) to prove for all n >= 0
       baseValues: set of base cases to verify
       n: target value
OUTPUT: proof that P(n) holds
BEGIN
  // Verify all base cases
  FOR EACH b IN baseValues DO
    ASSERT property(b) is true
  END FOR

  // Strong inductive step: assume P(0)..P(k) all hold
  FOR k FROM MAX(baseValues) + 1 TO n DO
    // The inductive hypothesis: P(j) for all j < k
    // Use ANY of P(0), P(1), ..., P(k-1) to prove P(k)
    ASSERT CAN_PROVE property(k) USING {property(j) : j < k}
  END FOR

  RETURN "P(n) proved by strong induction"
END

Real-World Applications

• Loop invariant proofs (induction) are the standard method for verifying algorithm correctness in formal methods and software verification tools like Dafny and SPARK
• Proof by contradiction establishes impossibility results throughout CS: the halting problem, Rice's theorem, lower bounds on comparison sorting ($\Omega(n \log n)$), and the CAP theorem
• Structural induction (induction on recursive data structures) proves properties of programs that operate on trees, lists, and other recursive types
• Constructive proofs in type theory (Curry-Howard correspondence) equate proofs with programs: a constructive proof of existence is literally an algorithm that computes the witness
• Proof assistants (Coq, Lean, Isabelle) require users to apply these techniques explicitly, making proof technique mastery essential for formal verification
• The well-ordering principle proves termination of algorithms: if a non-negative integer quantity strictly decreases each iteration, the loop must terminate

Key Takeaways

• Direct proof, contradiction, contrapositive, induction, well-ordering, and constructive/non-constructive proofs form the core toolkit for all mathematical and CS proofs
• Proof by contradiction assumes the negation and derives absurdity; it is the technique behind the halting problem, irrationality of $\sqrt{2}$, and infinite primes
• Mathematical induction proves statements for all natural numbers via a base case and an inductive step; it is the foundation of loop invariant proofs in algorithm verification
• Strong induction allows the inductive step to use all previous cases, not just the immediately preceding one; essential for recursive algorithm correctness
• Constructive proofs build the claimed object explicitly, while non-constructive proofs show existence without construction; in CS, constructive proofs correspond to algorithms
• Every algorithm correctness proof, complexity lower bound, and impossibility result in computer science uses one or more of these techniques