Proof Outlines
LINE NUMBERS: Only lines that are referred to have labels (for example, L1) in this document. For a formal proof, all lines are numbered. Line numbers appear at the beginning of a line. You can indent line numbers together with the lines they are numbering or all line numbers can be unindented, provided you are consistent.
INDENTATION: Indent when you make an assumption or define a variable. Unindent when this assumption or variable is no longer being used.
1. Implication: Direct proof of A IMPLIES B.
L1. Assume A.
.
L2. B
A IMPLIES B; direct proof: L1, L2
2. Implication: Indirect proof of A IMPLIES B.
L1. Assume NOT(B).
.
L2. NOT(A)
A IMPLIES B; indirect proof: L1, L2
3. Equivalence: Proof of A IFF B.
L1. Assume A.
.
L2. B
L3. A IMPLIES B; direct proof: L1, L2
L4. Assume B.
.
L5. A
L6. B IMPLIES A; direct proof: L4, L5 A IFF B; equivalence: L3, L6
4. Proof by contradiction of A.
L1. To obtain a contradiction, assume NOT(A). .
L2. B .
L3. NOT(B)
L4. This is a contradiction: L2, L3
Therefore A; proof by contradiction: L1, L4
1
5. Modus Ponens.
.
L1. A
.
L2. A IMPLIES B
B; modus ponens: L1, L2
6. Conjunction: Proof of A AND B:
.
L1. A
.
L2. B
A AND B; proof of conjunction; L1, 2
7. Use of Conjunction: .
L1. A AND B
A; use of conjunction: L1 B; use of conjunction: L1
8. Implication with Conjunction: Proof of (A1 AND A2) IMPLIES B.
L1. Assume A1 AND A2. A1; use of conjunction, L1 A2; use of conjunction, L1
.
L2. B
(A1 AND A2) IMPLIES B; direct proof, L1, L2
9. Implication with Conjunction: Proof of A IMPLIES (B1 AND B2).
L1. Assume A. .
L2. B1
.
L3. B2
L4. B1 AND B2; proof of conjunction: L2, L3 A IMPLIES (B1 AND B2); direct proof: L1, L4
10. Disjunction: Proof of A OR B and B OR A. .
L1. A
A OR B; proof of disjunction: L1 B OR A; proof of disjunction: L1
2
11. Proof by cases.
L1. C OR NOT(C) tautology
L2. Case 1: Assume C. .
L3. A
L4. C IMPLIES A; direct proof: L2, L3
L5. Case 2: Assume NOT(C). .
L6. A
L7. NOT(C) IMPLIES A; direct proof: L5, L6
A proof by cases: L1, L4, L7 12. Proof by cases of A OR B.
L1. C OR NOT(C) tautology L2. Case 1: Assume C.
.
L3. A
L4. A OR B; proof of disjunction, L3 L5. C IMPLIES (A OR B); direct proof, L2, L4
L6. Case 2: Assume NOT(C). .
L7. B
L8. A OR B; proof of disjunction, L7
L9. NOT(C) IMPLIES (A OR B); direct proof: L6, L8 A OR B; proof by cases: L1, L5, L9
13. Implication with Disjunction: Proof by cases of (A1 OR A2) IMPLIES B.
L1. Case 1: Assume A1. .
L2. B
L3. A1 IMPLIES B; direct proof: L1,L2
L4. Case 2: Assume A2. .
L5. B
L6. A2 IMPLIES B; direct proof: L4, L5
(A1 OR A2) IMPLIES B; proof by cases: L3, L6
3
14. Implication with Disjunction: Proof by cases of A IMPLIES (B1 OR B2).
L1. Assume A.
L2. C OR NOT(C) tautology L3. Case 1: Assume C.
.
L4. B1
L5. B1 OR B2; disjunction: L4
L6. C IMPLIES (B1 OR B2); direct proof: L3, L5 L7. Case 2: AssumeNOT(C).
.
L8. B2
L9. B1 OR B2; disjunction: L8
L10. NOT(C) IMPLIES (B1 OR B2); direct proof: L7, L9 L11. B1 OR B2; proof by cases: L2, L6, L10
A IMPLIES (B1 OR B2): direct proof. L1, L11
15. Substitution of a Variable in a Tautology:
Suppose P is a propositional variable, Q is a formula, and R′ is obtained from R by replacing every occurrence of P by (Q).
L1. R tautology
R′; substitution of all P by Q: L1
16. Substitution of a Formula by a Logically Equivalent Formula:
Suppose S is a subformula of R and R′ is obtained from R by replacing some occurrence of S by S′.
L1. R
L2. S IFF S′
L3. R′; substitution of an occurrence of S by S′: L1, L2
17. Specialization:
L1. c ∈ D
L2. ∀x∈D.P(x)
P(c); specialization: L1, L2
18. Generalization: Proof of ∀x ∈ D.P (x).
L1. Let x be an arbitrary element of D.
.
L2. P(x)
Since x is an arbitrary element of D, ∀x ∈ D.P (x); generalization: L1, L2
4
19. Universal Quantification with Implication: Proof of ∀x ∈ D.(P (x) IMPLIES Q(x)). L1. Let x be an arbitrary element of D.
L2. Assume P(x)
.
L3. Q(x)
L4. P(x) IMPLIES Q(x); direct proof: L2, L3
Since x is an arbitrary element of D,
∀x ∈ D.(P (x) IMPLIES Q(x)); generalization: L1, L4
20. Implication with Universal Quantification: Proof of (∀x ∈ D.P (x)) IMPLIES A.
L1. Assume ∀x ∈ D.P (x). .
L2. a ∈ D
P(a); specialization: L1, L2
.
L3. A
Therefore (∀x ∈ D.P (x)) IMPLIES A; direct proof: L1, L3
21. Implication with Universal Quantification: Proof of A IMPLIES (∀x ∈ D.P (x)).
L1. Assume A.
L2. Let x be an arbitrary element of D.
.
L3. P(x)
Since x is an arbitrary element of D, L4. ∀x ∈ D.P (x); generalization, L2, L3
A IMPLIES (∀x ∈ D.P (x)); direct proof: L1, L4
22. Instantiation:
L1. ∃x∈D.P(x)
Let c ∈ D be such that P (c); instantiation: L1
.
23. Construction: Proof of ∃x ∈ D.P (x).
L1. Let a = · · · .
L2. a ∈ D
.
L3. P(a)
∃x ∈ D.P (x); construction: L1, L2, L3
5
24. Existential Quantification with Implication: Proof of ∃x ∈ D.(P (x) IMPLIES Q(x)).
L1. Let a = · · ·
.
L2. a ∈ D
L3. Suppose P(a).
.
L4. Q(a)
L5. P(a) IMPLIES Q(a); direct proof: L3, L4
∃x ∈ D.(P (x) IMPLIES Q(x)); construction: L1, L2, L5
25. Implication with Existential Quantification: Proof of (∃x ∈ D.P (x)) IMPLIES A.
L1. Assume ∃x ∈ D.P (x).
Let a ∈ D be such that P (a); instantiation: L1
.
L2. A
(∃x ∈ D.P (x)) IMPLIES A; direct proof: L1, L2
26. Implication with Existential Quantification: Proof of A IMPLIES (∃x ∈ D.P (x)).
L1. Assume A.
L2. Let a = · · ·
.
L3. a ∈ D .
L4. P(a)
L5. ∃x ∈ D.P (x); construction: L2, L3, L4
A IMPLIES (∃x ∈ D.P (x)); direct proof: L1, L5 27. Subset: Proof of A ⊆ B.
L1. Let x ∈ A be arbitrary. .
L2. x ∈ B
The following line is optional:
L3. x ∈ A IMPLIES x ∈ B; direct proof: L1, L2
A ⊆ B; definition of subset: L3 (or L1, L2, if the optional line is missing)
6
28. Weak Induction: Proof of ∀n ∈ N.P(n)
Base Case:
.
L1. P(0)
L2. Let n ∈ N be arbitrary.
L3. Assume P(n).
.
L4. P(n+1)
The following two lines are optional:
L5. P (n) IMPLIES (P (n + 1); direct proof of implication: L3, L4
L6. ∀n ∈ N.(P (n) IMPLIES P (n + 1)); generalization L2, L5
∀n ∈ N.P(n) induction; L1, L6 (or L1, L2, L3, L4, if the optional lines are missing)
29. Strong Induction: Proof of ∀n ∈ N.P(n) L1. Let n ∈ N be arbitrary.
L2. Assume ∀j ∈ N.(j < n IMPLIES P(j))
.
L3. P(n)
The following two lines are optional:
L4. ∀j ∈ N.(j < n IMPLIES P(j)) IMPLIES P(n); direct proof of implication: L2, L3
L5. ∀n ∈ N.[∀j ∈ N.(j < n IMPLIES P(j)) IMPLIES P(n)]; generalization: L1, L4 ∀n ∈ N.P(n); strong induction: L5 (or L1, L2, L3, if the optional lines are missing)
30. Structural Induction: Proof of ∀e ∈ S.P (e), where S is a recursively defined set
Base case(s):
L1. For each base case e in the definition of S L2. P(e).
Constructor case(s):
L3. For each constructor case e of the definition of S,
L4. assume P(e′) for all components e′ of e.
.
L5. P(e)
∀e ∈ S.P (e); structural induction: L1, L2, L3, L4, L5
7
31. Well Ordering Principle: Proof of ∀e ∈ S.P (e), where S is a well ordered set, i.e. every nonempty subset of S has a smallest element.
L1. To obtain a contradiction, suppose that ∀e ∈ S.P (e) is false.
L2. Let C = {e ∈ S | P(e) is false} be the set of counterexamples to P. L3. C ̸= φ; definition: L1, L2
L4. Let e be the smallest element of C; well ordering principle: L2, L3 Let e′ = · · ·
.
L5. e′ ∈C .
L6. e′ < e.
L7. This is a contradiction: L4, L5, L6
∀e ∈ S.P (e); proof by contradiction: L1, L7
8