DISCRETE MATH • LOGIC AND PROOF

Proof by Cases

Divide a proposition into exhaustive subcases and conquer each one to establish universal truth.

Historical Context & Motivation

The strategy of splitting a problem into distinct scenarios and reasoning about each one independently is among the oldest logical maneuvers in mathematics. Ancient Greek geometers routinely divided geometric constructions into separate configurations—positive angle versus negative, acute versus obtuse—long before modern proof methodology was codified. Proof by cases (sometimes called proof by exhaustion when the cases are finite and enumerated) formalises this intuition: if a universe of discourse can be partitioned into subcases that together cover every possibility, and the desired conclusion holds in each subcase, then it holds universally.

Historically, this technique has appeared in number-theoretic arguments (Euclid's classification of primes and composites), in algebra (analysis of polynomial roots by sign), and in modern computer science (verifying program correctness over different input classes). Its logical foundation rests on the tautology of constructive dilemma: if P₁ ∨ P₂ ∨ … ∨ Pₙ is true and each Pᵢ → Q, then Q follows. Below is a brief timeline showing how case analysis matured from informal reasoning into a rigorous proof strategy.

~300 BCE
Euclid's Elements
Euclid employs case distinctions throughout the Elements, dividing geometric propositions by whether a point lies inside, on, or outside a circle—an early exhaustive case analysis.
1637
Fermat's Descent Arguments
Pierre de Fermat uses case splits based on residue classes modulo small primes to prove results in number theory, notably his method of infinite descent which relies on partitioning integers by divisibility.
1879
Frege's Begriffsschrift
Gottlob Frege formalises propositional logic, giving proof by cases an explicit logical foundation via the disjunction elimination rule in a formal deductive system.
1976
Four Color Theorem
Appel and Haken prove the Four Color Theorem by reducing it to 1,936 cases verified by computer—the most famous large-scale proof by exhaustion in mathematics.
2005
Formal Verification Era
Proof assistants like Coq and Isabelle/HOL mechanise case analysis, enabling machine-checked proofs that systematically enumerate and verify thousands of subcases in software and hardware verification.

The central question proof by cases answers is deceptively simple: when a direct or contrapositive argument is not forthcoming, can we still prove a statement by ensuring every possible scenario leads to the same conclusion? The answer, grounded in the logical completeness of an exhaustive partition, is a resounding yes—provided the partition truly covers every case.

Core Principles & Definitions

A proof by cases succeeds when three conditions are met: the cases must be exhaustive (they cover every element in the domain), each case must independently imply the conclusion, and the logic connecting them must be valid. The cases need not be mutually exclusive—overlap is harmless—but missing even one scenario invalidates the proof entirely. The following concept cards formalise these ideas.

1

Exhaustive Partition

The disjunction P₁ ∨ P₂ ∨ … ∨ Pₙ must be a tautology relative to the domain. Every element, value, or scenario must fall into at least one case. For example, partitioning integers as even or odd is exhaustive; partitioning by 'divisible by 3' alone is not.
2

Case Implication

Within each case Pᵢ, you must prove Pᵢ → Q using any valid proof technique—direct proof, contradiction, contrapositive, or even nested case analysis. The key is that Q is the same conclusion in every case.
3

Disjunction Elimination

The logical backbone is the rule: from (P₁ ∨ P₂ ∨ … ∨ Pₙ), (P₁ → Q), (P₂ → Q), …, (Pₙ → Q), conclude Q. This is valid in classical, intuitionistic, and constructive logics alike.
4

Without Loss of Generality (WLOG)

When cases are symmetric, we may prove only one and invoke symmetry for the rest. The phrase 'without loss of generality' signals that a symmetry argument reduces the number of cases. This must always be justified, not merely asserted.
KEY TAKEAWAY
Think of proof by cases like a security team clearing a building: they divide the structure into zones, search each zone independently, and once every zone is confirmed safe, the entire building is declared secure. If a single zone is left unchecked, the conclusion fails—the partition must be exhaustive. Similarly, if even one zone reveals a threat (a case where the conclusion doesn't hold), the universal claim collapses.

Visual Explanation

The diagram below illustrates the logical architecture of a proof by cases. The domain of discourse (represented by the large outer rectangle) is partitioned into subcases. Each subcase independently implies the conclusion Q. The disjunction elimination rule then combines these partial results into the final conclusion.

Each colored box represents an individual case (P₁, P₂, …, Pₖ). The dashed amber box confirms that the cases are exhaustive. Arrows converge at the green conclusion box, which is reached via disjunction elimination.

Notice that the arrows from each case box to the exhaustive-check layer are independent: the proof within Case 1 need not reference the argument in Case 2. This modularity is one of the technique's great strengths. Each subproof can employ a different method—direct reasoning in one case, contradiction in another—yet the overall structure remains unified by the disjunction elimination step at the bottom.

Mathematical Framework

The logical validity of proof by cases rests on a well-known tautology in propositional logic. We formalise the technique below, starting with the two-case version and generalising to an arbitrary finite number of cases.

TWO-CASE VERSION
[(P₁ ∨ P₂) ∧ (P₁ → Q) ∧ (P₂ → Q)] → Q
P₁, P₂ are the two cases (their disjunction must be a tautology over the domain). Q is the conclusion to be established. This is the constructive dilemma in classical logic.
GENERAL k-CASE VERSION
[(P₁ ∨ P₂ ∨ … ∨ Pₖ) ∧ ⋀ᵢ(Pᵢ → Q)] → Q
Here ⋀ᵢ denotes the conjunction over all i from 1 to k. The disjunction P₁ ∨ … ∨ Pₖ must evaluate to true for every element under consideration—this is the exhaustiveness requirement.

In natural deduction systems, the corresponding inference rule is typically called ∨-elimination (or disjunction elimination). Given a proof of P₁ ∨ P₂, together with a subproof deriving Q from the assumption P₁ and a subproof deriving Q from the assumption P₂, one may discharge both assumptions and conclude Q. The rule extends straightforwardly to any finite disjunction by iterated application.

PROOF TEMPLATE (SCHEMATIC)
Goal: ∀x ∈ D, R(x). Split: D = D₁ ∪ D₂ ∪ … ∪ Dₖ. Prove: x ∈ Dᵢ ⟹ R(x) for each i.
D is the domain, Dᵢ are the subsets forming the partition (or cover), and R(x) is the property to be proved. The union D₁ ∪ … ∪ Dₖ = D ensures exhaustiveness.
Overlap is Harmless
The cases need not be mutually exclusive. If some element x belongs to both D₁ and D₂, the conclusion R(x) is proved by Case 1 alone (or by Case 2 alone)—no contradiction arises. However, gaps are fatal: if some x belongs to no Dᵢ, the proof fails.

Common Case-Splitting Strategies

Choosing the right partition is an art as much as a science. The most effective case splits exploit the algebraic or structural properties of the objects involved, reducing a complex universal statement to manageable subclaims. Below is a classification of the most frequently encountered case-splitting strategies in discrete mathematics and adjacent fields.

Five canonical strategies for case-splitting. Parity and modular residues are especially common in number theory, while structural splits dominate graph theory and algebra.

When selecting a splitting strategy, the guiding heuristic is to choose cases that simplify the algebraic or logical structure of the proposition. For instance, splitting an integer n by parity lets you write n = 2k or n = 2k + 1, converting an arbitrary integer into a linear function of k—an enormous simplification when the conclusion involves n². Similarly, modular residue classes modulo 3 are ideal when the conclusion involves n³ or divisibility by 3, because cubing a residue class produces predictable remainders.

💡 When to Use Proof by Cases
Proof by cases is most useful when: (1) a hypothesis is explicitly a disjunction (e.g., 'x is rational or x is irrational'); (2) an absolute value or piecewise-defined function creates natural branches; (3) a direct proof for the general case is obstructed but the specialised subcases yield to direct argument; or (4) a classification theorem partitions objects into types.

Worked Example

We now apply proof by cases to a classic number-theoretic statement. The result is elementary but perfectly illustrates the technique's mechanics, including the choice of cases, the independent subproofs, and the final assembly.

Theorem: For every integer n, n² + n is even.

Proof by Cases — n² + n Is Even
1
Step 1 — Identify the Goal and DomainWe wish to prove that for every integer n, the expression n² + n is even. Equivalently, we must show that 2 divides n² + n. Observe that n² + n = n(n + 1), but we shall proceed via case analysis on the parity of n to demonstrate the technique explicitly.
2
Step 2 — Choose an Exhaustive PartitionEvery integer is either even or odd. This gives us two cases:
Case 1: n is even | Case 2: n is odd
3
Step 3 — Prove Case 1 (n is even)Assume n is even, so n = 2k for some integer k. Then n² + n = (2k)² + 2k = 4k² + 2k = 2(2k² + k). Since 2k² + k is an integer, n² + n is divisible by 2.
n² + n = 2(2k² + k) is even. ✓
4
Step 4 — Prove Case 2 (n is odd)Assume n is odd, so n = 2k + 1 for some integer k. Then n² + n = (2k + 1)² + (2k + 1) = 4k² + 4k + 1 + 2k + 1 = 4k² + 6k + 2 = 2(2k² + 3k + 1). Since 2k² + 3k + 1 is an integer, n² + n is divisible by 2.
n² + n = 2(2k² + 3k + 1) is even. ✓
5
Step 5 — Conclude by Disjunction EliminationSince every integer is either even or odd (the cases are exhaustive), and in both cases n² + n is even, we conclude that n² + n is even for all integers n.
∴ For every integer n, n² + n is even. □
📝 Observation
A slicker proof factors n² + n = n(n + 1), noting that consecutive integers always include one even factor. Proof by cases achieves the same result more mechanically. In practice, the elegance of the factorisation is preferable, but the case-analysis approach generalises to situations where no clean factorisation exists.

Strengths, Limitations & Comparisons

Proof by cases is a versatile but not universally optimal strategy. Understanding when it excels and when other techniques are superior is crucial for effective mathematical writing. The table below contrasts proof by cases with other major proof methods.

Comparison of proof by cases with direct proof and proof by contradiction
CriterionProof by CasesDirect ProofProof by Contradiction
When to useDomain splits naturally into subcases; hypothesis is a disjunction; piecewise-defined functionsHypothesis leads naturally to conclusion via a chain of implicationsNegation of conclusion yields useful information; existence/uniqueness results
StrengthsModular; each case is simpler than the whole; tolerates asymmetric structuresMost transparent and intuitive; preferred when availablePowerful for impossibility results; works when constructive path is unclear
LimitationsCan produce lengthy proofs; must verify exhaustiveness; less insightful if many casesNot always available; requires a clear implication chainNon-constructive; may feel indirect; harder to extract computational content
Typical # of stepsProportional to k (number of cases) × subproof lengthUsually shortest when applicableVariable; may involve deep auxiliary reasoning
Common pitfallNon-exhaustive partition (missing a case)Unjustified leap in the implication chainAssuming what you want to prove (circular reasoning)
KEY TAKEAWAY
Proof by cases is like a doctor running a differential diagnosis: when a single test cannot pinpoint the answer, you enumerate the possible conditions, rule each one in or out independently, and the combination of all sub-analyses yields the definitive conclusion. The method is reliable but sometimes expensive—if a single elegant test (direct proof) is available, it is usually preferable. But when the domain resists a unified approach, case analysis is the mathematically guaranteed fallback.

Connection to Advanced Theory

Proof by cases, though elementary in concept, connects deeply to several areas of advanced mathematics and theoretical computer science. The table below maps its relationship to more sophisticated proof paradigms.

From proof by cases to advanced techniques
Proof by Cases (This Lesson)Advanced Extension
Finitely many cases, each proved by handComputer-assisted proof by exhaustion: thousands of cases verified algorithmically (e.g., Four Color Theorem, Kepler Conjecture)
Case split on integers (parity, mod m)Structural induction: case analysis on recursive data structures (trees, lists, formulas) combined with an inductive hypothesis
Disjunction elimination in propositional logicPattern matching in type theory: in Curry–Howard correspondence, case analysis on a sum type A + B mirrors disjunction elimination
WLOG (symmetry reduction)Group actions and Burnside's lemma: symmetry groups formally reduce the number of distinct cases in combinatorial enumeration
Exhaustive verification over a finite domainModel checking: automated exhaustive state-space exploration in hardware/software verification

In courses on automata theory and programming languages, you will encounter structural induction as the natural marriage of case analysis with mathematical induction: the base cases of an inductive proof are themselves a case split, and the inductive step often requires further sub-case analysis on the form of a recursive structure. Mastery of proof by cases is therefore foundational—it is the atomic operation from which more complex proof architectures are assembled.

🔭 Looking Ahead
If you continue to courses in formal methods or type theory, you will see proof by cases reappear as case expressions and match statements in functional programming languages (Haskell, OCaml, Coq). The compiler's exhaustiveness checker is precisely the formal analogue of verifying that your cases cover the entire domain.

Practice Problems

The following five problems progress from conceptual understanding to critical analysis. Attempt each problem before reading the answer; active struggle is the primary mechanism by which proof technique becomes internalised.

PROBLEM 1CONCEPTUAL
A student claims to prove that every real number x satisfies |x| ≥ 0 by considering two cases: x > 0 and x < 0. Is this proof by cases valid? If not, identify the flaw.
PROBLEM 2BASIC CALCULATION
Prove by cases that for every integer n, 3 divides n³ − n.
PROBLEM 3INTERMEDIATE
Prove: for all integers m and n, if mn is even, then m is even or n is even. (Hint: use proof by cases on the parity of m.)
PROBLEM 4APPLIED
A program receives an integer input n and must compute f(n) = n² − 1. A programmer claims the output is always non-negative for |n| ≥ 1. Prove this claim using proof by cases, splitting on the sign of n.
PROBLEM 5CRITICAL THINKING
Prove or disprove: for every integer n, the expression n⁴ − n² is divisible by 12. If it is true, construct a proof by cases using an appropriate modular partition. If false, provide a counterexample and determine the largest integer that always divides n⁴ − n².

Lesson Summary

Proof by cases is a proof technique in which the domain of discourse is partitioned into an exhaustive set of subcases, and the desired conclusion is established independently within each subcase. Its logical foundation is the disjunction elimination rule: given P₁ ∨ P₂ ∨ … ∨ Pₖ and proofs that each Pᵢ → Q, one concludes Q. The cases may overlap without harm, but non-exhaustive partitions invalidate the proof. Common splitting strategies include parity, modular residues, sign/ordering, and structural type analysis.

While proof by cases can produce longer proofs than a direct argument, it offers modularity (each subcase is self-contained), flexibility (different proof techniques may be used in different cases), and is the foundational mechanism behind structural induction, computer-assisted proofs by exhaustion, and pattern matching in type theory. Mastering this technique equips you with a reliable strategy for any proposition that resists a single unified argument.

Varsity Tutors • Discrete Math • Proof by Cases