Direct proof and contraposition

Square the whole numbers from zero to five and you get 0, 1, 4, 9, 16 and 25. The entries divisible by two are 0, 4 and 16, and they sit at 0, 2 and 4, which are themselves divisible by two; the remaining entries sit at the remaining inputs. Six cases therefore agree with a claim: if the square of a whole number is even, then the number is even. Six cases are not a proof, and the previous section explains why.

What turns the six cases into a proof is an argument that covers every whole number at once, including the ones nobody will ever square. A proof is a sequence of steps from assumptions and definitions to the claim, in which each step is one that another careful reader would also make [S:5:17]. The last clause does the real work, because a proof is not an argument that merely happens to convince you. It is an argument you could hand to a suspicious stranger who accepts your definitions and nothing else. !The contrapositive matches the claim in all four rows, and the converse does not. The claim fails in one row only, the row where the hypothesis holds and the conclusion does not. Read the same four rows from the other end and the contrapositive fails in that same row, so the two columns carry the same truth value everywhere and the turn costs nothing. The converse differs in two rows, which is why it proves nothing about the claim. Four rows are the whole licence for contraposition. Status: schematic.

Call a whole number even when it equals 2i for some whole number i, and odd when it equals 2i + 1. Six is even because 6 = 2 × 3, and seven is odd because 7 = 2 × 3 + 1; these two definitions are the only machinery that the worked example needs.

A direct proof begins at the assumption and walks forward towards the goal. Here the assumption is that n² is even, so n² = 2i for some whole number i, and the goal is a sentence about n. The only move available is substitution, and substitution runs forward: put n = 2i into n² and out comes 4i².

Substitution does not run backwards on its own. From n² = 4i² you would have to conclude n = 2i, and that conclusion needs a fact about squares: a number and its negative are the only numbers with a given square, and n is not negative. Taking a square root is therefore not a step inside the whole numbers, because the square root of 2 is not one.

Every proof of this kind has three parts, and naming them removes most of the mystery. The starting points are the statements you may begin from: the hypotheses, the assumptions the claim hands you at the start, together with the definitions and everything already established. The goal is the statement you must finish at, and a step is a move from statements already established to one additional statement [S:5:17]. A proof is a finite sequence of such steps, which is why a proof can be verified line by line by somebody who did not invent it.

The contrapositive of "if P then Q" is "if not Q then not P", and the two sentences are true in exactly the same circumstances [S:16:140]. Four rows settle that equivalence, one for each way the two sentences P and Q can be true or false:

The two right-hand columns agree in every row, and that agreement is the entire licence for using the contrapositive [S:16:140]. The turned-round sentence begins at what you were trying to reach and ends at what you were given, which is the direction in which the algebra runs.

Worked example. Show that if n² is even then n is even.

The contrapositive is: if n is not even then n² is not even. Suppose that n is not even. Every whole number leaves remainder 0 or 1 on division by 2, so n is odd and n = 2i + 1 for some whole number i. Squaring and expanding,

That line says n² is one more than an even number, so n² is odd. No whole number is both even and odd, so n² is not even, and the claim follows from the table.

At i = 3 the number is n = 7, and 7² = 49 = 2 × 24 + 1, which is odd. The computation is a verification of the algebra on a single case and not a proof of anything, which is the distinction this chapter keeps pressing.

The converse is a different sentence altogether. "If n is even then n² is even" is the sentence you get by swapping hypothesis and conclusion, and proving it would tell you nothing about the claim you were asked to establish. The contrapositive and the converse are both true in this example, and that is a coincidence of the example rather than a rule [S:16:140].

When you read a result, locate which sentence is the assumption and which is the conclusion, because that direction decides which experiments count. Take the claim that if a method works then its benchmark improves. A run in which the method works and the benchmark does not improve ends the claim. A run in which the benchmark improves while the method fails says nothing at all, because the benchmark has other causes. The two sentences differ by one swap, and the difference decides what evidence would count.

The method has boundaries. Contraposition applies only to a claim of the form "if A then B", so it does nothing for a claim of another shape, and it carries the assumptions across unchanged. A proof also establishes only that the conclusion follows from the hypotheses, so if a hypothesis never holds the claim is true and empty: it forbids nothing, and no observation can count against it. The deeper limitation is that a proof is relative to its assumptions and its definitions, and a disagreement about either is not settled by the proof itself.

Proofs are written by people, and some published ones are wrong. An incorrect proof of the four colour theorem, which says that four colours suffice to colour any map so that regions sharing a border differ, stood for ten years before its mistake was discovered [S:5:15].

The formal statement. A proof of a conclusion from hypotheses is a finite sequence of sentences. Each sentence is a hypothesis, a definition, an axiom, or the conclusion of a rule whose premises appear earlier. A rule is sound when every assignment of truth values that makes its premises true also makes its conclusion true. Soundness is what lets a reader check a proof line by line without trusting the writer [S:5:18].

The theorem. An implication and its contrapositive have the same truth value in every row. The implication is false in exactly one row: hypothesis true, conclusion false. In that row the negated conclusion is true and the negated hypothesis is false, so the contrapositive is false too. In the other three rows the implication is true, and in each of them either the negated conclusion is false or the negated hypothesis is true, so the contrapositive is true. Two sentences that are false in the same single row agree in all four.

That is the whole licence for contraposition. It also states the limit: the move applies to an implication and to nothing else.

The worked example. Assume $n$ is odd, so $n=2i+1$ for some whole number $i$. Then $n^2=2(2i^2+2i)+1$, which has the form $2j+1$, so $n^2$ is odd. The contrapositive follows, and the original claim follows from it.

The hidden hypothesis. The step "every whole number is even or odd" is the division algorithm, and it is a theorem, not a definition. Without it, "not even" does not deliver $n=2i+1$, and the proof stops. The collection matters as well: over the integers the argument still works, but "even" has no meaning for a general real number, so the sentence is not defined there.

The edge case. The core says that the direct route is blocked because substitution runs forward. That is a claim about one toolkit, not about logic. A direct proof exists: write $n$ as an odd number times a power of 2, and read that power in $n^2$. The contrapositive is shorter, not the only path. Treating "no direct proof in this style" as "no proof" is the mistake this chapter catalogues elsewhere.

Where the walking analogy breaks. A proof is not a path in time. The order of the lines is a presentation, and a proof may use a lemma proved later or elsewhere. What matters is the dependency: each line rests on earlier ones. A machine checks that relation, and it does not care which line you wrote first.

What the core left out. The core left out the axioms, and it left out the choice of what counts as established. A proof is relative to a system, so a step that one reader accepts as settled another may reject as unproved [S:5:17]. That is not a defect of proof. It is why a proof states its assumptions before its first line.

Original sources. Direct proof is section 4.3 of Hammack [S:16:130] and contrapositive proof is chapter 5 [S:16:140]; the truth table that licenses the turn is printed in chapter 5. The definition of a proof as a sequence of sound deductions, with modus ponens as the basic rule, is section 1.4 of Mathematics for Computer Science [S:5:17]. The same chapter records that published proofs fail: an incorrect proof of the four colour theorem stood for ten years before its mistake was found [S:5:15].

An open question. A proof is only as good as the sentence it proves, and turning an English claim into a formal one is still done by hand. Whether that step can be automated without changing the claim is open. A formalisation can be faithful to a different theorem, and the kernel will accept it. Evidence that would settle the question: a system that formalises unseen statements, whose output is translated back into English and judged equivalent to the original by readers who did not write it, with a published error rate. Agreement on the proofs alone would not settle it, because a proof is checked against the statement and not against the intention.

A frontier result. Machine-checked proof is now available for mathematics. Lean 4 and the other kernels accept a proof only when every step is licensed, which is the mechanical version of the core's "another careful reader" [S:603:2]. The benchmark that measures progress on competition mathematics is written in Lean 4 and the other kernels, and its formalisations are built and debugged by hand before use [S:603:2]. The manual step is the formalisation, not the checking.

What to read next. Read section 4.3 of [S:16:130] and section 5.1 of [S:16:140] for the two proof templates, then section 1.4 of [S:5:17] for the rules that license each line. Read the background section of [S:603:2] for what a kernel checks, and keep the four-colour history in [S:5:15] in view: a checked proof and a correct proof are different claims.