Proof techniques are to InferenceRules what strategies are to tactics. A proof technique is a template for how to go about proving particular classes of statements: this template guides you in the choice of inference rules (or other proof techniques) to write the actual proof. These notes will talk about strategies for proving specific kinds of statements, and then give some examples of proofs that use one or more of these strategies.
1. Proof strategies
These are largely drawn from SolowBook, particularly the summary table on pages 156-159 (which is the source of the order and organization of the table and the names of the most of the techniques). RosenBook describes proof strategies of various sorts in §§1.5—1.7 and BiggsBook describes various proof techniques in Chapters 1, 3, and 4; both descriptions are a bit less systematic, but also include a variety of specific techniques that are worth looking at.
In the table below we are trying to prove A ⇒ B for particular statements A and B. The techniques are mostly classified by the structure of B. Before applying each technique, it may help to expand any definitions that appear in A or B.
Strategy |
When to use it |
What to assume |
What to conclude |
What to do/why it works |
Direct proof |
Try it first |
A |
B |
Apply inference rules to work forward from A and backward from B; when you meet in the middle, pretend that you were working forward from A all along. |
Contraposition |
B = ¬Q |
¬B |
¬A |
Apply any other technique to show ¬B ⇒ ¬A and then apply the contraposition rule. Sometimes called an indirect proof although the term indirect proof is often used instead for proofs by contradiction (see below). |
Contradiction |
When B = ¬Q, or when you are stuck trying the other techniques. |
A ∧ ¬B |
False |
Apply previous methods to prove both P and ¬P for some P. Note: this can be a little dangerous, because you are assuming something that is (probably) not true, and it can be hard to detect as you prove further false statements whether the reason they are false is that they follow from your false assumption, or because you made a mistake. Direct or contraposition proofs are preferred because they don't have this problem. |
Construction |
B = ∃x P(x) |
A |
P(c) for some specific object c. |
Pick a likely-looking c and prove that P(c) holds. |
Counterexample |
B = ¬∀x P(x) |
A |
¬P(c) for some specific object c. |
Pick a likely-looking c and show that ¬P(c) holds. This is identical to a proof by construction, except that we are proving ∃x ¬P(x), which is equivalent to ¬∀x P(x). |
Choose |
B = ∀x (P(x) ⇒ Q(x)) |
A and P(c) where c is chosen arbitrarily. |
Q(c) |
Choose some c and assume A and P(c). Prove Q(c). Note: c is a placeholder here. If P(c) is "c is even" you can write "Let c be even" but you can't write "Let c = 12", since in the latter case you are assuming extra facts about c. |
Specialization |
A = ∀x P(x) |
A |
B |
Pick some particular c and prove that P(c) ⇒ B. Here you can get away with saying "Let c = 12." (If c=12 makes B true). |
Proof by elimination |
B = C ∨ D |
A ∧ ¬C |
D |
The reason this works is that A ∧ ¬C ⇒ D is equivalent to ¬(A ∧ ¬C) ⇒ D ≡ ¬A ∨ C ∨ D ≡ A ⇒ (C ∨ D). Of course, it works equally well if you start with A ∧ ¬D and prove C. |
Case analysis |
A = C ∨ D |
C, D |
B |
Here you write two separate proofs: one that assumes C and proves B, and one that assumes D and proves B. A special case is when D = ¬C. You can also consider more cases, as long as A implies at least one of the cases holds. |
Some others that are mentioned in SolowBook: Induction, Direct Uniqueness, Indirect Uniqueness, various max/min arguments. We will cover InductionProofs and Uniqueness proofs eventually.
2. Examples
We'll work in the "first-order theory of the integers", which means we have 0, 1, +, -, *, <, and =, plus some other constants and relations that are easily derived from them (e.g. 2 is defined as 1+1, 3 = 1+1+1, 4 = 1+1+1=1, etc.) We'll assume that all of the usual grade-school facts about addition and multiplication and so forth are given.
Some definitions.
Even(x) ≡ x is even ≡ ∃k: x = 2k.
- Odd(x) ≡ ¬Even(x).
Square(x) ≡ x is a square ≡ ∃y: x = y2.
Composite(x) ≡ x is composite ≡ ∃y ∃z: (y > 1 ∧ z > 1 ∧ x = y*z).
Prime(x) ≡ x is prime ≡ (x > 1) ∧ ¬Composite(x)
Now let's try to prove a few things:
- Prove: ∀x ∀y: Even(x) ∧ Even(y) ⇒ Even(x+y).
- Fix x and y such that Even(x) and Even(y). [Starting a proof by choosing here.]
- From the definition of Even, ∃k: x = 2k. Let k be such that x = 2k. [Existential specialization rule.]
- From the definition of Even, ∃k: y = 2k. Let k' be such that y = 2k'.
- x+y = 2k + 2k'. [Substitution rule.]
- x+y = 2(k+k'). [Distributive property of multiplication (part of the axioms for the integers).]
- Even(x+y). [Existential generalization rule.]
- ∀x ∀y: Even(x) ∧ Even(y) ⇒ Even(x+y). [Conclusion of proof by choosing.]
- Prove: ¬Square(12)
Rewrite as ¬∃x x2 = 12 ≡ ∀x x2 ≠ 12 and fix x. [proof by choosing]
- Now consider two cases:
If -3 ≤ x ≤ 3, then x2 ≤ 9 < 12. So x2 ≠ 12.
If x ≥ 4 or x ≤ -4, then x2 ≥ 16 > 12. Again x2 ≠ 12.
- Prove: ∀x: Even(x) ⇒ Odd(x+1).
- By contradiction: assume ∃x: Even(x) ∧ ¬Odd(x+1).
- Even(x) ∧ Even(x+1). [Definition of Odd]
- ∃k: x = 2k. [Subtraction, Definition of Even]
- ∃k': x+1 = 2k'. [Subtraction, Definition of Even]
- Let k be such that x = 2k, k' be such that x = 2k'. [Existential specialization]
- 1 = x+1 - x = 2k' - 2k = 2(k-k'). [Algebra]
- Now consider two cases: q = k - k' ≤ 0 or q ≥ 1.
- If q ≤ 0, then q ≤ 0 and so 2q ≠ 1.
- If q ≥ 1, then 2q ≥ 2 and so 2q ≠ 1.
- 2(k-k') ≠ 1, a contradiction. Thus the assumption is false.
- Prove: ∃x: (Square(x) ∧ Even(x)).
- Let x = 0.
- Let y = 0.
x = y2.
∃y: x = y2. [Existential generalization]
- Square(x). [Definition of Square]
- Let k = 0.
- x = 2k.
- ∃k x = 2k. [Existential generalization]
- Even(x). [Definition of Even]
- Square(x) ∧ Even(x). [Conjunction]
- ∃x: (Square(x) ∧ Even(x)). [Existential generalization]
Prove: ¬∀x x2 > 12.
- Let x = 3. [proof by counterexample]
x2 = 9 ≯ 12.
Prove: x2-4 ≥ 0 ⇒ (x ≤ 0) ∨ (x ≥ 2).
Assume ¬(x ≤ 0), i.e. x > 0. [start of proof by elimination]
- Factor to get (x-2)(x+2) ≥ 0.
From x > 0, we have x+2 > 0.
- Divide both sides of (2) by x+2 to get x-2 ≥ 0.
- Add 2 to both sides to get x ≥ 2.
Prove: x3 > 0 ⇒ x > 0.
- Suppose x ≤ 0. [start of proof by contraposition]
x*x = x2 ≥ 0. [algebra]
x*x2 = x3 ≤ 0. [more algebra]
We've just shown x ≤ 0 ⇒ x3 ≤ 0, so by contraposition we have x3 > 0 ⇒ x > 0.
PineWiki