Negation and Classical Logic

Is there a rational number whose square is $2$? Is $x^2+1$ ever $0$ for a real number $x$? Is “if $x^2<0$, then $x=7$” true? Chapter 1 could prove that things are so, but not that something is not so, and it read the third sentence only informally, as a promise not broken: no rule yet derives it. By the end of this chapter you will be able to prove that something is not so; you will know when “suppose not” is a different kind of step from the others, and why that one step is all that classical logic adds. Two questions stay open at the end. How do you find a derivation when none comes to mind? Chapter 3 answers it. And how could you ever show that something is not derivable? Chapter 4 answers that.

Steps about “every” and “some”. Proofs in this chapter apply facts about every integer to one integer, pass from an arbitrary rational number to all of them, and name the $k$ in “$n=2k+1$”. These are steps about “every” and “some”. Here they are used as ordinary reasoning, as in school algebra; Chapter 5 gives them rules.

What you need. All of Chapter 1: the rules for “and”, “implies”, and “or”, and above all the definition of a derivation, with its boxes and its scope rule (Definition 1.4.2). School algebra about integers and real numbers is used in examples, as facts.

Time. About 30 hours on the core track (all of A, one B and one C per section, the exit checks); about 50 hours for everything.

Minimum before Sets, Relations, and Cardinality. Chapters 1–6 and 8, core; Sections 7.1–7.2 before its Chapter 3.

Roadmap

• Contradiction: Using a Negation. The rules $\mathrm{\neg }\mathrm{E}$ and $\mathrm{\perp }\mathrm{E}$: what a clash is, what it buys, why an impossible case closes itself and an implication with an impossible hypothesis is true, and the two sequents called the paradoxes of material implication.
• Proving a Negation. The rule $\mathrm{\neg }\mathrm{I}$, and with it the irrationality of $\sqrt{2}$, then of $\sqrt{p}$ for a prime $p$.
• Derived Rules: Proved Sequents as New Rules. A proved sequent used as one line; modus tollens, the contrapositive and disjunctive syllogism; and why pasting a proved sequent into a derivation is safe (weakening and cut).
• Iff, Equivalence, and What a Definition Says. The rules for $\leftrightarrow$, provable equivalence, why a definition’s “if” means “if and only if”, chains of equivalences, and why no statement is equivalent to its own negation.
• Proof by Contradiction and the Classical Rules. The rule $\mathrm{RAA}$, the classical laws it gives (double-negation elimination, excluded middle, De Morgan, Peirce), where the classical step is needed, and why three of its forms stand or fall together.

Named moves

• Goal $\mathrm{\perp }$: find a clash. Look for $\phi$ and $\mathrm{\neg }\phi$ among the available lines, or make $\phi$ a subgoal for some $\mathrm{\neg }\phi$ you have. (Section 2.1)
• An impossible case closes itself. In a proof by cases, a case that reaches $\mathrm{\perp }$ ends by $\mathrm{\perp }\mathrm{E}$ on the current goal. (Section 2.1)
• To prove “not $\phi$”, assume $\phi$. The box opens with the unnegated statement and ends on $\mathrm{\perp }$. (Section 2.2)
• Use a derived rule as one line. A proved sequent is a new rule. (Section 2.3)
• Two boxes for an iff. One box for each direction, each ending on the other side. (Section 2.4)
• When stuck, assume the negation of the goal. Proof by contradiction, and then hunt for a clash. (Section 2.5)
• A disjunction with neither side within reach: expect the classical step. When each side of a disjunctive goal breaks on its own, aim at the disjunction by $\mathrm{RAA}$. (Section 2.5)

Section 3.1 gathers these moves and Chapter 1’s into one table, and all thirteen rules onto one card.

Summary

The chapter added the rules for $\mathrm{\neg }$, $\mathrm{\perp }$ and $\leftrightarrow$ and the rule $\mathrm{RAA}$, which with Chapter 1’s seven make the thirteen primitive rules. It proved that a clash gives anything (Proposition 2.1.1) and that an impossible hypothesis makes an implication true (Proposition 2.1.2); it proved the theorem Argument B set out to prove (Theorem 2.1.3) and that $\sqrt{2}$ is irrational (Theorem 2.2.1). It turned proved sequents into rules, with weakening and cut as the reason pasting is safe (Lemma 2.3.3). It showed that an iff is two implications, that a definition’s “if” is an iff, and that no statement is equivalent to its own negation (Lemma 2.4.2). With $\mathrm{RAA}$ it derived double negation, excluded middle, De Morgan’s laws and Peirce’s law, and showed $\mathrm{RAA}$, $\mathrm{\neg }\mathrm{\neg }\mathrm{E}$ and $\mathrm{LEM}$ to be one principle (Theorem 2.5.7). Still open: a method for finding derivations (Chapter 3), and a way to show that a sequent has no derivation (Chapter 4), which also settles whether the classical rule could be done without.

Terms

• biconditional rules $\leftrightarrow \mathrm{I}$, $\leftrightarrow \mathrm{E}$: prove by two boxes; use either direction (Definition 2.4.1).
• classical rules $\mathrm{RAA}$, $\mathrm{\neg }\mathrm{\neg }\mathrm{E}$, $\mathrm{LEM}$: interderivable; one principle (Theorem 2.5.7).
• contradiction $\mathrm{\perp }$: the line a clash produces (Definition 2.1.1).
• contradiction rules $\mathrm{\neg }\mathrm{E}$, $\mathrm{\perp }\mathrm{E}$: a clash gives $\mathrm{\perp }$; $\mathrm{\perp }$ gives anything (Definition 2.1.1).
• contrapositive: $\mathrm{\neg }\psi \to \mathrm{\neg }\phi$, derivable from $\phi \to \psi$ (Proposition 2.3.2).
• cut: a proved lemma may be pasted in (Lemma 2.3.3).
• De Morgan’s laws: how negation passes through “and” and “or” (Proposition 2.5.5).
• derived rule: a proved sequent used as one line (Definition 2.3.1).
• disjunctive syllogism $\mathrm{DS}$: from $\phi \vee \psi$ and $\mathrm{\neg }\phi$, conclude $\psi$ (Proposition 2.3.4).
• double negation: $\mathrm{\neg }\mathrm{\neg }\phi$ and $\phi$, each from the other (Proposition 2.5.1).
• ex falso: from a clash, anything follows (Proposition 2.1.1).
• excluded middle $\mathrm{LEM}$: $\phi \vee \mathrm{\neg }\phi$, with no premises (Proposition 2.5.3).
• modus tollens $\mathrm{MT}$: from $\phi \to \psi$ and $\mathrm{\neg }\psi$, conclude $\mathrm{\neg }\phi$ (Proposition 2.3.1).
• negation rule $\mathrm{\neg }\mathrm{I}$: assume $\phi$, reach $\mathrm{\perp }$, conclude $\mathrm{\neg }\phi$ (Definition 2.2.1).
• Peirce’s law: $((\phi \to \psi )\to \phi )\to \phi$ (Proposition 2.5.4).
• provably equivalent, $⊣⊢$: each derivable from the other (Definition 2.4.2).
• reductio ad absurdum $\mathrm{RAA}$: assume $\mathrm{\neg }\phi$, reach $\mathrm{\perp }$, conclude $\phi$ (Definition 2.5.1).
• vacuously true: an implication whose hypothesis cannot hold (Proposition 2.1.2).
• weakening: extra premises never spoil a derivation (Lemma 2.3.3).