2.4  Iff, Equivalence, and What a Definition Says

One connective is still without rules: “if and only if”. Theorems say “n is odd if and only if n2 is odd”, and every definition, though written with a plain “if”, is used as an “if and only if”. Section 1.1 warned that “if” means different things in a theorem and in a definition; this section explains why. The one new thing here is the pair of rules for ↔; the rest of the section (provable equivalence, the layout of an “iff” proof, the convention about definitions, chains of equivalences) is what the rules are used for.

2.4.1. The rules for “if and only if”

“P if and only if Q” combines “P if Q”, which is Q→P, with “P only if Q”, which is P→Q, as Section 1.1 explained. A proof of it travels both ways; a use of it, either way. An implication is proved by a box, opened on the hypothesis and closed on the conclusion (Definition 1.4.1); an “if and only if” needs two such boxes.

An “if and only if” is two implications, and proving it takes two proofs.

Definition 2.4.1 (Rules for the Biconditional)
iφasm, for ↔I
⋮
jψ
kψasm, for ↔I
⋮
lφ
mφ↔ψ↔I i–j, k–l
iφ↔ψ
jφ
kψ↔E i, j
iφ↔ψ
jψ
kφ↔E i, j

The first schema is the rule ↔I (iff-introduction); its two assumptions are discharged when their boxes close, and each box’s last line (ψ in the first, φ in the second) is a line of that box itself, not of a box inside it. The two schemas below it are the two forms of ↔E (iff-elimination).

As in every schema (Definition 1.2.1), φ and ψ stand for any statements, replaced consistently, and i,j,k,l,m for line numbers. Read the rules clause by clause.

  1. Two boxes. ↔I 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 →I 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 ↔I”; in a written proof the two boxes are the paragraphs (⇒) and (⇐).
  2. 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.
  3. Citation. The justification cites both boxes as ranges, as in ↔I 2–4,5–7.
  4. Elimination, either way. From φ↔ψ and φ on available lines, ↔E writes ψ; from φ↔ψ and ψ, it writes φ. It is modus ponens in whichever direction we need, citing the biconditional first.

In the Givens/Goal table, ↔I splits a row in two: φ added to the Givens with the goal ψ, and ψ added with the goal φ.

2.4.2. First derivations with iff

The section’s goal-directed move: a goal φ↔ψ opens two boxes, one on each side, and each box’s goal is the other side.

Example (An iff read both ways)
  • (a) Show that P↔Q⊢Q↔P.
  • (b) Show that P↔Q,¬Q⊢¬P.

Solution.

  • (a) Idea. The goal is an iff, so the last line is ↔I, and we need a box from Q to P and a box from P to Q. Each box’s goal is one ↔E away: the premise crosses from its assumption to the other side.

    The goal at the foot (left), then its two boxes (right).

    1P↔Q
    ⋮
    6Q↔P
    1P↔Q
    2Qasm, for ↔I
    ⋮
    3P
    4Pasm, for ↔I
    ⋮
    5Q
    6Q↔P↔I 2–3, 4–5

    The finished derivation:

    1P↔Q
    2Qasm, for ↔I
    3P↔E 1, 2
    4Pasm, for ↔I
    5Q↔E 1, 4
    6Q↔P↔I 2–3, 4–5

    Line 3 uses the second form of ↔E (right to left), line 5 the first.

  • (b) Idea. The goal ¬P is a negation, so open a box on P and aim at ⊥ (Section 2.2). Inside, the premise P↔Q turns P into Q, and Q clashes with ¬Q.
1P↔Q
2¬Q
3Pasm, for ¬I
4Q↔E 1, 3
5⊥¬E 4, 2
6¬P¬I 3–5

This is the derivation of Proposition 2.3.1 with ↔E on line 4: if two statements are equivalent and one fails, so does the other.

The rules say nothing that the two implications do not say. The next result makes this exact.

Proposition 2.4.1 (An Iff Is Two Implications)

P↔Q⊢(P→Q)∧(Q→P), and (P→Q)∧(Q→P)⊢P↔Q.

Idea. Each goal chooses its rule. For the first, the goal is a conjunction of two implications: ∧I needs both, and each is built in its own →I box, crossing the premise with ↔E inside. For the second, the goal is an iff: open its two boxes. The premise is a conjunction, so take it apart first (premise-directed), and cross each box with one of its halves by →E.

First claim: the two implications as goals (left), then their boxes (right).

1P↔Q
⋮
4P→Q
⋮
7Q→P
8(P→Q)∧(Q→P)∧I 4, 7
1P↔Q
2Pasm, for →I
⋮
3Q
4P→Q→I 2–3
5Qasm, for →I
⋮
6P
7Q→P→I 5–6
8(P→Q)∧(Q→P)∧I 4, 7

Second claim: the premise taken apart (left), then the two boxes (right).

1(P→Q)∧(Q→P)
2P→Q∧E 1
3Q→P∧E 1
⋮
8P↔Q
1(P→Q)∧(Q→P)
2P→Q∧E 1
3Q→P∧E 1
4Pasm, for ↔I
⋮
5Q
6Qasm, for ↔I
⋮
7P
8P↔Q↔I 4–5, 6–7

Proof. For the first claim, the following is a derivation with premise P↔Q and last line (P→Q)∧(Q→P).

1P↔Q
2Pasm, for →I
3Q↔E 1, 2
4P→Q→I 2–3
5Qasm, for →I
6P↔E 1, 5
7Q→P→I 5–6
8(P→Q)∧(Q→P)∧I 4, 7

For the second claim, the following is a derivation with premise (P→Q)∧(Q→P) and last line P↔Q.

1(P→Q)∧(Q→P)
2P→Q∧E 1
3Q→P∧E 1
4Pasm, for ↔I
5Q→E 2, 4
6Qasm, for ↔I
7P→E 3, 6
8P↔Q↔I 4–5, 6–7

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 ↔ could have been an abbreviation for (P→Q)∧(Q→P). We keep it as a connective with its own rules, so that every connective is proved by an introduction rule and used by an elimination rule.

Example (Negating both sides of an iff)

Show that P↔Q⊢¬P↔¬Q.

Solution. Idea. The goal is an iff, so there are two boxes, one opened by ¬P and reaching ¬Q, the other the reverse. Each box’s goal is a negation, so each contains a ¬I box: the goal-directed move applied twice, one inside the other. Inside the inner box, ↔E crosses from one side of the premise to the other, and the result clashes with the outer assumption. The second half is part (b) of Example (An iff read both ways), run inside a box; the first is its mirror image, with the other form of ↔E.

The outer boxes (left), then a ¬I box inside each (right).

1P↔Q
2¬Pasm, for ↔I
⋮
6¬Q
7¬Qasm, for ↔I
⋮
11¬P
12¬P↔¬Q↔I 2–6, 7–11
1P↔Q
2¬Pasm, for ↔I
3Qasm, for ¬I
⋮
5⊥
6¬Q¬I 3–5
7¬Qasm, for ↔I
8Pasm, for ¬I
⋮
10⊥
11¬P¬I 8–10
12¬P↔¬Q↔I 2–6, 7–11

The finished derivation:

1P↔Q
2¬Pasm, for ↔I
3Qasm, for ¬I
4P↔E 1, 3
5⊥¬E 4, 2
6¬Q¬I 3–5
7¬Qasm, for ↔I
8Pasm, for ¬I
9Q↔E 1, 8
10⊥¬E 9, 7
11¬P¬I 8–10
12¬P↔¬Q↔I 2–6, 7–11

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 ¬φ, and why may it?

Solution. Line 2, ¬P, the assumption of the outer box 2–6, which is still open at line 5.

The derivation uses only the rules of this section and of Sections 2.1–2.2. Its converse, ¬P↔¬Q⊢P↔Q, is also derivable, with the rule of Section 2.5: in the box of P it must produce the positive statement Q, and the natural box, on ¬Q, closes to ¬¬Q, not Q.

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?

Lemma 2.4.2 (No Statement Is Equivalent to Its Negation)

⊢¬(P↔¬P).

Idea. The goal is a negation: open a ¬I box on P↔¬P, with goal ⊥. ↔E needs one side of the iff on a line, and neither is. So make ¬P a subgoal, by a ¬I box on P: inside it ↔E gives ¬P, which clashes with P. With ¬P in hand, ↔E the other way gives P, and the two clash again.

The outer box (left), then the subgoal ¬P with its box (right).

1P↔¬Pasm, for ¬I
⋮
7⊥
8¬(P↔¬P)¬I 1–7
1P↔¬Pasm, for ¬I
2Pasm, for ¬I
⋮
4⊥
5¬P¬I 2–4
⋮
7⊥
8¬(P↔¬P)¬I 1–7

Proof. The following is a derivation with no premises and last line ¬(P↔¬P).

1P↔¬Pasm, for ¬I
2Pasm, for ¬I
3¬P↔E 1, 2
4⊥¬E 2, 3
5¬P¬I 2–4
6P↔E 1, 5
7⊥¬E 6, 5
8¬(P↔¬P)¬I 1–7

Line 5 may be cited at lines 6 and 7: it lies in the box 1–7, as they do. No rule of Section 2.5 is used.

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 x be a real number. The sentence “x>0 if and only if x≤0” is false whatever x is: by the convention of Section 2.1, x≤0 is ¬(x>0), so the sentence is an instance of P↔¬P, and the lemma, used as a derived rule, refutes every instance.

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 P (line 2) to the right side ¬P; and line 6, from the right side ¬P (line 5) back to the left side P.

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.

Definition 2.4.2 (Provable Equivalence)

Statements P and Q are provably equivalent, written P⊣⊢Q, if P⊢Q and Q⊢P.

In words: there is a derivation with premise P and last line Q, and another with premise Q and last line P. The symbol is the turnstile of Definition 1.2.3 written twice, back to back; two derivations prove the claim.

A first example is P∧Q⊣⊢Q∧P: Proposition 1.2.1 derives Q∧P from P∧Q, and the same derivation with P and Q exchanged derives P∧Q from Q∧P. By the same exchange, Example (First derivations with “or”) gives P∨Q⊣⊢Q∨P, and part (a) of Example (An iff read both ways) gives P↔Q⊣⊢Q↔P.

Second readingEdge cases of provable equivalence

The degenerate example is P⊣⊢P: the one-line derivation of part (a) of Example (Derivations, simplest first) serves in both directions.

A minimal change gives a one-way street. Example (Two negations from one premise) derived P⊢¬¬P, but the converse, ¬¬P⊢P, would have to remove two negations, and no rule met so far removes one. So we cannot claim P⊣⊢¬¬P: the clause “Q⊢P” is the one missing. (It holds once Section 2.5 adds its rule.) Likewise Proposition 2.3.2 derives ¬Q→¬P from P→Q, but not yet the reverse.

The connective ↔ and the relation ⊣⊢ are two sides of one idea; the next result makes the link exact, and shows that ⊣⊢ behaves as an equivalence should.

Proposition 2.4.3 (Provable Equivalence and the Biconditional)

For all statements P, Q, R:

  • (a) P⊣⊢Q if and only if ⊢P↔Q;
  • (b) P⊣⊢P; if P⊣⊢Q, then Q⊣⊢P; and if P⊣⊢Q and Q⊣⊢R, then P⊣⊢R.

In words: one derivation of P↔Q from no premises is worth two derivations, one each way; and ⊣⊢ can be used like = in a calculation.

Second readingThe proof: copying derivations

Idea. Everything here moves whole derivations around. To prove ⊢P↔Q, the two boxes of ↔I are the two given derivations, with their premises turned into the boxes’ assumptions. To use ⊢P↔Q, write out its derivation and apply ↔E. For transitivity, run one derivation into the next: the last line of the first is the premise of the second.

Proof. We use one observation twice. Let D be a derivation, and copy its lines, in order and with their numbers shifted, to some place in another derivation, with every line of the copy inside the same boxes as that place. Then every citation inside the copy is still available: if line i of D is available at line k of D, every box of D containing line i contains line k, and the boxes added around the copy contain both lines. Closed boxes cited in D are handled the same way. So each copied line is justified by the same rule as before.

(⇒) in (a). Suppose P⊢Q and Q⊢P, by derivations D1 and D2. Build a derivation with no premises as follows. Open a box with the assumption P and, below it, copy D1, turning each of its premise lines P into a repetition of the assumption by (D3) of Definition 1.4.2. By the observation, the copy is justified, and its last line Q is a line of the box itself, since the last line of D1 lies in none of D1’s boxes. Close the box. Open a second box with Q, copy D2 in the same way, and close it on P. Then ↔I on the two boxes gives P↔Q. So ⊢P↔Q.

(⇐) in (a). Suppose ⊢P↔Q, by a derivation D with no premises. For P⊢Q, start with the premise P, copy D below it, and write Q by ↔E from the last line of the copy, P↔Q, and line 1. Both cited lines lie in no box, so both are available. For Q⊢P, do the same with premise Q, using the other form of ↔E. So P⊣⊢Q.

  • (b) The one-line derivation consisting of the premise P shows P⊢P, in both directions, so P⊣⊢P. Symmetry holds because Definition 2.4.2 says the same thing about P,Q as about Q,P. For transitivity it is enough to show that P⊢Q and Q⊢R give P⊢R, since the reverse direction is the same statement with P and R exchanged. Take a derivation D1 of Q from P, and below its last line copy a derivation D2 of R from Q, turning each premise line Q of D2 into a repetition of the last line of D1. 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 P and last line R. 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
P∧Q⊣⊢Q∧P Proposition 1.2.1, with the letters exchanged for the converse
P∨Q⊣⊢Q∨P Example (First derivations with “or”), likewise
(P∧Q)→R⊣⊢P→(Q→R) Proposition 1.4.2
P∧(Q∨R)⊣⊢(P∧Q)∨(P∧R) Proposition 1.6.1
(P→R)∧(Q→R)⊣⊢(P∨Q)→R Example (Cases on a hypothesis are two implications) and Example (A disjunctive hypothesis splits into two implications)
P↔Q⊣⊢(P→Q)∧(Q→P) Proposition 2.4.1
P↔Q⊣⊢Q↔P Example (An iff read both ways) (a), with the letters exchanged
¬¬¬P⊣⊢¬P Example (Three negations become one), and Example (Two negations from one premise) (a) with ¬P for P

The fourth row is distributivity of ∧ over ∨ as a provable equivalence. Some familiar laws are not in the table, because the text has derived them in one direction only; associativity of ∨ is one (Example (Regrouping a disjunction)).

Warning. A sequent in one direction is not an equivalence. P∧Q⊢P holds by ∧E, but the form “from P conclude P∧Q” breaks: take P: “2>1” and Q: “1>2”, and the premise is true while the conclusion is false. Before writing ⊣⊢, check that both derivations exist.

2.4.4. Proving an iff: two directions

In a written proof, the two boxes of ↔I become two paragraphs: (⇒) assumes the left side and reaches the right, (⇐) the reverse. Neither may borrow the other’s assumption: they are two separate boxes.

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.

Theorem 2.4.4 (Odd Square, Odd Number)

Let n be an integer. Then n is odd if and only if n2 is odd.

Idea. Two boxes. Forwards is (E3). Backwards, “n2 is odd” gives nothing to compute with, so split on (E1) and show the even case impossible, as in Example (An impossible case).

Proof. (⇒) This is (E3).

(⇐) Suppose n2 is odd [assumption for the second box]. By (E1), n is even or odd, and we argue by cases [∨E]. If n is odd, we are done. If n is even, say n=2k with k an integer, then n2=2(2k2) is even; so n2 is both even and odd [∧I], which contradicts (E2) [¬E]. So this case cannot occur, and n is odd in it too [⊥E]. In both cases n is odd.

This proves the theorem [↔I].

With the derived rules of Section 2.3, (⇐) fits in one breath, “n cannot be even, since then n2 would be even; so n is odd”: ¬I with (E2), then MT, then DS on (E1).

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.

Theorem 2.4.5 (Squaring Preserves Order)

Let x and y be real numbers with x≥0 and y≥0. Then x≤y⟺x2≤y2.

Idea. Forwards, multiply x≤y by x≥0 and by y≥0, and chain. Backwards, nothing undoes squaring without square roots, so we split instead: either x≤y, which is the goal, or y<x. In the second case the forward argument, run with a strict inequality, gives y2<x2, which clashes with the hypothesis: an impossible case, closed by ⊥E.

Proof. (⇒) Suppose x≤y. Multiplying by x≥0 gives x2≤xy, and multiplying by y≥0 gives xy≤y2. Hence x2≤y2.

(⇐) Suppose x2≤y2. For real numbers, x≤y or y<x, and we argue by cases [∨E]. If x≤y, we are done. If y<x, then x>y≥0, so x>0. Multiplying y<x by x>0 gives xy<x2, and multiplying y<x by y≥0 gives y2≤xy. Hence y2<x2, which contradicts x2≤y2 [¬E]; so this case cannot occur, and x≤y holds in it [⊥E]. In both cases x≤y.

This proves the theorem [↔I].

Remark. Each hypothesis has a job. The direction (⇒) needs x≥0, and fails without it: x=−2, y=1 gives x≤y but x2=4>1=y2. (Its proof also multiplied by y≥0, but there y≥0 already follows from y≥x≥0.) The direction (⇐) used only y≥0, and fails without it: x=1, y=−2 gives x2=1≤4=y2 but x>y.

A payoff comes at once. For a,b≥0, apply Theorem 2.4.5 to x=a and y=b: a≤b if and only if a≤b. Taking square roots preserves order, a fact used constantly in estimates. (That square roots of non-negative numbers exist is a school fact here.)

Quick check. Here is a proof of the statement “for a real number x, x2=1 if and only if x=1 or x=−1”.

If x=1, then x2=1⋅1=1. If x=−1, then x2=(−1)(−1)=1. This proves the claim.

Which direction has been proved, and which is missing? Supply the missing one.

Solution. The proof assumes the right side, “x=1 or x=−1”, splits it into its two cases, and reaches x2=1 in both. So it proves (⇐), by ∨E. The direction (⇒) is missing.

(⇒) Suppose x2=1. Then (x−1)(x+1)=x2−1=0. A product of real numbers is zero only if one of the factors is zero, so x−1=0 or x+1=0, that is, x=1 or x=−1.

Warning. A proof of an iff can prove one direction twice and look complete. For “n is odd if and only if n2 is odd”, a proof that shows “if n is odd, then n2 is odd” and then “if n2 is not odd, then n is not odd” has proved (⇒) and its contrapositive (Proposition 2.3.2), which is (⇒) again. The direction (⇐), “if n2 is odd, then n is odd”, is still missing; its contrapositive would be “if n is not odd, then n2 is not odd”. Before writing “this proves the theorem”, check that one paragraph assumes each side.

2.4.5. What a definition says

Here is a definition written the way this book and most others write definitions.

A function f:R→R is strictly increasing if, for all real numbers x and y, x<y implies f(x)<f(y).

Grammatically the sentence is an implication, “f is strictly increasing if [condition]”, and read as a theorem it would allow only one move, from the condition to the term. But a definition is not a theorem. It introduces a new term, and the new term means exactly the condition: no more, since nothing else was said about the term, and no less, since the condition is all the term was made to express. So the definition is used in both directions, as an ↔ between the term and the condition, and ↔E is how it is used.

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 :⇔ in definitions; this book, like most, writes “if” and puts the term defined in bold, which signals that the “if” is an “iff”. Here it is used three ways.

Example (A definition used in both directions)
  • (a) Show that f(x)=3x−5 defines a strictly increasing function f:R→R.
  • (b) Suppose g:R→R is strictly increasing. Show that g(1)<g(2).
  • (c) Show that h(x)=x2 does not define a strictly increasing function h:R→R.

Solution.

  • (a) Let x and y be real numbers with x<y. Multiplying by 3>0 gives 3x<3y, and subtracting 5 gives 3x−5<3y−5, that is, f(x)<f(y). So f satisfies the condition, and by the definition, read from right to left, f is strictly increasing [↔E].

  • (b) Since g is strictly increasing, the definition, read from left to right, says that x<y implies g(x)<g(y) for all real x and y [↔E]. Taking x=1 and y=2, and using 1<2, we get g(1)<g(2) [→E].

  • (c) Suppose h were strictly increasing [assumption for ¬I]. By the definition read from left to right, as in (b), −1<0 would give h(−1)<h(0), that is, 1<0, which is false [¬E]. So h is not strictly increasing [¬I].

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 “x<y implies f(x)≤f(y)”, it would be too broad: the constant function f(x)=0 would count as strictly increasing. Had it said “x<y implies f(y)−f(x)≥1”, it would be too narrow: f(x)=x would not count, since 0<12 and 12−0<1.

Warning. The convention is for definitions only. In a theorem, “if” means “if”, one direction. The theorem “if 6∣n, then n is even” is true for every integer n: n=6k=2(3k). Its converse, “if n is even, then 6∣n”, breaks at n=4. Reading a theorem’s “if” as “iff” means proving its converse without a proof, which is the error of Argument B in Section 1.1.

Second readingThe same slip in calculus

A familiar theorem of calculus says: if f is differentiable at a, then f is continuous at a. Its converse is false. The function f(x)=|x| is continuous at 0, but it is not differentiable there, since its graph has a corner: the quotient |h|/h is 1 for h>0 and −1 for h<0.

Quick check. Write the converse of “if a real number x satisfies x>2, then x2>4”, and break it.

Solution. The converse is “if x2>4, then x>2”. The value x=−3 breaks it: (−3)2=9>4, and −3>2 fails.

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: (a)⇒(b)⇒(c)⇒(a). Once the cycle is proved, any condition leads to any other by following the arrows round. Here is the derivation behind that sentence.

Proposition 2.4.6 (Proving Equivalence by a Cycle)

P→Q,Q→R,R→P⊢P↔Q. Likewise, from the same three premises, Q↔R and R↔P are derivable.

Idea. The goal is an iff, so there are two boxes. From P, one step along the cycle reaches Q. From Q, the cycle reaches P the long way round, through R: a backward chain of →E, as in Section 1.3. The other two equivalences need no new work, because the three premises do not change when the letters are rotated.

The goal at the foot (left), then its two boxes (right).

1P→Q
2Q→R
3R→P
⋮
9P↔Q
1P→Q
2Q→R
3R→P
4Pasm, for ↔I
⋮
5Q
6Qasm, for ↔I
⋮
8P
9P↔Q↔I 4–5, 6–8

Proof. The following is a derivation with the three premises and last line P↔Q.

1P→Q
2Q→R
3R→P
4Pasm, for ↔I
5Q→E 1, 4
6Qasm, for ↔I
7R→E 2, 6
8P→E 3, 7
9P↔Q↔I 4–5, 6–8

Now replace P, Q, R throughout by Q, R, P respectively. The premises P→Q, Q→R, R→P become Q→R, R→P, P→Q, the same three statements in a different order, and every line remains justified by the same rule, since the letters stood for any statements (as in clause 2 after Definition 2.3.1). So the renamed derivation derives Q↔R from the same premises. Rotating once more gives R↔P. This proves the proposition.

In a cycle every condition reaches every other along the arrows; longer cycles work the same way, with longer chains of →E in the boxes.

Warning. Two arrows back and forth are not a cycle through three conditions. Proving (a) ⇒ (b) and (b) ⇒ (a) shows that (a) and (b) are equivalent and says nothing about (c): no arrow enters or leaves it. For a real number x, take (a) “x>0”, (b) “2x>0”, and (c) “x>1”. Both arrows between (a) and (b) are true, and (c) is not equivalent to them: x=12 satisfies (a) and (b) but not (c). Every condition in the list must lie on the cycle.

Example (Three descriptions of the unit interval)

Let x be a real number. Prove that the following are equivalent.

  • (a) 0<x<1.
  • (b) x2<x.
  • (c) x>0 and 1/x>1.

Solution. By Proposition 2.4.6 it suffices to prove (a) ⇒ (b) ⇒ (c) ⇒ (a).

(a) ⇒ (b). Suppose 0<x<1. Multiplying x<1 by x>0 gives x2<x.

(b) ⇒ (c). Suppose x2<x. First, x>0: otherwise x≤0, and then x≤0≤x2, so x≤x2, which contradicts x2<x. (In rules: we have x≤0 or x>0; the first is refuted by a ¬I box, and DS (Proposition 2.3.4) leaves the second.) Since x>0, we may divide x2<x by x, which gives x<1, and then divide x<1 by x, which gives 1<1/x. So x>0 and 1/x>1.

(c) ⇒ (a). Suppose x>0 and 1/x>1. Multiplying 1<1/x by x>0 gives x<1. So 0<x<1.

The order of the cycle was a choice, made so that each arrow was short: (b) ⇒ (c) carried the only case split. The reverse cycle would also do, with different arrows to prove.

2.4.7. The rule card

Before the card, the two rules at work on large statements.

Example (Instances of ↔I and ↔E)
Rule Letters replaced Cited New line
↔I φ:=P∧Q, ψ:=Q∧P box P∧Q … Q∧P, box Q∧P … P∧Q (P∧Q)↔(Q∧P)
↔E φ:=¬P, ψ:=Q→R ¬P↔(Q→R), Q→R ¬P (the second form)
↔E φ:=P∨Q, ψ:=¬R (P∨Q)↔¬R, P∨Q ¬R

Not an instance. From two lines P→Q and Q→P, the line “P↔Q — ↔I” is not an instance: ↔I cites two boxes, not two implications. The two lines give the iff through Proposition 2.4.1 used as a derived rule (after ∧I), or by opening the two boxes.

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
¬E φ, ¬φ ⟹ ⊥ “…, which contradicts …” exact hn hp (goal False)
⊥E ⊥ ⟹ any φ “This case cannot occur.” “So there is nothing to prove.” exfalso
¬I box φ … ⊥ ⟹ ¬φ “Suppose P. … This is a contradiction. Hence not P.” intro hp (goal False)
MT φ→ψ, ¬ψ ⟹ ¬φ (derived) “Since Q fails, so does P.” mt h hnq
CP φ→ψ ⟹ ¬ψ→¬φ (derived) “We prove the contrapositive: suppose not Q; … so not P.” mt
DS φ∨ψ, ¬φ ⟹ ψ (derived) “P is impossible, so Q.” h.resolve_left hnp
↔I box φ … ψ, box ψ … φ ⟹ φ↔ψ “(⇒) Suppose P. … so Q. (⇐) Suppose Q. … so P.” constructor
↔E φ↔ψ, φ ⟹ ψ (or with ψ, φ) “Since P holds if and only if Q does, and P holds, so does Q.” 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: ↔I and ↔E). Each step below is wrong; the tag names the clause it breaks.

  • Close ↔I 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 ↔E from φ↔ψ and ¬φ: clause 4, ↔E needs one side itself; ¬ψ takes a ¬I box.
  • Write φ↔ψ by ↔I citing two implication lines: clause 3, the rule cites boxes, as ranges (the look-alike of Example (Instances of ↔I and ↔E)).

Clause 2 is where the rule bites: WRONG beside RIGHT, with premises P→Q, R and (Q∧R)→P. On the left, line 7 copies P from the closed first box.

1P→Q
2R
3(Q∧R)→P
4Pasm, for ↔I
5Q→E 1, 4
6Qasm, for ↔I
7PR 4
8P↔Q↔I 4–5, 6–7
1P→Q
2R
3(Q∧R)→P
4Pasm, for ↔I
5Q→E 1, 4
6Qasm, for ↔I
7Q∧R∧I 6, 2
8P→E 3, 7
9P↔Q↔I 4–5, 6–8

The left list never cites premises 2 and 3, so it would show P→Q⊢P↔Q, which breaks: with P: “x>5” and Q: “x>3”, at x=4 the premise is true and P↔Q is false.

Remark (Looking ahead). Chapter 5 uses the lemma ¬(P↔¬P) to show that no barber can shave exactly those who do not shave themselves, and in what sense no set can contain exactly the sets that do not contain themselves. Analysis on the Real Line, Chapter 1 proves from its axioms that every non-negative real number has a square root, the school fact behind the square-root payoff above.

2.4.8. Exercises

A. Check your understanding

Exercise (A1)
  • (a) State the rules ↔I and ↔E, and the definition of P⊣⊢Q.
  • (b) For a real number x≥0, consider “x2=x if and only if x=0 or x=1”. Write the directions (⇒) and (⇐) as implications. Which one would a proof begin with “Suppose x2=x”?
  • (c) True or false, with a reason: from the definition “an integer n is even if there is an integer k with n=2k” and the fact that 10 is even, we may conclude that 10=2k for some integer k.
  • (d) True or false, with a reason: from the theorem “if x>1, then x2>1” and the fact that x2>1, we may conclude that x>1.

Solution.

  • (a) ↔I: from a box φ…ψ and a box ψ…φ, both available, write φ↔ψ. ↔E: from φ↔ψ and either side, write the other (Definition 2.4.1). P⊣⊢Q means P⊢Q and Q⊢P (Definition 2.4.2).

  • (b) (⇒): if x2=x, then x=0 or x=1. (⇐): if x=0 or x=1, then x2=x. The direction (⇒) begins “Suppose x2=x”, 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 ↔E. (Indeed k=5.)

  • (d) False. A theorem’s “if” is one direction only, and the conclusion would be its converse. The converse fails at x=−2: x2=4>1 but x<1.

Exercise (A2: Drill)

The parts run from one step, through a missing line, a justification column and steps to judge, to short derivations.

  • (a) Lines 1 P↔Q, 2 Q. What does “↔E 1, 2” write?

  • (b) A box 3–6 runs from P∨Q to ¬R, and a box 7–9 from ¬R to P∨Q. What does “↔I 3–6, 7–9” write?

  • (c) Write “x2=4 if and only if x=2 or x=−2” as two implications. Which begins “Suppose x2=4”?

  • (d) Definition: “an integer n is a multiple of 3 if n=3k for some integer k”. From 12=3⋅4, what follows, reading the definition which way?

  • (e) Line 6 is Q∧R, justified “↔E 2, 5”, and line 2 is P↔(Q∧R). What is line 5?

  • (f) Line 12 is ¬P↔Q, justified “↔I 4–7, 8–11”. What are lines 4, 7, 8 and 11?

  • (g) Fill in the justifications (i)–(iv).

    1P↔¬Q
    2Q
    3P(i)
    4¬Q(ii)
    5⊥(iii)
    6¬P(iv)
  • (h) Lines 1 P↔Q, 2 ¬P. Does ↔E give anything?

  • (i) A box 2–4 runs from P to Q; a box 5–7 from Q to P, and line 6 cites line 3. Is “P↔Q — ↔I 2–4, 5–7” correct?

  • (j) One box runs from P to Q. What does it prove?

  • (k) True or false: P⊣⊢Q says no more than ⊢P→Q.

  • (l) A proof that (a), (b), (c) are equivalent proves (a) ⇒ (b), (b) ⇒ (a) and (b) ⇒ (c). Is it complete?

  • (m) Derive P↔Q, P⊢Q∧P.

  • (n) Derive P↔Q, Q↔R, R⊢P.

  • (o) Derive P↔Q, ¬P⊢¬Q.

Solution.

  • (a) P, by the second form.

  • (b) (P∨Q)↔¬R: the first box’s assumption on the left, its last line on the right.

  • (c) (⇒) if x2=4, then x=2 or x=−2; (⇐) the converse. The direction (⇒) begins “Suppose x2=4”.

  • (d) 12 is a multiple of 3, reading the definition from the condition to the term (↔E).

  • (e) P, the left side, so that the first form writes the right side Q∧R.

  • (f) Line 4 is ¬P and line 7 is Q (the first box); line 8 is Q and line 11 is ¬P (the second).

  • (g)
    • (i) assumption, for ¬I; (ii) ↔E 1, 3; (iii) ¬E 2, 4; (iv) ¬I 3–5.
  • (h) No: ↔E needs P or Q itself. ¬Q comes by a ¬I box, as in part (o).

  • (i) No: line 6 cites line 3, inside the closed sibling box 2–4.

  • (j) P→Q, by →I; not P↔Q.

  • (k) False: it says P⊢Q and Q⊢P, two derivations (equivalently ⊢P↔Q); ⊢P→Q is only half of it.

  • (l) No: no arrow leaves (c). Add (c) ⇒ (a) or (c) ⇒ (b).

  • (m) 3 Q, ↔E 1, 2; 4 Q∧P, ∧I 3, 2.

  • (n) 4 Q, ↔E 2, 3; 5 P, ↔E 1, 4.

  • (o) 3 Q, assumption, for ¬I; 4 P, ↔E 1, 3; 5 ⊥, ¬E 4, 2; 6 ¬Q, ¬I 3–5.

B. Practice

Exercise (B1: Iff is transitive)

Show that P↔Q,Q↔R⊢P↔R.

Solution. The goal is an iff, so we open two boxes: P to R, and R to P. In each, the premises are used as bridges, one after the other, by ↔E.

1P↔Q
2Q↔R
3Pasm, for ↔I
4Q↔E 1, 3
5R↔E 2, 4
6Rasm, for ↔I
7Q↔E 2, 6
8P↔E 1, 7
9P↔R↔I 3–5, 6–8

Lines 4 and 8 use P↔Q in opposite directions, as do lines 5 and 7 with Q↔R.

Exercise (B2: A parity equivalence)

Let n be an integer. Prove that n is even if and only if n+3 is odd.

Solution. (⇒) Suppose n is even, say n=2k with k an integer. Then n+3=2k+2+1=2(k+1)+1, and k+1 is an integer, so n+3 is odd.

(⇐) Suppose n+3 is odd, say n+3=2j+1 with j an integer. Then n=2j−2=2(j−1), and j−1 is an integer, so n is even.

This proves the equivalence.

Exercise (B3: Strict inequalities)

Let x and y be real numbers with x≥0 and y≥0. Deduce from Theorem 2.4.5 and Example (Negating both sides of an iff) that x<y if and only if x2<y2. You may use that, for real numbers a and b, a<b holds exactly when b≤a fails.

  • (a) Apply Theorem 2.4.5 with the roles of x and y 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 P and Q, 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: y≤x if and only if y2≤x2.

  • (b) With P: “y≤x” and Q: “y2≤x2”, Example (Negating both sides of an iff), used as a derived rule (Definition 2.3.1), gives: y≤x fails if and only if y2≤x2 fails.

  • (c) By the fact quoted, the left side says x<y and the right side says x2<y2.

  • (d) That x<y if and only if x2<y2.

Exercise (B4: Both directions)

A search for P↔Q⊢(P∧R)↔(Q∧R) has reached the stage below. Name the move, then complete it.

1P↔Q
⋮
12(P∧R)↔(Q∧R)?

Solution. The move is two boxes for an iff: the goal’s main connective is ↔, so line 12 will be ↔I, with a box from P∧R to Q∧R and a box back. Inside each, take the conjunction apart, cross with ↔E, and rebuild.

1P↔Q
2P∧Rasm, for ↔I
3P∧E 2
4R∧E 2
5Q↔E 1, 3
6Q∧R∧I 5, 4
7Q∧Rasm, for ↔I
8Q∧E 7
9R∧E 7
10P↔E 1, 8
11P∧R∧I 10, 9
12(P∧R)↔(Q∧R)↔I 2–6, 7–11

The second box never cites a line of the first: line 10 gets P afresh from line 8.

Exercise (B5: Criticize the definition)

For real numbers a, b, x, we want to define “x lies strictly between a and b”, meaning that one of a, b is less than x and x is less than the other. Here are five candidate conditions.

  • (i) a<x and x<b.
  • (ii) a<x or x<b.
  • (iii) (a<x and x<b) or (b<x and x<a).
  • (iv) (x−a)(x−b)<0.
  • (v) x≤a fails and b≤x fails.
  • (a) For each, say whether it is too broad (it admits a triple a,b,x 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 x lies strictly between a and b, then x lies strictly between b and a” false? Give one triple that shows it for all of them.

Solution.

  • (a)
    • (i) Too narrow: a=5, b=2, x=3 lies between and fails (i). It is not too broad: (i) gives one of the wanted orders.
  • (ii) Too broad: a=2, b=5, x=100 satisfies 2<100 but does not lie between. And too narrow: a=5, b=2, x=3 lies between, but 5<3 and 3<2 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, “x≤a fails” is a<x and “b≤x fails” is x<b. So it is too narrow, by the same triple as (i), and needlessly negative.

  • (b) (⇒) In the case a<x<b, x−a>0 and x−b<0, so the product is negative. In the case b<x<a, x−a<0 and x−b>0, so again the product is negative. The two cases are ∨E on (iii).

    (⇐) Suppose the product is negative. Then neither factor is 0, and the two factors cannot have the same sign, since a product of two positive or of two negative numbers is positive. So x−a>0>x−b, that is a<x<b, or x−a<0<x−b, that is b<x<a.

  • (c) (i), (ii) and (v). With a=2, b=5, x=3, each holds for the ends 2,5 and fails for the ends 5,2 (for (ii): 2<3, while neither 5<3 nor 3<2). A definition of “between” should not depend on the order of the two ends; (iii) and (iv) do not, since exchanging a and b 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.

Exercise (B6: Four conditions, one cycle)

Let n be an integer. Prove by one cycle of four implications that the following are equivalent.

  • (i) n is odd.
  • (ii) n+1 is even.
  • (iii) 8∣n2−1.
  • (iv) n2 is odd.

You may use Theorem 2.4.4 and the fact that k(k−1) is even for every integer k. Then: a proof that proved only (i) ⇔ (ii) and (iii) ⇔ (iv) would be incomplete; which two implications would complete it most cheaply?

Solution. We prove the cycle (i) ⇒ (ii) ⇒ (iii) ⇒ (iv) ⇒ (i). It suffices by the argument of Proposition 2.4.6: for any two conditions, each reaches the other by a chain of →E along the arrows, inside the two boxes of ↔I.

(i) ⇒ (ii). If n=2k+1, then n+1=2(k+1).

(ii) ⇒ (iii). If n+1=2j, then n−1=2(j−1), so n2−1=(n−1)(n+1)=4j(j−1). By the fact quoted, j(j−1)=2m for an integer m, so n2−1=8m.

(iii) ⇒ (iv). If n2−1=8m, then n2=2(4m)+1, which is odd.

(iv) ⇒ (i). This is Theorem 2.4.4, read from right to left.

(Exercise B3 of Section 1.6 met the fact (i) ⇒ (iii) by another route.)

For the second question: (i) ⇒ (iv) and (iv) ⇒ (i). Both are Theorem 2.4.4, so they cost nothing. Any two implications joining the two pairs, one in each direction, would do, for instance (ii) ⇒ (iii) and (iv) ⇒ (i); with them every condition reaches every other.

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) ⇒ (iv) or (iv) ⇒ (i) argued by examples.

Exercise (B7: Derive or break)

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 x that make its counterexample set true.

  • (a) P↔Q⊢(P∨R)↔(Q∨R).
  • (b) (P∨R)↔(Q∨R)⊢P↔Q.
  • (c) P↔(Q∧R)⊢P→Q.
  • (d) P↔(Q∧R)⊢Q→P.
  • (e) P↔Q, Q↔¬R⊢¬(P∧R).
  • (f) P↔Q⊢¬(P∧¬Q).
  • (g) ¬(P∧¬Q)⊢P↔Q.
  • (h) P↔Q, P∨Q⊢P∧Q.

Solution.

  • (a) Derive. Two boxes for the iff, and a case split inside each.
    1P↔Q
    2P∨Rasm, for ↔I
    3Pasm, for ∨E
    4Q↔E 1, 3
    5Q∨R∨I 4
    6Rasm, for ∨E
    7Q∨R∨I 6
    8Q∨R∨E 2, 3–5, 6–7
    9Q∨Rasm, for ↔I
    10Qasm, for ∨E
    11P↔E 1, 10
    12P∨R∨I 11
    13Rasm, for ∨E
    14P∨R∨I 13
    15P∨R∨E 9, 10–12, 13–14
    16(P∨R)↔(Q∨R)↔I 2–8, 9–15
  • (b) Break. Take P: “x>0”, Q: “x>5”, R: “x>−1”. At x=1, P∨R and Q∨R are both true, so the premise is true; P is true and Q false, so P↔Q is false. The counterexample set (Definition 1.1.3) (P∨R)↔(Q∨R), ¬(P↔Q) is true at x=1.

  • (c) Derive.

    1P↔(Q∧R)
    2Pasm, for →I
    3Q∧R↔E 1, 2
    4Q∧E 3
    5P→Q→I 2–4
  • (d) Break. Take P: “x>5”, Q: “x>0”, R: “x>3”. At x=1, Q∧R and P are both false, so the premise is true, while Q→P is false, since Q is true and P false. The counterexample set is true at x=1.

  • (e) Derive.

    1P↔Q
    2Q↔¬R
    3P∧Rasm, for ¬I
    4P∧E 3
    5Q↔E 1, 4
    6¬R↔E 2, 5
    7R∧E 3
    8⊥¬E 7, 6
    9¬(P∧R)¬I 3–8
  • (f) Derive.
    1P↔Q
    2P∧¬Qasm, for ¬I
    3P∧E 2
    4Q↔E 1, 3
    5¬Q∧E 2
    6⊥¬E 4, 5
    7¬(P∧¬Q)¬I 2–6
  • (g) Break. Take P: “x>5”, Q: “x>0”. At x=1, P∧¬Q is false, since P is, so the premise is true; P is false and Q true, so P↔Q is false. The counterexample set is true at x=1.

  • (h) Derive. Split on the second premise; in each case ↔E supplies the other letter.

1P↔Q
2P∨Q
3Pasm, for ∨E
4Q↔E 1, 3
5P∧Q∧I 3, 4
6Qasm, for ∨E
7P↔E 1, 6
8P∧Q∧I 7, 6
9P∧Q∨E 2, 3–5, 6–8
  • (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 x at which every member of the counterexample set is true. Fatal errors (0 for the claim): a “break” at which a premise fails; RAA in a derivation; a box of ↔I citing its sibling.

C. Going deeper

Exercise (C1: Divisibility by six)

For integers d and n, write d∣n if n=dk for some integer k. Let n be an integer. Prove that the following three conditions are equivalent, by a single cycle of three implications.

  • (i) 6∣n;
  • (ii) 2∣n and 3∣n;
  • (iii) 6∣n2.

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) ⇒ (iii) ⇒ (ii) ⇒ (i). The last arrow is the one that needs an idea: the two halves of (ii) must be used together, not one at a time.

Solution. We prove (i) ⇒ (iii) ⇒ (ii) ⇒ (i), which suffices by Proposition 2.4.6.

(i) ⇒ (iii). Suppose n=6k. Then n2=36k2=6(6k2), so 6∣n2.

(iii) ⇒ (ii). Suppose n2=6j. Then n2=2(3j) is even, so n is even by Theorem 2.1.3, that is, 2∣n. Also n2=3(2j), so 3∣n2, and by part (a) of Exercise (B3: The square root of three, used later), 3∣n. Hence 2∣n and 3∣n [∧I].

(ii) ⇒ (i). Suppose 2∣n and 3∣n, and write n=3b with b an integer. The integer b is odd or even. If b were odd, then n=3b would be odd: writing b=2c+1 gives 3b=6c+3=2(3c+1)+1. But n is even, and no integer is both, so this case cannot occur [¬E,⊥E]. Hence b is even, say b=2c, and n=6c, so 6∣n.

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) ⇒ (iii) by computation. - 3: (iii) ⇒ (ii), citing Theorem 2.1.3 for the factor 2 and part (a) of Exercise (B3: The square root of three, used later) for the factor 3. - 4: (ii) ⇒ (i), combining the two factors correctly (ruling out b odd, or n=3n−2n, or otherwise).

Fatal errors (0 for the step): a “cycle” that omits a condition; using “2∣n and 3∣n gives 6∣n” without proof; using “6∣n2 implies 6∣n” as known. Any other cycle through the three conditions earns full marks if each of its arrows is proved: 1 point for the cycle and its citation, and 3 points for each of its three arrows.

Exercise (C2: Dropping a hypothesis, and repairing the statement)
  • (a) Suppose only y≥0 is assumed in Theorem 2.4.5, and x is an arbitrary real number. The remark after it says that (⇐) survives. Which steps of its proof use y≥0, and why is x≥0 never needed? Refute (⇒) with a new pair.
  • (b) Prove that for all real numbers x and y, |x|≤|y| if and only if x2≤y2.

Hint: for (b), apply Theorem 2.4.5 to the right pair of numbers.

Solution.

  • (a) The proof of (⇐) uses y≥0 twice: for x>0 from x>y, and for y2≤xy. Its other multiplication is by the derived x>0, so x≥0 is never used. For (⇒), take x=−3, y=1: x≤y and y≥0, but x2=9>1=y2.

  • (b) Let x and y be real numbers. Then |x|≥0 and |y|≥0, so Theorem 2.4.5 applies to the pair |x|, |y| and gives |x|≤|y| if and only if |x|2≤|y|2. Finally |x|2=x2, since |x| is x or −x and (−x)2=x2, and likewise |y|2=y2. This proves that |x|≤|y| if and only if x2≤y2.