2.4 Iff, Equivalence, and What a Definition Says
One connective is still without rules: “if and only
if”. Theorems say “
2.4.1. The rules for “if and only if”
“
An “if and only if” is two implications, and proving it takes two proofs.
The first schema is the rule
As in every schema (Definition 1.2.1),
- Two boxes.
needs two available boxes: one opened by and ending in , the other opened by and ending in , each last line a line of its own box. Each is exactly the box would need for one direction. Their order does not matter, but both must be there: a single box from to proves and nothing more. Each box’s assumption is printed “asm, for ”; in a written proof the two boxes are the paragraphs and . - Separate boxes. The boxes are siblings, not nested, so nothing in the second may cite a line of the first (the scope rule of Definition 1.4.2). Each direction is a proof on its own.
- Citation. The justification cites
both boxes as ranges, as in
. - Elimination, either way. From
and on available lines, writes ; from and , it writes . It is modus ponens in whichever direction we need, citing the biconditional first.
In the Givens/Goal table,
2.4.2. First derivations with iff
The section’s goal-directed move: a goal
- (a) Show that
. - (b) Show that
.
Solution.
- (a) Idea.
The goal is an iff, so the last line is
, and we need a box from to and a box from to . Each box’s goal is one away: the premise crosses from its assumption to the other side.The goal at the foot (left), then its two boxes (right).
1612 asm, for34 asm, for56 2–3, 4–5The finished derivation:
12 asm, for3 1, 24 asm, for5 1, 46 2–3, 4–5Line 3 uses the second form of
(right to left), line 5 the first. - (b) Idea.
The goal
is a negation, so open a box on and aim at (Section 2.2). Inside, the premise turns into , and clashes with .
This is the derivation of Proposition 2.3.1
with
The rules say nothing that the two implications do not say. The next result makes this exact.
Idea. Each goal chooses its rule.
For the first, the goal is a conjunction of two
implications:
First claim: the two implications as goals (left), then their boxes (right).
Second claim: the premise taken apart (left), then the two boxes (right).
Proof. For the first claim, the
following is a derivation with premise
For the second claim, the following is a derivation
with premise
Lines 2 and 3 lie in no box, so both boxes may cite them. This proves both claims.
Second readingWhy iff keeps its own rules
So
Show that
Solution. Idea. The goal
is an iff, so there are two boxes, one opened by
The outer boxes (left), then a
The finished derivation:
The two halves are mirror images.
Quick check. In the derivation of
Example (Negating both sides of an iff),
which line does line 5 cite as
Solution. Line 2,
The derivation uses only the rules of this section
and of Sections 2.1–2.2. Its converse,
Example (Negating both sides of an iff) negated both sides of an iff. Can one side be the negation of the other, a statement equivalent to its own negation?
Idea. The goal is a negation: open
a
The outer box (left), then the subgoal
Proof. The following is a
derivation with no premises and last line
Line 5 may be cited at lines 6 and 7: it lies in the
box
In words: no statement is equivalent to its own negation; a definition that made a term mean the failure of that very term would define nothing.
For an instance, let
Quick check. In the proof of Lemma 2.4.2, which two lines use the biconditional, and in which direction?
Solution. Line 3, from the left
side
2.4.3. Provable equivalence
Proposition 2.4.1 is a pair of sequents, one in each direction. It is not the first such pair: Proposition 1.4.2 and Proposition 1.6.1 are pairs too. When two statements can each be derived from the other, either may stand in for the other in any derivation, and the situation deserves a name.
Two statements are provably equivalent when each can be derived from the other.
Statements
In words: there is a derivation with premise
A first example is
Second readingEdge cases of provable equivalence
The degenerate example is
A minimal change gives a one-way street. Example (Two negations from one premise)
derived
The connective
For all statements
- (a)
if and only if ; - (b)
; if , then ; and if and , then .
In words: one derivation of
Second readingThe proof: copying derivations
Idea. Everything here moves whole
derivations around. To prove
Proof. We use one observation
twice. Let
- (b) The one-line
derivation consisting of the premise
shows , in both directions, so . Symmetry holds because Definition 2.4.2 says the same thing about as about . For transitivity it is enough to show that and give , since the reverse direction is the same statement with and exchanged. Take a derivation of from , and below its last line copy a derivation of from , turning each premise line of into a repetition of the last line of . That line lies in no box, so it is available everywhere below it, and by the observation the rest of the copy is justified. The result has premise and last line . This proves the proposition.
Here are equivalences derived so far. Each row gives two derived rules (Definition 2.3.1), one in each direction.
| Provable equivalence | Derived in |
|---|---|
| Proposition 1.2.1, with the letters exchanged for the converse | |
| Example (First derivations with “or”), likewise | |
| Proposition 1.4.2 | |
| Proposition 1.6.1 | |
| Example (Cases on a hypothesis are two implications) and Example (A disjunctive hypothesis splits into two implications) | |
| Proposition 2.4.1 | |
| Example (An iff read both ways) (a), with the letters exchanged | |
| Example (Three negations become one),
and Example (Two negations from one premise)
(a) with |
The fourth row is distributivity of
Warning. A sequent in one direction
is not an equivalence.
2.4.4. Proving an iff: two directions
In a written proof, the two boxes of
The first example completes the story of parity. We use the facts (E1)–(E3) of Section 2.1: every integer is even or odd; no integer is both even and odd; the square of an odd integer is odd.
Let
Idea. Two boxes. Forwards is (E3).
Backwards, “
Proof.
This proves the theorem
With the derived rules of Section 2.3,
The next example is about real numbers, and its two directions do different work. Each hypothesis is needed: dropping either one breaks one of the two directions, as the remark after the proof shows.
Let
Idea. Forwards, multiply
Proof.
This proves the theorem
Remark. Each hypothesis has a job.
The direction
A payoff comes at once. For
Quick check. Here is a proof of the
statement “for a real number
If
, then . If , then . This proves the claim.
Which direction has been proved, and which is missing? Supply the missing one.
Solution. The proof assumes the
right side, “
Warning. A proof of an iff can
prove one direction twice and look complete. For “
2.4.5. What a definition says
Here is a definition written the way this book and most others write definitions.
A function
is strictly increasing if, for all real numbers and , implies .
Grammatically the sentence is an implication, “
In a definition, “if” means “if and only if”.
This is a convention of mathematical language, not a
rule of logic. Some books write “iff” or
- (a) Show that
defines a strictly increasing function . - (b) Suppose
is strictly increasing. Show that . - (c) Show that
does not define a strictly increasing function .
Solution.
(a) Let
and be real numbers with . Multiplying by gives , and subtracting gives , that is, . So satisfies the condition, and by the definition, read from right to left, is strictly increasing .(b) Since
is strictly increasing, the definition, read from left to right, says that implies for all real and . Taking and , and using , we get .(c) Suppose
were strictly increasing . By the definition read from left to right, as in (b), would give , that is, , which is false . So is not strictly increasing .
Part (a) uses the definition from the condition to
the term; parts (b) and (c) use it from the term to the
condition. A definition read only as an “if” would
permit (a) and nothing else. Because the term means
exactly the condition, a candidate condition is judged
against the intended meaning. Had the definition said
“
Warning. The convention is for
definitions only. In a theorem, “if”
means “if”, one direction. The theorem “if
Second readingThe same slip in calculus
A familiar theorem of calculus says: if
Quick check. Write the converse of
“if a real number
Solution. The converse is “if
2.4.6. Chains of equivalences
“The following are equivalent: (a), (b), (c)” means
that any two of the three are equivalent: three iff
statements, or six implications. Three implications
suffice, if they go round in a cycle:
Idea. The goal is an iff, so there
are two boxes. From
The goal at the foot (left), then its two boxes (right).
Proof. The following is a
derivation with the three premises and last line
Now replace
In a cycle every condition reaches every other along
the arrows; longer cycles work the same way, with longer
chains of
Warning. Two arrows back and forth
are not a cycle through three conditions. Proving (a)
Let
- (a)
. - (b)
. - (c)
and .
Solution. By Proposition 2.4.6
it suffices to prove (a)
(a)
(b)
(c)
The order of the cycle was a choice, made so that
each arrow was short: (b)
2.4.7. The rule card
Before the card, the two rules at work on large statements.
| Rule | Letters replaced | Cited | New line |
|---|---|---|---|
| box |
|||
Not an instance. From two lines
Chapter 1’s seven rules are on the card at the end of Section 1.6; here are this chapter’s so far.
| Rule | Shape | You write | Lean |
|---|---|---|---|
| “…, which contradicts …” | exact hn hp (goal
False) |
||
| “This case cannot occur.” “So there is nothing to prove.” | exfalso |
||
| box |
“Suppose |
intro hp (goal False) |
|
| “Since |
mt h hnq |
||
| “We prove the contrapositive: suppose not |
mt |
||
| “ |
h.resolve_left hnp |
||
| box |
“ |
constructor |
|
| “Since |
h.mp hp / h.mpr hq |
The rows for this section’s rules complete the table
for the connectives. The Lean names in the last column
come from the two fields of an iff, mp
(“modus ponens”, left to right) and mpr
(right to left).
Warning (Not allowed:
- Close
with one box: clause 1, two boxes (a single box proves only). - In the second box, cite a line of the first: clause 2, the boxes are siblings (the pair below).
- Write
by from and : clause 4, needs one side itself; takes a box. - Write
by citing two implication lines: clause 3, the rule cites boxes, as ranges (the look-alike of Example (Instances of and )).
Clause 2 is where the rule bites: WRONG beside RIGHT,
with premises
The left list never cites premises 2 and 3, so it
would show
Remark (Looking ahead). Chapter 5
uses the lemma
2.4.8. Exercises
A. Check your understanding
- (a) State the rules
and , and the definition of . - (b) For a real
number
, consider “ if and only if or ”. Write the directions and as implications. Which one would a proof begin with “Suppose ”? - (c) True or false,
with a reason: from the definition “an integer
is even if there is an integer with ” and the fact that is even, we may conclude that for some integer . - (d) True or false,
with a reason: from the theorem “if
, then ” and the fact that , we may conclude that .
Solution.
(a)
: from a box and a box , both available, write . : from and either side, write the other (Definition 2.4.1). means and (Definition 2.4.2).(b)
: if , then or . : if or , then . The direction begins “Suppose ”, since it assumes the left side.(c) True. A definition’s “if” means “if and only if”, so the definition may be used from the term “even” to the condition, by
. (Indeed .)(d) False. A theorem’s “if” is one direction only, and the conclusion would be its converse. The converse fails at
: but .
The parts run from one step, through a missing line, a justification column and steps to judge, to short derivations.
(a) Lines 1
, 2 . What does “ 1, 2” write?(b) A box
runs from to , and a box from to . What does “ 3–6, 7–9” write?(c) Write “
if and only if or ” as two implications. Which begins “Suppose ”?(d) Definition: “an integer
is a multiple of 3 if for some integer ”. From , what follows, reading the definition which way?(e) Line 6 is
, justified “ 2, 5”, and line 2 is . What is line 5?(f) Line 12 is
, justified “ 4–7, 8–11”. What are lines 4, 7, 8 and 11?(g) Fill in the justifications (i)–(iv).
123 (i)4 (ii)5 (iii)6 (iv)(h) Lines 1
, 2 . Does give anything?(i) A box
runs from to ; a box from to , and line 6 cites line 3. Is “ — 2–4, 5–7” correct?(j) One box runs from
to . What does it prove?(k) True or false:
says no more than .(l) A proof that (a), (b), (c) are equivalent proves (a)
(b), (b) (a) and (b) (c). Is it complete?(m) Derive
.(n) Derive
.(o) Derive
.
Solution.
(a)
, by the second form.(b)
: the first box’s assumption on the left, its last line on the right.(c)
if , then or ; the converse. The direction begins “Suppose ”.(d)
is a multiple of , reading the definition from the condition to the term ( ).(e)
, the left side, so that the first form writes the right side .(f) Line 4 is
and line 7 is (the first box); line 8 is and line 11 is (the second).- (g)
- (i) assumption, for
; (ii) 1, 3; (iii) 2, 4; (iv) .
- (i) assumption, for
(h) No:
needs or itself. comes by a box, as in part (o).(i) No: line 6 cites line 3, inside the closed sibling box
.(j)
, by ; not .(k) False: it says
and , two derivations (equivalently ); is only half of it.(l) No: no arrow leaves (c). Add (c)
(a) or (c) (b).(m) 3
, 1, 2; 4 , 3, 2.(n) 4
, 2, 3; 5 , 1, 4.(o) 3
, assumption, for ; 4 , 1, 3; 5 , 4, 2; 6 , .
B. Practice
Show that
Solution. The goal is an iff, so we
open two boxes:
Lines 4 and 8 use
Let
Solution.
This proves the equivalence.
Let
- (a) Apply Theorem 2.4.5
with the roles of
and exchanged. What does it say? - (b) Use Example (Negating both sides of an iff)
as a derived rule on (a): with which statements in place
of
and , and what does it give? - (c) Translate both sides of (b) with the fact quoted.
- (d) What have you proved?
Solution.
(a) The exchange is allowed, since both numbers are non-negative:
if and only if .(b) With
: “ ” and : “ ”, Example (Negating both sides of an iff), used as a derived rule (Definition 2.3.1), gives: fails if and only if fails.(c) By the fact quoted, the left side says
and the right side says .(d) That
if and only if .
A search for
Solution. The move is two boxes
for an iff: the goal’s main connective is
The second box never cites a line of the first: line
10 gets
For real numbers
- (i)
and . - (ii)
or . - (iii) (
and ) or ( and ). - (iv)
. - (v)
fails and fails.
- (a) For each, say
whether it is too broad (it admits a triple
that should be excluded), too narrow (it excludes one that should be admitted), or right, giving a triple for each fault. - (b) A definition is read as an iff. Prove that (iii) and (iv) are equivalent.
- (c) Which candidates
would make “if
lies strictly between and , then lies strictly between and ” false? Give one triple that shows it for all of them.
Solution.
- (a)
- (i) Too narrow:
, , lies between and fails (i). It is not too broad: (i) gives one of the wanted orders.
- (i) Too narrow:
(ii) Too broad:
, , satisfies but does not lie between. And too narrow: , , lies between, but and both fail (the triple of (c)).(iii) Right: it lists the two possible orders.
(iv) Right, by (b).
(v) This is (i) in negative dress: by the convention of Section 2.1, “
fails” is and “ fails” is . So it is too narrow, by the same triple as (i), and needlessly negative.
- (b)
In the case , and , so the product is negative. In the case , and , so again the product is negative. The two cases are on (iii). Suppose the product is negative. Then neither factor is , and the two factors cannot have the same sign, since a product of two positive or of two negative numbers is positive. So , that is , or , that is . - (c) (i), (ii) and
(v). With
, , , each holds for the ends and fails for the ends (for (ii): , while neither nor ). A definition of “between” should not depend on the order of the two ends; (iii) and (iv) do not, since exchanging and exchanges the two disjuncts of (iii) and the two factors of (iv).
Marking scheme. (10 points) - 4: (a), one point each for (i) and (v) with a correct triple, one for (ii) with both triples (too broad and too narrow), and one for calling (iii) and (iv) right. - 4: (b), each direction 2; the second must say why the factors have opposite signs. - 2: (c), (i), (ii) and (v) with one triple.
Fatal error (0 for (b)): proving only one direction and calling the conditions equivalent.
Let
- (i)
is odd. - (ii)
is even. - (iii)
. - (iv)
is odd.
You may use Theorem 2.4.4
and the fact that
Solution. We prove the cycle (i)
(i)
(ii)
(iii)
(iv)
(Exercise B3 of Section 1.6 met the fact (i)
For the second question: (i)
Marking scheme. (10 points) - 1: a cycle through all four conditions, citing the argument of Proposition 2.4.6 or arguing that it suffices. - 8: 2 for each of the four arrows. - 1: the completion question.
Fatal errors (0 for the step): a “cycle” that omits a
condition; (iii)
For each claim, derive it with the rules of Chapter 1
and Sections 2.1–2.4, or break it by statements about a
real number
- (a)
. - (b)
. - (c)
. - (d)
. - (e)
. - (f)
. - (g)
. - (h)
.
Solution.
- (a) Derive. Two
boxes for the iff, and a case split inside each.
12
asm, for3 asm, for4 1, 35 46 asm, for7 68 2, 3–5, 6–79 asm, for10 asm, for11 1, 1012 1113 asm, for14 1315 9, 10–12, 13–1416 2–8, 9–15 (b) Break. Take
: “ ”, : “ ”, : “ ”. At , and are both true, so the premise is true; is true and false, so is false. The counterexample set (Definition 1.1.3) , is true at .(c) Derive.
12 asm, for3 1, 24 35 2–4(d) Break. Take
: “ ”, : “ ”, : “ ”. At , and are both false, so the premise is true, while is false, since is true and false. The counterexample set is true at .(e) Derive.
123 asm, for4 35 1, 46 2, 57 38 7, 69 3–8- (f) Derive.
12
asm, for3 24 1, 35 26 4, 57 2–6 (g) Break. Take
: “ ”, : “ ”. At , is false, since is, so the premise is true; is false and true, so is false. The counterexample set is true at .(h) Derive. Split on the second premise; in each case
supplies the other letter.
- (b) and (g) are the
converses of (a) and (f), and (d) replaces the
conclusion of (c) by its converse; each of the three
breaks. (a) is the
-twin of Exercise (B4: Both directions), with a case split inside each box.
Marking scheme. (16 points) For each
claim: 1 for the verdict; 1 for a derivation every line
of which checks, or for a choice of statements and one
value of
C. Going deeper
For integers
- (i)
; - (ii)
and ; - (iii)
.
You may use Theorem 2.1.3 and part (a) of Exercise (B3: The square root of three, used later).
Solution (Hint 1). Choose the order of the cycle so that each arrow is short. The two results you may use both pass from a square to the number itself.
Solution (Hint 2). Try (i)
Solution. We prove (i)
(i)
(iii)
(ii)
Marking scheme. (10 points) - 1:
names a cycle through all three conditions and cites Proposition 2.4.6
(or proves the needed implications explicitly). - 2: (i)
Fatal errors (0 for the step): a “cycle” that omits a
condition; using “
- (a) Suppose only
is assumed in Theorem 2.4.5, and is an arbitrary real number. The remark after it says that survives. Which steps of its proof use , and why is never needed? Refute with a new pair. - (b) Prove that for
all real numbers
and , if and only if .
Hint: for (b), apply Theorem 2.4.5 to the right pair of numbers.
Solution.
(a) The proof of
uses twice: for from , and for . Its other multiplication is by the derived , so is never used. For , take , : and , but .(b) Let
and be real numbers. Then and , so Theorem 2.4.5 applies to the pair , and gives if and only if . Finally , since is or and , and likewise . This proves that if and only if .