2.1 Contradiction: Using a Negation
Chapter 1 gave rules for “and”, “implies”, and “or”, and not one of them mentions “not”. Yet written proofs are full of sentences such as “this is impossible”, “this case cannot occur”, and “which contradicts what we assumed”. This section gives the two rules that use a negation: the first says exactly what a clash between two lines is, and the second says what a clash buys. The rule that proves a negation is the subject of the next section.
2.1.1. A case that cannot occur
Here is Argument A of Section 1.1, told as a proof by
cases. Let
Chapter 1 has a rule for a proof by cases:
Two things are missing, and no rule of Chapter 1 supplies them.
- A way to record the impossibility:
the lines “
is even” and “ is odd”, together with “no integer is both”, should produce a line that says “contradiction”. - A way to close the impossible box
with the goal: from the line “contradiction”, the box
should be allowed to write “
is even”, so that both boxes end on the same line and applies.
Section 1.1 introduced the symbols for both. The
connective
2.1.2. The rules for a clash
The rule for recording a clash has a simple content.
The statement
A statement and its negation clash; from a clash, anything follows.
The left schema is
Why may
As in every schema (Definition 1.2.1),
- Two given lines, both available (the scope rule of Definition 1.4.2), in either order on the page.
- Exactly
and : the second is the first with one in front of the whole of it, symbol for symbol. “Contradicts it in spirit” is not enough: and cannot both hold, but neither is the other’s negation as written (the box below). - The citation lists the unnegated
line first: “
” says that line is . - The new line is
and nothing else; what to do with the clash is the business of .
And
- Schema. The right one in the block above.
- Reading. One available line
, cited alone; write any statement, related to nothing above, a negation or itself included. - Example. From line 4
, “ 4” writes , or , or .
Second readingWhere a line ⊥ comes from, and why ⊥E is honest
Two more observations complete the reading. First,
Second, why is
In the Givens/Goal table,
Quick check. Which of these pairs
of lines are, as written, an instance of the given lines
of
Solution.
- (i) Yes, with
; cite the line first. (ii) Yes, with : the second line is . Cite first, then . (iii) No. The main connective of is (Definition 1.1.2), so it is not a negation at all; the applies to alone. The negation of would be .
Remark. Convention:
negations of order and equality. For real
numbers
The fact “no integer is both even and odd” is a
negation of a conjunction,
Quick check. For a real number
Solution.
- (i) Yes:
is ; cite first. (ii) Yes: is ; cite first. (iii) No: is , and is not . The line , written out, must first be built by (drill A2(l)).
Warning. A clash must have the
exact shape
Warning.
2.1.3. First derivations with a clash
The five examples below grow in difficulty. Each Idea
says why each rule was chosen, in the two directions
Chapter 1 used: from the goal (what does the goal’s main
connective ask for?) and from the premises (what does an
available line’s main connective let us do?). This
section adds one question to each list. From the goal:
when nothing produces the goal, can a clash produce
it? From the premises: an available negation
Show that (a)
Idea.
- (a) is the rule
itself, the degenerate case with no clash to find. In (b), the first premise is a conjunction, so the premise-directed move takes it apart by . Its half and the premise are exactly a pair , . The goal has nothing to do with the premises: no rule builds it from them. Only can write it, and needs a line , which the clash supplies.
Snapshots for (b): the goal alone; then the goal
handed to
Solution.
- (a) Two lines: the
premise, and one application of
.12 1 - (b) Five lines.
Line 4 cites line 3 first because line 3 plays
The next result is the pattern of (b) with nothing extra around it. We state it as a proposition, because later sections cite it.
Idea. The premises are a clash as
they stand, so
Proof. The derivation
has premises
In the next derivation the clash happens inside a
box, and the rule
Idea. The goal is an implication,
so the goal-directed move of Chapter 1 (
Snapshots: the box with its goal
Proof. The derivation
has premise
Line 4 is the line that makes the box close properly:
In the next example no clash is lying about. It has to be made.
Show that
Idea. As before, the goal
Snapshots: the box with its goal
Solution. Six lines.
Line 4 cites line 3 as
Quick check. Inside the box of
Solution. No.
The last of these first derivations is the pattern of the opening argument: a case split in which one case is impossible.
Show that
Idea. The goal
Snapshots: the split set up; then the first box’s
goal handed to
Solution. Nine lines.
The second box consists of its assumption alone, a
one-line box, just as in the derivation of
Look at line 7 of this derivation again. The box of
Warning. The impossible case must
be impossible from what is available in its own
box. A clash with a line of a sibling box, or
of a box that has already closed, is a scope error (Definition 1.4.2),
even when the clash “looks right”. In Example (An impossible case)
the clash in the box of
The moves of this section, in one place. Goal
2.1.4. How the rules look in a mathematical proof
We can now prove the fact of Argument A in Section
1.1, with every rule named. Three school facts about
integers enter as premises. An integer
- (E1) every integer is even or odd;
- (E2) no integer is both even and odd;
- (E3) the square of an odd integer is odd.
The third is a computation. If
and
Let
Idea. The hypothesis “
Proof. Suppose
Case
Case
In both cases
The logic of the proof fits in a derivation. Write
Each line is one sentence of the proof.
| Line | Sentence of the proof |
|---|---|
| 1–3 | (E1) for |
| 4 | Suppose |
| 5 | Case |
| 6 | Case |
| 7 | By (E3), |
| 8 | So |
| 9 | which contradicts (E2). |
| 10 | So this case cannot occur, and in it |
| 11 | In both cases |
| 12 | This proves that if |
Line 8 cites line 4, the assumption of the outer box;
it may, since the box
Quick check. Which sentence of the
proof of Theorem 2.1.3
is the rule
Solution. The sentence “So this
case cannot occur, and in it
Every rule in this proof is a primitive rule:
2.1.5. Vacuous truth
We can now settle the question that makes many readers distrust logic. Is the sentence
if
, then
true, for a real number
Let
Idea. The goal is an implication,
so open a box with
Solution. With the school fact as the premise:
In prose: suppose
We wrote out all five lines rather than citing Proposition 2.1.2 as a single step. Using an already proved sequent as one line of a new derivation is a genuine new permission, and Section 2.3 grants it; until then, a derivation repeats the steps.
An implication whose hypothesis cannot hold is called
vacuously true. Nothing about it was
decided by convention. It is forced by two rules that
each look harmless:
Everyday language agrees. A friend says: “if you finish the exercises by Friday, I will buy you lunch”. You do not finish them. Whatever your friend does on Friday, the promise has not been broken. A promise never tested is never broken.
Vacuous truth is not a curiosity; it is what makes
case splits work. In Example (An impossible case),
line 7 closed the impossible case by
Warning. “True” is not “useful”.
The statements “if
2.1.6. Two sequents that sound wrong
Two sequents in hand sound wrong when read aloud with
unrelated statements. The first is
Each comes from a rule, so whoever rejects one must
say which rule goes: the first rests on
Mathematics does not suffer: its “if” almost always
sits under “every”, joining two statements about one
variable, as in “for every integer
Quick check. Let
Solution. The first by
Second readingThe ‘if’ of a counterfactual
“If
2.1.7. The rule card
Before the card, the two rules at work on large statements, one use per row.
| Rule | Cited lines | New line | |
|---|---|---|---|
Not instances. (i) The 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 |
In Lean the two steps are often taken together:
absurd hp hn closes any goal from a proof
hp of hn of contradiction
finds such a pair by itself.
Warning (Not allowed:
- “
from and , as written”: the lines must be exactly and (Exactly and ; the convention box, drill A2(l)). - “
— ”, with line the negation: the unnegated line is cited first (The citation). - “
from the one line ”: needs two lines, and runs from , never to it (Two given lines; the warning that does not run backwards).
Remark (Looking ahead). Chapter 4
gives each connective a truth table. The rows of
2.1.8. Exercises
A. Check your understanding
- (a) Write the
schemas of
and from memory. - (b) Match each
sentence, taken from proofs, with the rule it uses,
or : “But was assumed odd, and we have just shown it is even”; “In this case , which is impossible, so there is nothing to prove”. - (c) True or false,
with a reason:
lets us write from any line. - (d) In Example (An impossible case), why is the second box only one line long?
- (e) In the derivation after Theorem 2.1.3, why does line 8 need line 4, and why may it cite it?
Solution.
(a)
: from a line with and a line with , both available, write at line , citing . : from an available line with , write any statement at line , citing . The two schemas are those of Definition 2.1.1.(b) The first is
: “odd” and “even” clash through (E2), and the sentence records the clash. The second is : “impossible” records a clash (an against , left unsaid), and “there is nothing to prove” closes the case with whatever the case needs.(c) False.
runs from to any statement, not from any statement to . needs a line to start from. The rule that records a clash as is , and it needs two lines and .(d) The box is opened by
, and is already the goal of both boxes. So the box’s first line is also its last line, which is all asks of it.(e) Line 8 is
, built by from and ; line 4 is the only line that says . It may cite line 4 because the only box containing line 4, the box , also contains line 8 (the scope rule of Definition 1.4.2).
Each part takes a line or two. Lines are numbered as in a derivation. 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 “ 2, 1” write? - (b) Lines 1
, 2 . Which line is for , and how is the step cited? - (c) Line 1 is
. Which of , , , may “ 1” write? - (d) Lines 4
and 6 are available at line 7. Write line 7 by , with its citation. - (e) Line 7 is
, justified “ 5, 2”, and line 2 is . What is line 5? - (f) Line 9 is
, justified “ 8”. What is line 8? - (g) Justify each
line, the first three being premises: 1
, 2 , 3 , 4 , 5 , 6 , 7 . - (h) Lines 1
, 2 . Is “3. — 2, 1” legal? - (i) Line 1 is
. May “2. — 1” be written? - (j) For a real
number
, do the lines and clash? - (k) Find the illegal
line: 1
; 2 ; 3 | ; 4 | , 1, 3; 5 | , 2, 4; 6 | , 5; 7 , 3–6. - (l) For one real
number
, lines 1 and 2 are given. Make them a clash, line by line. - (m) Derive
. - (n) Derive
. - (o) Derive
.
Solution.
(a)
.(b)
(line 2), and (line 1): the step is cited “ 2, 1”.(c) All four:
writes any statement.(d) 7
, “ 4, 6”: line 4 is , line 6 is .(e)
, the unnegated form of line 2.(f)
: cites one line, and it is .(g) 4
2, 3; 5 4; 6 5, 1; 7 6.(h) No: line 1’s main connective is
, so it is not a negation. First write by 1 as line 3, then by 2, 3.(i) No:
starts from a line ; no rule writes from a single line .(j) No: both hold at
.(k) Line 5: the unnegated line comes first. With line 2 as
, line 4 would have to be . Correct: “ 4, 2”.(l) Write line 2 as
( says that fails, and is written out because must build it); 3 , 1; 4 , 3, 2.(m) 3
, 2; 4 , 1, 3; 5 , 4.(n) 2 |
, assumption; 3 | , 2, 1; 4 | , 3; 5 , 2–4.(o) 4
, 1, 3; 5 , 4, 2; 6 , 5.
B. Practice
- (a) Show that
. - (b) Show that
, and say why may write a negation.
Solution.
- (a) As in Example (Manufacturing the other half of a clash),
with
in place of : the box of manufactures by on the other side.12 asm, for3 24 3, 15 46 2–5 - (b) Take the first premise apart, fire the implication on the second premise, and clash.
Line 7 is an instance of
Let
Solution. Suppose
Case
Case
In both cases
The step “
Let
Solution. The school fact is
The second is the same, with
No real number is both greater than
A search for
Solution. The move is an
impossible case closes itself. The case
For each claim, either derive it with the rules of
Chapter 1 and of this section (
- (a)
. - (b)
. - (c)
. - (d)
. - (e)
. - (f)
. - (g)
. - (h)
.
Solution.
- (a) Derive. Split on
the first premise; the case
is impossible beside the premise , and the case is the goal.123 asm, for4 35 2, 46 57 asm, for8 1, 3–6, 7–7 (b) Break. Take
: “ ”, : “ ”. At , is true ( ), is true ( fails), and is true, so is true: the counterexample set , , is true.(c) Derive. The premise
fires the implication, and its conclusion clashes with .123 1, 24 2, 35 4(d) Break. Take
: “ ”, : “ ”. The premise holds for every . At , is true ( fails) and is true ( ), so is true: the counterexample set , , is true.(e) Derive. The goal is an implication; inside its box,
manufactures the other half of the clash with the first premise.123 asm, for4 2, 35 4, 16 57 3–6(f) Break. Take
: “ ”, : “ ”. At , is false, so is true; and and are both false, so is false. The counterexample set , is true.(g) Break. Take
: “ ”, : “ ”, : “ ”. The premise holds for every . At , is true ( ), is true ( fails), and is false, so is true: the counterexample set , , , is true.(h) Derive. Inside the box of
, the first premise fires, and its half clashes with the premise .
The four that break are look-alikes. (b) draws the
wrong conclusion from a refuted disjunct: the
disjunctive syllogism of Section 2.3, after putting the
disjunction in the other order, gives
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
- (a) List the rules
used by a derivation of
and by one of . - (b) Suppose
were dropped. Derive without it, and say what this derivation stops short of. - (c) Suppose instead
were allowed only when the box’s assumption is cited by some line of the box or is itself the box’s last line. Which of the two derivations of (a) is lost? Is the one-line box of lost? Is the sequent lost? - (d) Let
be an integer. For , and , write the instance of “if is a multiple of , then is even”, and say for each whether the first sequent of (a), the second, or neither, decides its truth.
Solution.
(a)
: , , (Proposition 2.1.2). : and repetition.(b) Four lines:
12 asm, for3 2, 14 2–3It stops at
inside the box, where the derivation of Proposition 2.1.2 wrote : the step from to was ’s. What survives says only that leads to a contradiction.- (c) The derivation
of
is lost: no line of its box cites the assumption (line 3 repeats line 1). The box of is kept: its last line is its assumption, which the restriction allows. The derivation of Proposition 2.1.2 is kept: line 3 cites the assumption. But the sequent is not lost. This derivation meets the restriction, since line 3 cites the assumption:12 asm, for3 2, 14 35 2–4The restriction kills one derivation, not the sequent; a logic that really rejects the paradox has to restrict more than one rule.
- (d)
: “if is a multiple of , then is even”; hypothesis and conclusion are both false, so only decides it. : “if is a multiple of , then is even”; the hypothesis is false and the conclusion true, so either sequent decides it. : “if is a multiple of , then is even”; both parts are true ( ), so the first sequent does not apply and the second does, since the conclusion is true. This is the one instance of the three whose hypothesis holds, the kind in which the theorem says something: here it can be fired by .
Marking scheme. (10 points) 2: (a),
both rule lists. 2: (b), a correct four-line derivation
(1) and the remark that the step to
C. Going deeper
- (a) Show that
. - (b) What does (a)
say about the statement “
, or and ”, for a real number ?
Solution.
- (a) The premise is a
disjunction, so split it by
, with both boxes ending in the goal . The box of is a one-line box. The box of is impossible: gives a clash, and closes the case.12 asm, for3 asm, for4 35 36 4, 57 68 1, 2–2, 3–7 - (b) With
: “ ” and : “ ”, the statement is , since is . By (a), it gives . So the second disjunct adds nothing: a disjunct that can never hold is an impossible case, and it closes itself. (Conversely, gives the whole statement by , so the two say the same thing.)
A student wants to show
- (a) Is the sequent
derivable? - (b) Find the first line that is not justified, and name the clause of Definition 1.4.2 it breaks.
- (c) Show that the move made at that line can lead from a true premise to a false conclusion.
- (d) Write a correct derivation.
Solution.
(a) Yes: it is Proposition 2.1.2. The conclusion is true; the question is whether this argument proves it.
(b) Line 4. It cites line 3, which lies inside the box
, and that box has closed before line 4. By the scope rule of Definition 1.4.2, a line inside a closed box is not available. (Lines 1–3 are fine: a box may close without a rule discharging it, although nothing then leaves it. Lines 5–7 would be fine if line 4 were.)(c) Lines 1–4 alone would “derive”
by the same move. Read as “ ” and as “ ”, and take . The premise is true, and the conclusion is false. So the move “write, outside a box, what a closed box’s would allow” can lead from a true premise to a false line. The line on line 3 holds only under the assumption ; once the box closes, that assumption is gone, and so is the clash.(d) Move the
inside the box, where the clash is:
Marking scheme. (10 points) - 2:
answers (a) yes, citing Proposition 2.1.2
or giving a derivation. - 3: names line 4 as the first
failure and the scope rule (a line inside a closed box
is not available) as the clause broken. - 3: gives a
counterexample to the step, not only to
some conclusion: a reading of
Fatal errors (0 for the step): blaming line 7 or line
6 (they are correct once line 4 is); saying that