Proof by Cases¶

Version: v3 · 2026-09-28 · History
Prime #: 1590
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomains: Proof Theory, Formal Logic → Mathematics
Also from: Philosophy
Aliases: Proof by exhaustion, Proof by case analysis, Case analysis

Core Idea¶

Proof by cases converts a global claim into local obligations. A declared universe is divided into case conditions whose union covers every admissible possibility; the same proposition is then derived under each condition. Once those conditional derivations and the coverage claim are valid, the temporary case assumptions can be discharged and the proposition follows over the entire universe.

The method is not defined by a small or finite-looking list. Its load-bearing fact is warranted exhaustiveness. Cases may overlap without invalidating the argument, although a true partition often makes bookkeeping cleaner. A few illustrative successes, a large test sample, or a decision tree with an unproved branch does not supply the same warrant. The structure travels from mathematical parity arguments to software verification, legal alternative analysis, and safety reasoning whenever those fields genuinely establish coverage and a branchwise common conclusion.

How would you explain it like I'm…

Check Every Group

Is it true that every kid in your class can have a snack today? Some kids brought a snack, and the teacher brought snacks for everyone who didn't. Every kid is one or the other, and either way they get a snack. That's proof by cases: split everything into groups that cover everyone, then show it's true for each group.

Cover All the Cases

Proof by cases is a way to show something is always true by splitting all the possibilities into groups and showing it's true in each group. For example, to show that a number times the next number (like 4 × 5) is always even, you split into two cases: the first number is even, or it's odd. If it's even, the answer is even; if it's odd, the next number is even, so the answer is even. Since every whole number is either even or odd, you've covered them all. The most important part is making sure your cases really cover every possibility — checking just a few examples isn't enough.

Exhaustive Case Analysis

Proof by cases establishes a general claim by dividing all possibilities into cases that together cover everything, then proving the claim separately in each case. If the cases truly cover every possibility and the claim holds in each, it holds everywhere. For example, to prove n² + n is always even, split into n even and n odd — every integer falls into one of these. The key requirement is exhaustiveness: you must justify that no possibility slips through the cracks. Cases can overlap without breaking the proof, though non-overlapping cases keep things tidier. Testing many examples, or a flowchart with one unchecked branch, is not the same — without proven coverage, there's no guarantee.

Proof by cases converts a global claim into local obligations. A declared universe of possibilities is divided into case conditions whose union covers every admissible possibility; the same proposition is derived under each condition; and, given valid conditional derivations plus a valid coverage claim, the case assumptions are discharged and the proposition holds over the whole universe. In logic this is disjunction elimination: from A ∨ B, A → P, and B → P, infer P. The method is not defined by having a small or finite list of cases — its load-bearing element is warranted exhaustiveness. Cases may overlap without invalidating the argument, though a genuine partition simplifies bookkeeping. A handful of successful examples, a large test sample, or a decision tree with an unproved branch does not supply that warrant. The structure appears in parity arguments in mathematics, exhaustive case analysis in software verification (e.g., total pattern matching), alternative-scenario analysis in law, and safety cases — whenever coverage is genuinely established and every branch reaches the same conclusion.

Structural Signature¶

Recurring features:

proposition — supplies the same conclusion to be established in every branch It is essential. Counterfactual: Different conclusions in different branches do not establish one proposition over the union.
possibility space — declares the universe over which the conclusion is claimed It is essential. Counterfactual: Without a bounded universe, case coverage cannot be assessed.
case conditions — divide the possibility space into locally tractable branches It is essential. Counterfactual: A single undifferentiated argument is not a case proof.
collective exhaustiveness — warrants that no admissible situation lies outside the listed cases It is essential. Counterfactual: Omitting one possible situation leaves the global conclusion unproved.
branchwise derivations — establish the proposition while each case condition is assumed It is essential. Counterfactual: Listing cases without a valid derivation in each is only classification or testing.
case-assumption discharge — lifts the branch conclusions to the entire declared universe It is essential. Counterfactual: Keeping the conclusion conditional on one branch never yields the required universal result.
coverage audit — checks both branch validity and the completeness of the partition It is evidential. Counterfactual: Numerous successful examples do not compensate for an unexamined missing branch.

What It Is Not¶

It is not classification alone; the cases must carry proofs of one proposition.
It is not induction, whose warrant links a base case to successor or structural steps.
It is not sampling or example-based confirmation, however numerous the examples.
It is not brute-force search unless the search space is proved exhaustive and every outcome supports the claimed conclusion.
Closest near-miss. A brute-force check of many inputs is the closest near miss when no warrant shows that the checked inputs exhaust the claimed domain.

Broad Use¶

Mathematics. Parity, sign, residue, interval, and structural cases support global theorems.
Formal logic. A common conclusion is derived from every disjunct.
Software verification. Exhaustive input or state classes generate branch proof obligations.
Decision analysis. Exhaustive factual or hazard scenarios are checked against one governing requirement.

Clarity¶

State the proposition, quantified universe, case predicates, coverage argument, and branch derivations. Say whether cases overlap, how boundary values are assigned, and whether computer enumeration is complete. Many successful trials or a taxonomy without one common conclusion is not a proof by cases.

Manages Complexity¶

The operator replaces one global derivation with a coverage obligation and simpler conditional proofs. It exposes exceptional regimes but can multiply obligations, duplicate arguments, and hide an omitted case. Shared lemmas should reduce repetition without obscuring the exhaustive cover.

Abstract Reasoning¶

Write the exact proposition and its quantifier domain.
Choose case predicates that make the local reasoning simpler.
Prove that every admissible object satisfies at least one case predicate.
Track overlaps or establish disjointness when it matters for bookkeeping.
Derive the identical target proposition under each case assumption.
Discharge all temporary assumptions and infer the target over the full universe.
Audit computational branches, boundary points, and exceptional values for omitted cases.

Knowledge Transfer¶

The reasoning operator transfers literally when another domain can name a universe, provide a warranted exhaustive cover, and establish one conclusion in every branch. The transferable cargo is the coverage-plus-branchwise-proof warrant, not the surface presence of alternatives. Transfer stops at scenario sampling, representative examples, open-ended diagnoses, or policy options whose completeness is only assumed.

Examples¶

Formal/abstract¶

Canonical¶

To prove a statement for every integer, derive it once under n=2k and again under n=2k+1; parity exhausts the integers.

Mapped back: universe → integers; cases → even and odd; conclusion → the same statement in both branches.

Applied/industry¶

Applied / In Practice¶

A list-processing proof treats the empty, singleton, and length-at-least-two shapes separately and proves one postcondition in each branch.

Mapped back: universe → all finite lists; coverage → three exhaustive shape classes; branch evidence → a derivation per class.

Applied / In Practice¶

A program passes a thousand selected tests, but the input space is larger and the sample is not a proven exhaustive partition.

Mapped back: boundary → many checked instances without coverage.

Structural Tensions¶

T1 — Exhaustive Coverage versus Tractable Branch Count. Refining cases can simplify each proof while multiplying the number of obligations and opportunities for omission.

Diagnostic: State the coverage theorem separately and consolidate branches that share the same decisive lemma.

T2 — Mechanical Checking versus Explanatory Insight. A computer can verify thousands of branches while leaving the reason for the common conclusion hard to see.

Diagnostic: Distinguish the correctness certificate from the higher-level explanation or invariant.

Seen in practice: Case checking in tension with a shared explanation

Structural–Framed Character¶

Proof by Cases sits at the structural end of the structural–framed spectrum. Its identity rests on dividing a declared universe into case conditions whose union covers every admissible possibility and deriving the same proposition under each, so the conclusion follows over the whole universe.

Its vocabulary of proposition, possibility space, cases, and exhaustiveness is generic and keeps one meaning across fields. It is evaluatively neutral: a valid case proof establishes a result without commending it. Its origin is formal logic and mathematics rather than any institution, and it can be defined without human practice. Applying it recognizes the same coverage and branchwise derivation wherever warranted exhaustiveness is present, rather than importing a perspective. A parity argument that treats even and odd integers separately, a software verification that covers every branch of an input space, and a safety analysis that establishes the same conclusion for each possible situation all fit, whereas a large test sample without a coverage warrant does not. On every diagnostic, it reads structural.

Substrate Independence¶

Substrate independence lies in a repeated relation: one target claim, an exhaustive cover of its domain, and a valid conditional derivation on each member. Integers, program states, legal findings, and hazard scenarios can all fill those roles. The prime does not require mathematical notation, finite enumeration, or any particular subject matter. The reasoning operator transfers literally when another domain can name a universe, provide a warranted exhaustive cover, and establish one conclusion in every branch. The transferable cargo is the coverage-plus-branchwise-proof warrant, not the surface presence of alternatives. Transfer stops at scenario sampling, representative examples, open-ended diagnoses, or policy options whose completeness is only assumed.

Relationships to Other Abstractions¶

Current abstraction Proof by Cases Prime

Parents (1) — more general patterns this builds on

Proof by Cases is part of Partition Prime

Proof by Cases contains a Partition because its case conditions must be collectively exhaustive over the admissible universe before local derivations license the global conclusion.

Hierarchy path (1) — routes to 1 parentless root

Proof by Cases → Partition → Set and Membership

Neighborhood in Abstraction Space¶

Proof by Cases sits among the more crowded primes in the catalog (33^rd percentile for distinctiveness): several abstractions describe nearly the same structure, so a description that fits it will tend to fit its neighbors too — transporting it usually means disambiguating within this family rather than landing on it exactly.

Family — Unclustered & Miscellaneous (481 primes)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With¶

Partition. Tell: Does the division support a proof of one proposition in every block, or merely organize objects?
Mathematical induction. Tell: Is the warrant exhaustive parallel cases, or preservation along a successor or structural relation?
Disjunction elimination. Tell: Is the reference the general reasoning pattern across representations, or the specific formal rule in a logical calculus?
Testing. Tell: Has every admissible input been covered with proof-level warrant, rather than sampled empirically?

Solution Archetypes¶

No catalogued solution archetypes reference this prime yet.

References¶

Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Proof_by_exhaustion (revision 1368627298).
Preserved source candidate: https://www.m-a.org.uk/resources/2017-Sep-Proof-Glaisters-MiS.pdf
Preserved source candidate: https://www.ebsco.com/
Preserved source candidate: https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Gentle_Introduction_to_the_Art_of_Mathematics_(Fields)/03%3A_Proof_Techniques_I/3.05%3A_Even_More_Direct_Proofs-_By_Cases_and_By_Exhaustion

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.