Skip to content

Case Against Cases

April 22, 2015


How to avoid too many cases at least some of the time

Unknown

Theon of Alexandria was history’s main editor of Euclid’s Elements.

Today I want to talk about case analysis proofs.

The connection is that Euclid is sometimes credited with inventing case analysis proofs. He can also be credited as the first to evince a desire to avoid them. Euclid made a habit of giving just one case and leaving the reader to imitate his proof for others. One example is the theorem that given a triangle {ABC} with apex {C}, every other point {D} on the same side of the base {AB} as {C} makes either {|AD| \neq |AC|} or {|BD| \neq |BC|}. Euclid gives a proof only for the case where {D} is outside the triangle. In other cases {D} could be inside the triangle or incident to one of its edges.

Theon lived from 335 to 405 CE in Euclid’s town of Alexandria. He was the last Director of the Library of Alexandria before its final destruction by fire toward the end of the 4th century. It is possible that he directed the entire research institution, called the Musaeum in honor of the Muses, that had been built around the library, and whose vestiges and successor the Serapeum were destroyed in or around 391 CE. He was also the father of the mathematician Hypatia, who was gruesomely murdered in 415 by a mob supporting the Christian bishop Cyril against the Roman governor Orestes whom she advised.

Sometimes Euclid left out cases of theorems or proofs because he wasn’t going to use them later. Theon filled in several such cases and even added a theorem or two of his own. His greatest service is that he filled in extra propositions and lemmas to some of Euclid’s arguments to make them easier to follow. Theon’s editions were the only ones known until an earlier one without his emendations was discovered at the Vatican in 1803, and they remained the standard for school texts in Britain and elsewhere clear through the 1800s.

Proofs by Cases

Many theorems have clean proofs, some have technical proofs, some have messy proofs. One type of messy proof uses many different cases. These proofs begin like this:

We note that there are ten possible cases based on the {\dots}

The proof then proceeds to analyze each of the ten cases. Ugh. I personally do not like such proofs—who does? The main problem with them is the danger of both omission and perdition: If you omit a case that needs to be there then the proof is incomplete—or worse, wrong—while if you include all cases but err on a single one, then the whole proof is lost.

Even if the proof is correct, who will read it? Our friends at Wikipedia redirect “proof by cases” to the old classical name, proof by exhaustion. Today this connotes how the reader might feel. Concretely, they note:

A proof with a large number of cases leaves an impression that the theorem is only true by coincidence, and not because of some underlying principle or connection.

Nevertheless, they note some theorems for which the only known proofs have many cases:

  • The nonexistence of a finite projective plane of order 10.
  • The classification of finite simple groups.
  • The Kepler conjecture.

Thomas Hales’s proof of the last of these has recently been formally completed using two computerized proof assistants.

Moreover, last year’s computerized advance on the Erdős Discrepancy Problem used SAT-solvers in an overt kind of proof-by-exhaustion. Perhaps only a computer can love such a proof.

More concretely, perhaps some theorems elude proof because we humans don’t see a good way to break things down into cases, whereas computers can try many options. But saying this brings the matter around full circle because it is asking us humans for a guiding principle to form the cases. This might encourage us instead to go back and look for a guiding principle by which to do the proof without cases.

Avoiding Case Proofs

Sometimes one can avoid case-analysis proofs. Sometimes finding the right wording will do it. In a pumping-lemma proof that the language {\{a^n b^n c^n : n > 0\}} is not context-free, one might break into cases according to whether a certain pair {u,w} of critical substrings includes {a}‘s, {b}‘s, and/or {c}‘s. Or you can just say the pair cannot include all three, so that the three “regions” of a pumpable string {x = a^p b^p c^p =: yuvwz} cannot stay in sync with each other when forming {x^{(0)} = yvz} or {x^{(2)} = yuuvwwz} and so on. But this is only wording. Can we give a more concrete suggestion?

Here is a method. If you can manage it then I think it is the best method. It is to prove a more general statement that implies what you previously could only prove by case analysis.

Here are some simple examples of what I am thinking about.

{\bullet } Consider the following theorem from a webpage on proofs by exhaustion:

Theorem: If {n} is a positive integer, then {n^{7}-n} is divisible by {7}.

The following is the case analysis proof that is given there:

case2

This is all correct, but not very convincing. A better proof is to show the stronger result:

Theorem: If {n} is a positive integer and {p} is a prime, then {n^{p}-n} is divisible by {p}.

{ \bullet } Suppose you have a graph from a certain family and want to prove that it has a path of length {100}. A case analysis might work, but a better method might to note that all graphs in this family have high degree. Then invoke the famous theorem of Andrew Dirac:

Theorem: A graph with {n \ge 3} vertices is Hamiltonian if every vertex has degree {n / 2} or greater.

{\bullet } Suppose that you are confronted with proving that all the roots of some polynomial are real. You could compute the actual roots of the polynomial, but that is potentially error-prone. A better approach might be to find a symmetric real matrix {A} so that the eigenvalues of {A} are the roots of the polynomial.

{\bullet} A case analysis involving sums can sometimes be tamed by replacing the sums with integrals. Ken recalls a take-home final on which he spent ten pages arranging terms of a multiple summations in various ways according to the values of some parameters, only to learn from the answer key that it was a one-page consequence of Fubini’s Thoerem.

Open Problems

Is there a way to quantify the extent to which a theorem needs case analysis in its proofs?

11 Comments leave one →
  1. Mr Blah permalink
    April 22, 2015 11:54 am

    how many cases is considered too much ? 3?

  2. April 22, 2015 1:46 pm

    On Boole’s Ark all cases come two by two. Here’s a sketch of the Case Analysis-Synthesis Theorem (CAST) that weathers any deluge:

    Case Analysis-Synthesis Theorem

  3. April 22, 2015 1:49 pm

    another very interesting “case study” in “cases” is the 4 color theorem. which was reduced to exhaustive computer search. and never has really been made into a human-understandable/ conceptualizable proof despite much effort & some further progress. it also reminds me of hilberts old ideas on “finitistic” mathematics apparently now reflected in the concepts of decidability (although it seems nobody has ever pointed this out in a survey).
    which reminds me of my own newer thoughts on this relating CS/math in the old curry howard correspondence & shows why math can be so difficult/ complex at times:

    a math theorem/ proof is a program that runs in a mathematicians head.

    • April 24, 2015 8:02 am

      I agree. Sometimes, I wonder: if the humans had more fingers, then we would accept larger case analysis as “natural”. Perhaps, mathematician centipedes would be fine with the 4 color theorem’s proof : )

      • April 24, 2015 12:19 pm

        actually ability of humans to conceptualize large proofs is very likely its related to concepts studied in psychology called cognitive load and also chunking, and there is some similar concept in software engr called “cognitive overhead”… but all this is not acknowledged much in the math field where large complex proofs are quite rampant now yet rarely “meta-analyzed”.

  4. April 22, 2015 2:39 pm

    To me, the case proof of the nonexistence of a finite projective plane of order 10 simply means that no one has still understood this result. And as you mentioned in your post, what we need here is an argument to classify the integers n such that there exists a finite projective plane of order n. Or to be less ambitious, at least an argument that rules out 10 and a bunch of other integers, if not a characterization.

  5. E.L. Wisty permalink
    April 22, 2015 5:41 pm

    Reblogged this on Pink Iguana.

  6. April 23, 2015 3:15 pm

    Chess endgame tablebases — databases that play n-piece chess-games perfectly — can be regarded as vast collections of chess-related case-analysis proofs … hundreds of billions of rigorous proofs … with many (most?) of these proofs being lengthy and intricate beyond human understanding.

    Some chess-proofs have a structure that is amenable to human understanding … Lucena versus Philodor positions in rook-and-pawn versus rook endgames, for example. Other positions have no structure that humans can perceive.

    Conclusion  There’s mystery and beauty in chess … but not every position is mysteriously beautiful (or even accessible to human understanding). Similarly, there’s mystery and beauty in mathematics … but not every theorem is mysteriously beautiful (or even accessible to human understanding).

    An essay by Ken Regan on this topic would be welcomed and enjoyed (by me and many).

    • April 24, 2015 7:48 am

      By an amusing coincidence, the game Carlsen-Kramnik that is going on right now in in the Shamkir Chess Tournament, looks like it may be heading toward a Lucena-winning endgame (sought by Carlsen) versus a Philodor-drawing endgame (sought by Kramnik).

      In this game the engines see the chess-future by case-analysis; the humans see the future (presumably) by pattern-recognition (as encoded in narratives?). Here Ken Regan assuredly sees more than me!

Trackbacks

  1. The Shapes of Computations | Gödel's Lost Letter and P=NP
  2. Did Euclid Really Mean ‘Random’? | Gödel's Lost Letter and P=NP

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s