Direct proof and the contrapositive: chaining implications, and when to flip them
A direct proof chains implications from premise to goal, each link justified: assume, manipulate, conclude. When that road is steep, flip to the contrapositive — ¬Q→¬P proves P→Q. Code review works the same way: you approve a function by chaining its guarantees.
During a code review, a junior engineer asked the team lead a question that sounds naive and is not: “How do you actually know this never returns null?” The lead did not run the code. She read it aloud, slowly. The route only fires after the auth middleware, so req.user exists. The handler passes req.user.id, which the schema already validated as a UUID. getProfile either returns a row or throws — its contract says it never returns null for a valid UUID. So the caller never sees null. Four sentences, each one leaning on the previous, ending exactly at the thing they wanted to know. Nobody called it that, but the lead had just produced a direct proof — the oldest move in mathematics: a chain of statements where every link is justified, from what you know to what you claim.
After this lesson you can build a direct proof using the assume-manipulate-conclude structure, use definitions as the handles a proof grips, recognize an unjustified link in a code review, explain why the contrapositive proves the same implication, and distinguish the contrapositive from the converse.
A proof of a claim is a chain of statements, each justified. Every statement is either a definition, an established fact, an explicit assumption, or a valid step from earlier links. Nothing mystical — a proof is an argument so explicit that a hostile reader finds a justification at every poke. Most claims worth proving have the shape P→Q. A direct proof of P→Q makes the obvious move: walk forward.
The three moves: assume, manipulate, conclude. Assume P holds and unpack what P means using definitions. Manipulate what you have — algebra, known facts — one justified step at a time. Conclude by recognizing the definition of Q in what you produced. Definitions are the handles; if you cannot state the definition, you cannot start the chain.
Claim. If n is even, then n² is even.
Proof. Assume n is even. By definition, n = 2k for some integer k. Then n² = (2k)² = 4k² = 2·(2k²). Since integers are closed under multiplication, 2k² is an integer — so n² equals 2 times an integer, which is the definition of even. Therefore n² is even. ∎
The phrase “for some integer k” names a witness without choosing it — which is how four sentences cover infinitely many numbers.
The contrapositive ¬Q→¬P is the same statement as P→Q. Their truth tables are identical in every row. Proving either proves both. When the direct road is steep — the premise hands you the harder object — flip to the contrapositive instead.
“If n² is odd, then n is odd” resists direct attack: you hold a fact about n² and need a fact about n. Its contrapositive is “if n is even, then n² is even” — which we just proved in Step 2. One citation closes it: by contraposition, since n even implies n² even, n² odd implies n odd. ∎
The converse Q→P is a different statement and proves nothing about P→Q. The converse is the arrow reversed without negating. Its truth table differs from P→Q in two rows — a genuinely distinct claim. The classic production bug: the spec says “if invalid, return null”. Logs show a null. Reviewer writes “so the input was invalid” — that is the converse, which the spec never promised. Null can also come from a timeout or empty result set. The only licensed flip is the contrapositive: if non-null, the input was valid.
Code review as a direct proof.
// Claim: if the input passed validation, sendReceipt never sees a missing email.
app.post("/orders", validate(orderSchema), (req, res) => {
const order = req.body; // link 1: validate() ran → body matches schema
const email = order.customer.email; // link 2: schema requires customer.email
sendReceipt(email); // link 3: email is non-empty → never null
res.sendStatus(201);
});Approving this PR is checking a direct proof: every line must be justified by a guarantee established earlier. The moment email is marked optional in the schema, link 2 breaks — and that is the exact line the future bug report will point to. A review comment “what guarantees that order.customer exists?” is a request for a missing justification, word for word what a mathematician asks at a seminar.
▸Why this works
“You assumed n is even — isn’t that cheating?” No. P→Q does not claim Q; it claims Q holds whenever P does. To verify “whenever P, Q”, you step into the world where P holds and show Q follows. You are not asserting n is even in the real world — you are exploring the world where it is. The proof would only be circular if you assumed Q, the conclusion. Assuming P is not a bug in the method; it is the method.
Name the three moves of a direct proof (comma-separated).
In 'if n is even then n² is even', what definition do you unpack at the 'assume' step? Write the algebraic form.
Is the contrapositive ¬Q→¬P the same statement as P→Q? Answer yes or no.
The spec says 'if input is invalid, return null'. You observe a null return. Can you conclude the input was invalid? Answer yes or no.
The spec says 'if input is invalid, return null'. You observe a NON-null return. Can you conclude the input was valid? Answer yes or no.
The spec guarantees: if input is invalid, the function returns null. In production logs you find a call that returned null. What can you conclude about its input?
A proof is a finite chain of statements, each one a definition, a known fact, an explicit assumption, or a valid step from earlier links — explicit enough that a hostile reader finds a justification at every poke. A direct proof of P→Q assumes P, unpacks it with a definition, pushes justified algebra, and re-packs the result into the goal’s definition. “For some integer k” names a witness without choosing it — how four sentences cover infinitely many cases. Code review runs the same craft with guarantees for links, and an unjustified link is exactly where the future bug report will point. Loops extend this through invariants — each iteration preserving a property is one link of a chain as long as the input. When the direct road is steep, flip to the contrapositive: P→Q and ¬Q→¬P are the same statement. But never flip without negating: the converse Q→P is a different statement, and “it returned null, so the input was invalid” is its classic production disguise. Negate and swap, or do not swap at all.
Practice
Start at the top. Tasks go easiest → hardest: recall a fact, apply it to a case, then a senior-level stretch. Open one, attempt it, then reveal.
Something unclear?
Ask a question about this lesson. Questions are anonymous and go straight to the author to make the lesson better.
Apply this
Put this lesson to work on a real build.