8.7 The Dispute over Excluded Middle

Here is a proof that two numbers with a certain property exist which, when it is finished, still does not tell you what the numbers are. It is correct by the rules of this book. Some mathematicians, called intuitionists, reject it, for a century now and for reasons that are mathematical rather than merely fussy. This section shows the proof, says what those mathematicians ask of a proof, finds the one rule that fails to provide it, and asks what can be proved without that rule and what analysis would lose.

8.7.1. Irrational powers, with and without a witness

Here is the standard example of a proof that establishes existence without saying what exists.

Theorem 8.7.1 (An Irrational Power of an Irrational Number Can Be Rational) Optional: nothing later depends on this.

There are irrational numbers $a$ and $b$ such that $a^b$ is rational.

Try it first (ten minutes): find such $a$ and $b$ explicitly, and prove that your $a$ and $b$ are irrational and that $a^b$ is rational.

Idea. The first candidates anyone tries are $a = b = \sqrt 2$ . Then the question is whether $\sqrt 2^{\sqrt 2}$ is rational, and the attempt stalls there: nothing in this book decides it. There are two ways out. The classical one splits on the undecided question with $\mathrm{LEM}$ . If $\sqrt 2^{\sqrt 2}$ is rational, the first candidates work. If not, use it as the new $a$ and raise it to $\sqrt 2$ once more, which turns the exponent into $\sqrt 2 \cdot \sqrt 2 = 2$ . The proof below takes this way. The other way chooses an exponent that undoes the square root, and the proposition after the proof takes it.

Proof. Let $s \mathrel{:=} \sqrt 2^{\sqrt 2}$ , a positive real number. By excluded middle, $s$ is rational or $s$ is not rational [ $\mathrm{LEM}$ ], and we argue by cases [ $\mathrm{\vee E}$ ].

Case 1: $s$ is rational. Take $a \mathrel{:=} \sqrt 2$ and $b \mathrel{:=} \sqrt 2$ . Both are irrational by Theorem 2.2.1, and $a^b = s$ is rational [ $\mathrm{\exists I}$ ].

Case 2: $s$ is not rational. Take $a \mathrel{:=} s$ and $b \mathrel{:=} \sqrt 2$ . Then $a$ is irrational by the case assumption and $b$ by Theorem 2.2.1, and $a^b = \bigl( \sqrt 2^{\sqrt 2} \bigr)^{\sqrt 2} = \sqrt 2^{\sqrt 2 \cdot \sqrt 2} = \sqrt 2^{\,2} = 2,$ which is rational [ $\mathrm{\exists I}$ ].

In either case there are irrational $a$ and $b$ with $a^b$ rational. This proves the theorem.

The classical step is the first line, $\mathrm{LEM}$ on the statement “ $s$ is rational”. Every other step uses only rules other than $\mathrm{RAA}$ . The proof does not tell us which pair works. It hands over two candidate pairs, $(\sqrt 2, \sqrt 2)$ and $(\sqrt 2^{\sqrt 2}, \sqrt 2)$ , and a guarantee that one of them succeeds. The next subsection says why some mathematicians do not accept such a proof. Section 2.5 described excluded middle as making a decision; here the decision about “ $s$ is rational” is made, and nobody learns its outcome.

Remark. In fact the second case holds: $\sqrt 2^{\sqrt 2}$ is transcendental, so in particular irrational, by the Gelfond–Schneider theorem, proved independently by Gelfond and by Schneider in 1934. That theorem lies far beyond this book, and nothing here uses it. It also does not repair the proof above, which never needed to know the answer.

The other way out finds the witness. Since $\sqrt 2^{\,b} = 2^{b/2}$ , the exponent $b = 2\log_2 m = \log_2(m^2)$ gives $\sqrt 2^{\,b} = m$ for every integer $m \ge 2$ . The choice $m = 2$ gives $b = 2$ , which is rational, so $m$ must avoid the powers of $2$ ; the first choice left is $m = 3$ .

Proposition 8.7.2 (A Witness for an Irrational Power) Optional: nothing later depends on this.

The number $\log_2 9$ is irrational. Consequently $a \mathrel{:=} \sqrt 2$ and $b \mathrel{:=} \log_2 9$ are irrational numbers with $a^b = 3$ .

Idea. The irrationality goes as for $\sqrt 2$ : suppose $\log_2 9$ is a fraction $p/q$ , clear the denominator, and look at parity. Here the clash is quicker than for $\sqrt 2$ : a power of $2$ would equal a power of $9$ , and one is even while the other is odd. The positivity of $\log_2 9$ is what makes the power of $2$ even.

Proof. Suppose that $\log_2 9 = p/q$ for integers $p$ and $q$ with $q \ne 0$ ; replacing $p$ , $q$ by $-p$ , $-q$ if necessary, we may take $q \ge 1$ . Since $2^0 = 1 < 9$ and $t \mapsto 2^t$ is increasing, $\log_2 9 > 0$ , so $p > 0$ , that is, $p \ge 1$ . From $2^{p/q} = 9$ , raising both sides to the power $q$ gives $2^p = 9^q .$ The left side is even, since $2^p = 2 \cdot 2^{p-1}$ with $p - 1 \ge 0$ . The right side is odd, being a product of $q$ odd factors. No integer is both even and odd, by (E2) of Section 2.1, so this is a contradiction. Hence $\log_2 9$ is not rational [ $\mathrm{\neg I}$ ].

For the consequence, $a = \sqrt 2$ is irrational by Theorem 2.2.1, and $b = \log_2 9$ is irrational by what was just shown. Since $\log_2 9 = \log_2 (3^2) = 2\log_2 3$ , $a^b = \bigl( 2^{1/2} \bigr)^{\log_2 9} = 2^{(\log_2 9)/2} = 2^{\log_2 3} = 3 .$ This proves the proposition.

This proof uses no classical rule. The irrationality of $\log_2 9$ is a negative statement, “no fraction equals $\log_2 9$ ”, and its box closes by $\mathrm{\neg I}$ , like the proof of Theorem 2.2.1. The witness $(\sqrt 2, \log_2 9)$ is written down. So Proposition 8.7.2 gives a second proof of Theorem 8.7.1, and this one names its witness. (The exponent laws for real exponents are school facts here.)

Quick check. Does the proof of Proposition 8.7.2 use a classical rule? Does it name its witness?

Solution. No classical rule: its box assumes $\log_2 9 = p/q$ and concludes the negation, by $\mathrm{\neg I}$ . And yes, the witness $(\sqrt 2, \log_2 9)$ is written down.

8.7.2. What a proof provides

Chapter 4 gave the connectives a meaning through truth values: every letter is true or false, and a table computes the rest. That semantics already takes a side, since a row decides every letter. The intuitionist explains a statement instead by saying what counts as a proof of it. The resulting clauses are called the BHK reading, after Brouwer, Heyting, and Kolmogorov.

To know a statement is to have a proof of it, and a proof of a compound statement is built from proofs of its parts.

There is no proof of $\bot$ .
A proof of $P \wedge Q$ is a pair: a proof of $P$ and a proof of $Q$ .
A proof of $P \vee Q$ is a proof of $P$ or a proof of $Q$ , with a label saying which.
A proof of $P \to Q$ is a method that takes any proof of $P$ and returns a proof of $Q$ .
A proof of $\neg P$ is a method that takes any proof of $P$ and returns a proof of $\bot$ . So $\neg P$ is read as $P \to \bot$ , exactly the reading that the table in Section 2.2, after Definition 2.2.1, found row by row.
A proof of $\exists x\, \varphi$ is an object $t$ together with a proof of $\varphi[t/x]$ .
A proof of $\forall x\, \varphi$ is a method that produces, for every object $t$ , a proof of $\varphi[t/x]$ .

In words: a disjunction must say which side, an existence claim must name the object, and an implication or a universal statement must come with a method that works on every input. A proof of a negation provides no object at all; it is a guarantee that no proof of the negated statement will ever arrive.

Each rule other than $\mathrm{RAA}$ builds exactly what its clause asks for. $\mathrm{\vee I}$ writes $P \vee Q$ from a line $P$ , so it knows which side it used. $\mathrm{\exists I}$ writes $\exists x\, \varphi$ from an instance $\varphi[t/x]$ , so the witness $t$ is on the page. A $\mathrm{{\to}I}$ box is a method: given the assumption, it produces the conclusion. $\mathrm{RAA}$ is the exception. Its box shows that $\neg\varphi$ leads to $\bot$ , which is a proof of $\neg\neg\varphi$ , and then it writes $\varphi$ . Under the BHK reading a method for refuting every refutation of $\varphi$ is not a proof of $\varphi$ .

Excluded middle under BHK. A proof of $P \vee \neg P$ for every statement $P$ would be a single method that decides each statement, says which side holds, and proves that side. Nobody has such a method. Take Goldbach’s conjecture, that every even integer greater than $2$ is a sum of two primes: nobody has proved it and nobody has refuted it, so nobody can produce a labeled proof of “Goldbach’s conjecture or its negation”. The proof of Theorem 8.7.1 is of this kind: it splits on “ $s$ is rational or not” by $\mathrm{LEM}$ , and so never says which pair works.

Not every, and some not. Chapter 6 derived $\neg\forall x\, \varphi \vdash \exists x\, \neg\varphi$ (Proposition 6.2.1 (a)) with two $\mathrm{RAA}$ boxes, and noted that the derivation never says which $x$ fails $\varphi$ . The BHK reading says why that matters. A proof of the premise is a method that refutes every proof of $\forall x\, \varphi$ ; a proof of the conclusion must name an object. Nothing in the first produces the second, and the derivation does not try: its conclusion comes from $\mathrm{RAA}$ , not from an $\mathrm{\exists I}$ applied to an available instance. Classical mathematics accepts the step. A constructive mathematician accepts that conclusion only with an object in hand.

Quick check. Describe a BHK proof of $\neg(P \wedge \neg P)$ . Does it decide whether $P$ holds?

Solution. We need a method that takes any proof of $P \wedge \neg P$ and returns a proof of $\bot$ . A proof of $P \wedge \neg P$ is a pair: a proof $p$ of $P$ and a method $f$ turning proofs of $P$ into proofs of $\bot$ . Apply $f$ to $p$ . That is the whole method, and it never decides $P$ : it only uses a pair that someone else supplies. (It is the BHK reading of a $\mathrm{\neg I}$ box on $P \wedge \neg P$ whose clash is $\mathrm{\neg E}$ on its two halves.)

8.7.3. One extra rule

Chapter 2 found that one rule stands apart. $\mathrm{RAA}$ belongs to no connective, and over the other primitive rules it derives $\mathrm{\neg\neg E}$ and $\mathrm{LEM}$ and is derived by each of them (Theorem 2.5.7). Chapter 4’s optional Theorem 4.7.4 showed that the other propositional rules cannot derive it.

Recall what Section 2.5 established. Over the primitive rules other than $\mathrm{RAA}$ , the three rules $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ , and $\mathrm{LEM}$ each derive the other two, so adding any one of them gives the same derivable sequents. There is one classical principle, and it has three faces. Nothing needs re-proving here; what is new is the decision to leave the principle out and see what remains.

Call a derivation intuitionistic if no line is justified by $\mathrm{RAA}$ and no line uses a derived rule or a cited result whose own derivation uses $\mathrm{RAA}$ . Intuitionistic logic is the system of these derivations. Its rules are the introduction and elimination rules for $\wedge$ , $\to$ , and $\vee$ (Chapter 1); $\mathrm{\neg I}$ , $\mathrm{\neg E}$ , $\mathrm{\bot E}$ , $\mathrm{{\leftrightarrow}I}$ , and $\mathrm{{\leftrightarrow}E}$ (Chapter 2); the rules for $\forall$ , $\exists$ , and $=$ (Chapter 5); and repetition. Classical logic, the logic of Chapters 1–7, is the same list with $\mathrm{RAA}$ added. TAUT (Section 4.8) is not among these rules: it is licensed by Corollary 4.8.5, that is, by the completeness theorem, whose proof splits on atoms by $\mathrm{LEM}$ (Lemma 4.8.3), so a line justified by TAUT, on a formula or on a propositional skeleton (Section 6.3), uses $\mathrm{RAA}$ in the sense just defined.

This is why Chapter 2 kept $\mathrm{\bot E}$ as a primitive rule although $\mathrm{RAA}$ and repetition derive it (the remark in the second-reading fold after Theorem 2.5.7). Had $\mathrm{\bot E}$ been dropped, striking $\mathrm{RAA}$ would have taken it away too, and the remaining system would be weaker than the one intuitionists actually use: it could no longer derive $\bot \vdash P$ . That is a claim about all derivations, and we state it without proof; nothing depends on it. With $\mathrm{\bot E}$ kept, the rules without $\mathrm{RAA}$ are exactly intuitionistic logic.

System	Rules	$\vdash P \vee \neg P$ ?
intuitionistic	the primitive rules other than $\mathrm{RAA}$	not derivable (Theorem 4.7.4 for the propositional rules, and the optional Section 8.8 again, by stages of knowledge; the rules for $\forall$ , $\exists$ and $=$ do not change this, stated without proof)
classical	the same rules and $\mathrm{RAA}$	derivable (Proposition 2.5.3)

Every intuitionistic derivation is a derivation, so everything intuitionistic logic derives, classical logic derives too, and soundness applies to it: Theorem 4.7.2, and, for derivations whose lines contain quantifiers or equations, the soundness statement for predicate logic in Section 7.2. The difference is a list of sequents that only the classical system reaches. Chapters 2–7 flag the derivations that use $\mathrm{RAA}$ as they go, so the results on that list can be read off the text; Exercise B4 asks for them.

Quick check. Is the derivation of Proposition 2.5.1 (a), $P \vdash \neg\neg P$ , intuitionistic? Is that of (b)?

Solution.

(a) Yes: it is one $\mathrm{\neg I}$ box on $\neg P$ . (b) No: it is derived with $\mathrm{RAA}$ .

8.7.4. Excluded middle cannot be refuted

If intuitionists do not assert $P \vee \neg P$ , perhaps they deny it. They do not, and they could not: its double negation needs no classical rule at all.

Proposition 8.7.3 (Excluded Middle Cannot Be Refuted) Optional: nothing later depends on this.

For every statement $P$ , $\vdash \neg\neg(P \vee \neg P)$ , by a derivation that uses neither $\mathrm{RAA}$ nor $\mathrm{\bot E}$ .

Try it first (ten minutes): the goal is a negation. Open the box that the goal asks for, hunt for a clash, and note which rule closes each box you open.

Idea. An attempt that starts from $P \vee \neg P$ stalls at once: $\mathrm{\vee I}$ needs one side, and neither side is in hand. But the goal is not $P \vee \neg P$ . It is $\neg(\neg(P \vee \neg P))$ , a negation, so the goal-directed move of Section 2.2 opens a $\mathrm{\neg I}$ box on $\neg(P \vee \neg P)$ with the goal $\bot$ . That assumption can clash only with $P \vee \neg P$ , which $\mathrm{\vee I}$ builds from either side, so we manufacture a side as in Example (Manufacturing the other half of a clash). A box on $P$ gives $P \vee \neg P$ , a clash, and $\mathrm{\neg I}$ closes it with $\neg P$ . Then $\mathrm{\vee I}$ builds $P \vee \neg P$ from $\neg P$ , and that is the second clash. Every box ends in $\bot$ and closes by $\mathrm{\neg I}$ .

Before reading on: self-explain lines 5 and 6.

Proof. Exercise B1 (a) of Section 3.2 (Exercise (B1: Three theorems)) derived this already, inside a conjunction; here is that derivation again, read for what it does not use. The derivation is:

\neg (P \vee \neg P)

asm, for

\mathrm{{\neg}I}

P

asm, for

\mathrm{{\neg}I}

P \vee \neg P

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

3, 1

\neg P

\mathrm{{\neg}I}

2–4

P \vee \neg P

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

6, 1

\neg\neg (P \vee \neg P)

\mathrm{{\neg}I}

1–7

The two boxes close by $\mathrm{\neg I}$ , at lines 5 and 8. The other rules used are $\mathrm{\vee I}$ (lines 3 and 6) and $\mathrm{\neg E}$ (lines 4 and 7). The derivation has no premises. This proves the proposition.

Set it beside the derivation of Proposition 2.5.3. Lines 1–7 are the same, line for line. Only line 8 differs: there $\mathrm{RAA}$ closed the outer box and wrote $P \vee \neg P$ ; here $\mathrm{\neg I}$ closes it and writes the negation of its assumption. So the whole classical content of Proposition 2.5.3 sits in its last line.

Second readingNon-example by minimal change

Keep lines 1–7, and write $P \vee \neg P$ at line 8 with the justification $\mathrm{\neg I}\ 1\text{–}7$ . The box still checks. What fails is the conclusion of $\mathrm{\neg I}$ , which must be the negation of the box’s assumption, $\neg\neg(P \vee \neg P)$ . Writing $P \vee \neg P$ there needs $\mathrm{RAA}$ .

What the proposition says is this: nobody can refute excluded middle. A refutation of $P \vee \neg P$ , put beside this derivation, would prove $\bot$ from no premises, and no derivation does that. (That last fact is soundness: Theorem 4.7.2, or the soundness statement for predicate logic in Section 7.2 when $P$ or the derivation involves quantifiers or equality, since no valuation, and no structure and assignment, makes $\bot$ true.) The intuitionist does not claim that excluded middle fails. The intuitionist declines to assert it, because asserting it would mean having a proof of one side, and for many statements $P$ , an open conjecture for instance, nobody has one.

The proposition under BHK. The derivation of Proposition 8.7.3 is such a method, and it decides nothing. Its conclusion asks for a method that takes any $f$ , a method sending proofs of $P \vee \neg P$ to proofs of $\bot$ , and returns a proof of $\bot$ . Here is one. Given a proof $p$ of $P$ , label it “left” and apply $f$ : that turns proofs of $P$ into proofs of $\bot$ , which is a proof $g$ of $\neg P$ (lines 2–5). Now label $g$ “right” and apply $f$ once more (lines 6–7). At no point did the method need to know whether $P$ holds.

Remark. The proposition is one instance of a general fact, due to Glivenko (1929) and stated here without proof: if a statement built from letters by the connectives is derivable with all the rules, then its double negation is derivable without $\mathrm{RAA}$ . Classical propositional logic survives inside intuitionistic logic, behind two negations. The fact fails once quantifiers are allowed; $\neg\neg\forall x\, (\varphi \vee \neg\varphi)$ is in general not derivable without $\mathrm{RAA}$ (also stated without proof).

Warning. Intuitionistic logic does not say that excluded middle is false. No instance $P \vee \neg P$ can be refuted, since $\neg\neg(P \vee \neg P)$ is derivable without $\mathrm{RAA}$ ; dropping a rule is not adding its negation. (Brouwer’s own analysis adds axioms about the real numbers under which the universal statement “every real number is $0$ or not $0$ ” is refuted, but no single instance is.)

Quick check. Does Proposition 8.7.3 show that $P \vee \neg P$ is derivable without $\mathrm{RAA}$ ?

Solution. No. It derives $\neg\neg(P \vee \neg P)$ ; writing $P \vee \neg P$ after the same box needs $\mathrm{RAA}$ , and Chapter 4’s optional theorem in Section 4.7 shows that for a letter $p$ no derivation without $\mathrm{RAA}$ reaches $p \vee \neg p$ , as does the optional Section 8.8.

8.7.5. Which laws survive without RAA

Chapters 2 and 6 flagged every law they derived with $\mathrm{RAA}$ . Here they are side by side, split into directions. The middle column was derived without $\mathrm{RAA}$ . For the right column, with letters $p$ , $q$ , no derivation without $\mathrm{RAA}$ exists. The optional Section 8.8 proves this for the propositional rows; for the quantifier rows it is stated without proof.

Law	Derived without $\mathrm{RAA}$	Needs $\mathrm{RAA}$
double negation (Proposition 2.5.1)	(a) $P \vdash \neg\neg P$	(b) $\neg\neg P \vdash P$
contraposition (Proposition 2.3.2, Proposition 2.5.2)	$P \to Q \vdash \neg Q \to \neg P$	$\neg Q \to \neg P \vdash P \to Q$
De Morgan (Proposition 2.5.5)	(a), (b), (c)	(d) $\neg(P \wedge Q) \vdash \neg P \vee \neg Q$
implication as a disjunction (Proposition 2.5.6)	(a) $\neg P \vee Q \vdash P \to Q$	(b) $P \to Q \vdash \neg P \vee Q$
excluded middle (Proposition 2.5.3)	$\vdash \neg\neg(P \vee \neg P)$ (Proposition 8.7.3)	$\vdash P \vee \neg P$
Peirce’s law (Proposition 2.5.4)	—	$\vdash ((P \to Q) \to P) \to P$
negated implication (Proposition 6.2.2)	$\varphi \wedge \neg\psi \vdash \neg(\varphi \to \psi)$	$\neg(\varphi \to \psi) \vdash \varphi \wedge \neg\psi$
modus tollens, disjunctive syllogism, constructive dilemma (Proposition 2.3.1, Proposition 2.3.4, Example (Constructive dilemma))	all	—
quantifier negation (Proposition 6.2.1)	(b); (c) both ways	(a) $\neg\forall x\, \varphi \vdash \exists x\, \neg\varphi$
passage laws (Proposition 6.2.7)	eight of the ten directions	$\dashv$ in (d) and in (e)

For each propositional entry of the right column, the double negation of its conclusion is derivable without $\mathrm{RAA}$ from the same premises, by Glivenko’s theorem in the remark above (stated without proof) applied to the implication from the premises’ conjunction; Exercise B5 (a) and (b) derive two cases.

Quick check. An intuitionist has proved $\neg Q \to \neg P$ . May she conclude $P \to Q$ ?

Solution. Not in general: that step is Proposition 2.5.2, in the right column of the table. She may when $Q$ is itself a negation, by Section 2.5’s fold “RAA is never needed to finish a negation”, which Section 8.1 applies to the contrapositive.

8.7.6. A short history

The dispute has dates.

In 1908 L. E. J. Brouwer published “De onbetrouwbaarheid der logische principes” (“The unreliability of the logical principles”) in the Tijdschrift voor Wijsbegeerte. His point was that excluded middle had been abstracted from reasoning about finite collections, where every case can in principle be checked, and then applied without justification to infinite ones, where it cannot. Over the next two decades he rebuilt parts of analysis on this view, and the movement took the name intuitionism.

In 1925 A. N. Kolmogorov showed that classical reasoning can be imitated inside a logic without excluded middle by putting a double negation in front of every subformula: the first double-negation translation (Exercise C2 below checks one step of it).

In July 1927 David Hilbert lectured in Hamburg on “Die Grundlagen der Mathematik”, printed in 1928. He defended excluded middle in a much-repeated comparison: to take it from the mathematician would be like forbidding the astronomer the telescope or the boxer the use of his fists. The quarrel between his program and Brouwer’s became known as the Grundlagenstreit, the dispute over foundations. It turned personal in 1928, when Hilbert had Brouwer removed from the editorial board of the Mathematische Annalen; the board was then dissolved and re-formed without him.

In 1929 V. Glivenko proved the theorem of the remark above: classical propositional logic sits inside intuitionistic logic behind a double negation. In 1930 Arend Heyting published “Die formalen Regeln der intuitionistischen Logik” in the Sitzungsberichte der Preußischen Akademie der Wissenschaften. It wrote down rules for intuitionistic logic, in a format different from ours, and from then on the logic could be studied as a formal system like any other.

In 1933 Kurt Gödel published a double-negation translation of arithmetic, which shows that classical arithmetic is consistent if intuitionistic arithmetic is. Gerhard Gentzen had found an equivalent translation independently and withdrew his paper of 1933 when Gödel’s appeared.

In 1967 Errett Bishop published Foundations of Constructive Analysis. It developed a large part of analysis without excluded middle, and also without Brouwer’s philosophy and his special axioms about the real numbers. Most of what is now called constructive analysis descends from it.

Second readingAnother dispute: the conditional

Excluded middle is not the only rule that has been questioned. Chapter 1 read $P \to Q$ as a promise that is broken only when $P$ holds and $Q$ fails, so a true $Q$ makes $P \to Q$ true whatever $P$ says, and $\vdash P \to (Q \to P)$ . Some logicians find that too generous: an “if” should connect its two parts. Logics built on that view, called relevance logics, reject $P \to (Q \to P)$ . This book keeps Chapter 1’s reading, which is the one mathematics uses.

8.7.7. What analysis would lose

What does analysis look like without the rule? Here are four previews, stated informally and without proof. Classical analysis takes the first as an axiom and proves the other three; each is a place where classical reasoning, by the rule or by an axiom, does work that a constructive proof cannot.

The supremum. Classical analysis takes as an axiom that every non-empty set of real numbers that is bounded above has a supremum. Constructively, a non-empty set $A$ bounded above has a supremum if and only if it is order-located: for all real numbers $x < y$ , either $y$ is an upper bound of $A$ or some element of $A$ exceeds $x$ (Bishop’s form of the least upper bound principle). The classical axiom asserts the supremum without requiring anyone to make these decisions.
Monotone sequences. E. Specker (1949) gave an increasing, bounded sequence of rational numbers that a computer program can list term by term, but whose limit is not a computable real number: no program can print its decimal digits. So the convergence of bounded monotone sequences, which classical analysis proves from that axiom, cannot come with a method for computing the limit.
The intermediate value theorem. Let $f$ be continuous on $[a, b]$ with $f(a) < 0 < f(b)$ . Classically, one proves that $f(x) = 0$ for some $x \in [a, b]$ . Constructively, what holds in general is the approximate version: for every $\varepsilon > 0$ some $x \in [a, b]$ has $\left| f(x) \right| < \varepsilon$ . The exact version holds under extra hypotheses, for example when $f$ is strictly increasing. A bisection needs the sign of $f$ at a midpoint $m$ , and finitely many digits of $f(m)$ cannot always tell whether $f(m)$ is negative, zero, or positive: the digits of a value equal to $0$ begin like those of a tiny positive or negative one.
Bolzano–Weierstrass. A bisection proof of the theorem says: one of the two halves of an interval contains infinitely many terms of the sequence; continue with that half. That step is $\mathrm{LEM}$ on “the left half contains infinitely many terms”, a statement that nobody can decide in general, and the proof does not say which half.

8.7.8. Proofs as programs

The BHK clauses read like the description of a programming language. A proof of $P \wedge Q$ is a pair; a proof of $P \vee Q$ is a value tagged “left” or “right”; a proof of $P \to Q$ is a function; a proof of $\exists x\, \varphi$ is a pair of an object and a proof; a proof of $\forall x\, \varphi$ is a function that accepts any object. This match between propositions and types, and between proofs and programs, is the Curry–Howard correspondence. It is what a proof assistant such as Lean is built on: checking a proof is checking that a program has the right type.

Second readingProofs as programs, in Lean

Intuitionistic logic fits this picture exactly. $\mathrm{LEM}$ does not, since no program decides every proposition. Lean adds classical logic by an axiom, Classical.choice, a form of the axiom of choice. Excluded middle, Classical.em, is then a theorem, derived from choice together with two extensionality principles by Diaconescu’s theorem. Lean draws one line with care. A definition that uses classical logic to produce data, for instance a number chosen by deciding an arbitrary proposition, must be marked noncomputable, since no program computes it. A proof that uses Classical.em needs no mark, because proofs carry no data.

-- excluded middle is a theorem, proved from the axiom of choice
example (p : Prop) : Or p (Not p) := Classical.em p

-- a number defined by deciding an arbitrary proposition
open Classical in
noncomputable def indicator (p : Prop) : Nat := if p then 1 else 0

Warning. “Constructive” does not mean “computable in practice”. A constructive proof provides a method, and the method may be hopeless. Deciding whether a whole number is prime by trying every smaller divisor is constructive, and for a number with a thousand digits no computer could finish it. Constructive mathematics asks whether a method exists, not whether it is fast.

8.7.9. The book’s position

The main line of this book stays classical. The decision is made once, in the axioms for the real numbers, which include trichotomy: for real numbers $a$ and $b$ , exactly one of $a < b$ , $a = b$ , $b < a$ holds. Constructive analysis does not accept trichotomy for real numbers, because it would decide the sign of every real number. So a case split such as “ $x \ge 0$ or $x < 0$ ” rests on an axiom, and the book does not flag it.

What the book does flag is a genuinely non-constructive step of the kind discussed above, such as the bisection step of Bolzano–Weierstrass, and every use of the axiom of choice. One clause says so, and nothing more. Such a step is never silent anyway: by Definition 8.3.2, a $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ step is written out as an explicit case split or an explicit removal of a double negation. A reader who wants to know where the classical rule enters a proof can always find the place.

Remark (Looking ahead). Analysis on the Real Line takes trichotomy as one of its axioms in Chapter 1, and flags in one clause each genuinely non-constructive step it makes.

8.7.10. Exercises

A. Check your understanding

Exercise (A1)

Parts (a)–(d) are about Proposition 8.7.3 and its derivation; part (e) is about the proof of Theorem 8.7.1.

(a) Which rule closes each of the two boxes, and at which line?
(b) The outer box opens with a negation and ends in $\bot$ , the shape of an $\mathrm{RAA}$ box. Why is no $\mathrm{RAA}$ used?
(c) Give the BHK reading of the conclusion $\neg\neg(P \vee \neg P)$ .
(d) True or false, with a reason: for some statement $P$ , intuitionistic logic derives $\neg(P \vee \neg P)$ from no premises.
(e) Which line of that proof uses $\mathrm{LEM}$ , and on which statement? Does the proof say which pair $(a, b)$ works?

Solution.

(a) The inner box, lines 2–4, opens with $P$ and closes by $\mathrm{\neg I}$ at line 5, giving $\neg P$ . The outer box, lines 1–7, opens with $\neg(P \vee \neg P)$ and closes by $\mathrm{\neg I}$ at line 8.
(b) The rule that closes a box is decided by what is written after it, not by the box. Line 8 writes $\neg\neg(P \vee \neg P)$ , the negation of the box’s assumption $\neg(P \vee \neg P)$ , and that is what $\mathrm{\neg I}$ writes. $\mathrm{RAA}$ would be needed only to write $P \vee \neg P$ after the same box.
(c) A method that takes any method $f$ , sending proofs of $P \vee \neg P$ to proofs of $\bot$ , and returns a proof of $\bot$ . The derivation provides one: label a proof of $P$ “left” and apply $f$ , which gives a proof of $\neg P$ ; label that proof “right” and apply $f$ again.
(d) False. Such a derivation would also be a derivation with all the rules. Together with the derivation of $P \vee \neg P$ from no premises (Proposition 2.5.3), $\mathrm{\neg E}$ would derive $\bot$ from no premises. No derivation does that: by Theorem 4.7.2, or by the soundness statement for predicate logic in Section 7.2 when $P$ or the derivation involves quantifiers or equality, $\bot$ would be true under every valuation (in every structure under every assignment), and no valuation, and no structure and assignment, makes $\bot$ true.
(e) The first line, which splits on “ $\sqrt 2^{\sqrt 2}$ is rational” by $\mathrm{LEM}$ . The proof does not say which pair works: it shows that $(\sqrt 2, \sqrt 2)$ works in the first case and $(\sqrt 2^{\sqrt 2}, \sqrt 2)$ in the second, and does not decide which case holds.

Exercise (A2: Drill)

Answer each in a line. (a)–(d) ask whether a derivation avoids $\mathrm{RAA}$ ; (e), (f) and (i) read proofs under BHK; the rest apply the section to proofs and claims.

(a) A derivation’s last line is $P$ , by $\mathrm{RAA}$ from a box on $\neg P$ . Is the derivation intuitionistic?
(b) A box opens with $P$ and ends in $\bot$ , and the next line is $\neg P$ . Which rule? Is the step intuitionistic?
(c) Is $\neg\neg\neg P \vdash \neg P$ derivable without $\mathrm{RAA}$ ?
(d) A classmate derives $\neg P \vee \neg Q$ from $\neg(P \wedge Q)$ and says no $\mathrm{RAA}$ was used. What do you check first?
(e) Under BHK, what does a proof of $(P \wedge Q) \to P$ do?
(f) Under BHK, what must a proof of $\exists n \in \mathbb{N} \; (n^2 > 50)$ hand over?
(g) “ $x \ge 0$ or $x < 0$ ; we consider the two cases.” What is this in logical form, and does the book flag it?
(h) “Suppose $\sqrt 3$ is rational. … a contradiction. Hence $\sqrt 3$ is irrational.” Is this intuitionistic?
(i) A proof establishes $\neg\neg\exists x\, \varphi$ . What does it hand over under BHK?
(j) True or false: every intuitionistic derivation is a derivation of Chapters 1–7.
(k) May an intuitionist argue “not every element of $A$ is positive, so some element of $A$ is not positive”?
(l) Which line of the proof of Theorem 8.7.1 would an intuitionist reject, and would she reject its conclusion?

Solution.

(a) No: the last line is justified by $\mathrm{RAA}$ .
(b) $\mathrm{\neg I}$ ; yes.
(c) Yes: Example (Three negations become one) derives it, and its derivation uses no $\mathrm{RAA}$ .
(d) Every line and every cited result. That direction of De Morgan’s law is in the right column of the table in “Which laws survive without RAA”, so some line is $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ , or cites a result derived with one of them.
(e) It takes any pair, a proof of $P$ and a proof of $Q$ , and returns the first component.
(f) A natural number together with a proof of the instance: for example $8$ , with $8 \in \mathbb{N}$ and $8^2 = 64 > 50$ .
(g) $\mathrm{LEM}$ in form, an instance of trichotomy for the real numbers. The book does not flag it: it rests on an axiom (“The book’s position”).
(h) Yes: the goal is a negation, “ $\sqrt 3$ is not rational”, and the box on “ $\sqrt 3$ is rational” closes by $\mathrm{\neg I}$ .
(i) No object: only a method that turns any refutation of $\exists x\, \varphi$ into a proof of $\bot$ .
(j) True. It uses some of the rules of Chapters 1–7 and no others, so it is a derivation, and soundness applies to it.
(k) Not in general: that step is Proposition 6.2.3 (a), the bounded form of Proposition 6.2.1 (a), derived with $\mathrm{RAA}$ and in the right column of the table. She asks for the element.
(l) The first line, the $\mathrm{LEM}$ split on “ $s$ is rational”. Not the conclusion: the second proof in “Irrational powers, with and without a witness” proves it with a named witness, $(\sqrt 2, \log_2 9)$ , and no classical rule.

B. Practice

Exercise (B1: Double negation of double negation elimination)

Derive $\vdash \neg\neg(\neg\neg P \to P)$ without $\mathrm{RAA}$ , and name the rule on every line.

Hint: the goal is a negation; compare the derivation of the proposition in this section.

Solution. The goal is a negation, so we open a $\mathrm{\neg I}$ box on $\neg(\neg\neg P \to P)$ , with the goal $\bot$ . The assumption clashes only with $\neg\neg P \to P$ , an implication, which $\mathrm{{\to}I}$ builds from a box on $\neg\neg P$ that ends in $P$ . The first way to have $P$ is to assume it: inside a box on $P$ , the implication holds by $\mathrm{{\to}I}$ with $P$ repeated, and it clashes with the assumption, so $\neg P$ follows by $\mathrm{\neg I}$ . Now $\neg P$ clashes with any $\neg\neg P$ , so a second box on $\neg\neg P$ reaches $\bot$ , $\mathrm{\bot E}$ writes $P$ , and the implication is built a second time.

\neg (\neg\neg P \to P)

asm, for

\mathrm{{\neg}I}

P

asm, for

\mathrm{{\neg}I}

\neg\neg P

asm, for

\mathrm{{{\to}}I}

P

\mathrm{R}

\neg\neg P \to P

\mathrm{{{\to}}I}

3–4

\bot

\mathrm{{\neg}E}

5, 1

\neg P

\mathrm{{\neg}I}

2–6

\neg\neg P

asm, for

\mathrm{{{\to}}I}

\bot

\mathrm{{\neg}E}

7, 8

P

\mathrm{{\bot}E}

\neg\neg P \to P

\mathrm{{{\to}}I}

8–10

\bot

\mathrm{{\neg}E}

11, 1

\neg\neg (\neg\neg P \to P)

\mathrm{{\neg}I}

1–12

Lines 1, 2, 3, and 8 are assumptions. Line 4 repeats line 2 into the box of line 3, since $\mathrm{{\to}I}$ needs $P$ as a line of that box itself. Line 9 is $\mathrm{\neg E}$ on $\neg P$ (line 7) and its negation $\neg\neg P$ (line 8). Every box closes by $\mathrm{{\to}I}$ or $\mathrm{\neg I}$ , so no $\mathrm{RAA}$ is used. Unlike the derivation of the proposition in this section, this one uses $\mathrm{\bot E}$ , at line 10. For a letter $p$ , the sequent $\vdash \neg\neg p \to p$ itself has no derivation without $\mathrm{RAA}$ (the optional Section 8.8 proves it with a two-stage model); its double negation has one.

Exercise (B2: Reading proofs as methods)

(a) Give the BHK reading of a proof of $P \to \neg\neg P$ , and describe such a proof.
(b) The same for $(P \to Q) \to (\neg Q \to \neg P)$ .
(c) The same for $\forall n \in \mathbb{N} \; \exists m \in \mathbb{N} \; (m > n)$ , over the natural numbers.
(d) A proof of an existence claim $\exists x\, \varphi$ opens with “suppose that no $x$ satisfies $\varphi$ ” and reaches a contradiction. Without a classical rule, which of $\neg\neg\exists x\, \varphi$ and $\exists x\, \varphi$ does it prove? What does it provide under the BHK reading?

Solution.

(a) A method that takes any proof $p$ of $P$ and returns a proof of $\neg\neg P$ , that is, a method that takes any proof $f$ of $\neg P$ and returns a proof of $\bot$ . The method: given $p$ , and then given $f$ , apply $f$ to $p$ . This is the BHK reading of Proposition 2.5.1 (a).
(b) A method that takes any method $h$ (from proofs of $P$ to proofs of $Q$ ) and returns a proof of $\neg Q \to \neg P$ : a method that takes any $g$ (from proofs of $Q$ to proofs of $\bot$ ) and returns a proof of $\neg P$ , that is, a method from proofs of $P$ to proofs of $\bot$ . The method: given $h$ , $g$ , and a proof $p$ of $P$ , compute $g(h(p))$ . This is the BHK reading of Proposition 2.3.2, whose derivation uses no $\mathrm{RAA}$ .
(c) Unfolding the bounded quantifiers (Definition 5.1.1): a method that takes any object $n$ and a proof that $n \in \mathbb{N}$ , and returns an object $m$ together with a proof of $m \in \mathbb{N} \wedge m > n$ . The method: given $n$ and the proof of $n \in \mathbb{N}$ , output $m = n + 1$ , with the proofs that $n + 1 \in \mathbb{N}$ and $n + 1 > n$ .
(d) The box opens with $\neg\exists x\, \varphi$ and ends in $\bot$ , so $\mathrm{\neg I}$ closes it with $\neg\neg\exists x\, \varphi$ . Writing $\exists x\, \varphi$ instead is $\mathrm{RAA}$ (or $\mathrm{\neg\neg E}$ after $\mathrm{\neg I}$ ), a classical step. Under the BHK reading the proof provides a method that takes any proof that nothing satisfies $\varphi$ and returns a proof of $\bot$ . It provides no object: a proof of $\exists x\, \varphi$ would have to name one.

Exercise (B3: Where the witness goes missing)

In the derivation of Proposition 6.2.1 (a), which step makes the existence claim without a witness? Why does no witness appear, although line 4 is an $\mathrm{\exists I}$ ?

Solution. Two lines are classical: line 6, an $\mathrm{RAA}$ that writes the instance $\varphi[x_0/x]$ after a box on its negation, and line 9, the $\mathrm{RAA}$ that writes the conclusion $\exists x\, \neg\varphi$ . Line 6 produces no existence claim. Line 9 is the step that asserts existence: it closes the box on $\neg\exists x\, \neg\varphi$ , which ends in $\bot$ , and writes $\exists x\, \neg\varphi$ . Closed by $\mathrm{\neg I}$ , the same box would give only $\neg\neg\exists x\, \neg\varphi$ .

No witness appears because no $\mathrm{\exists I}$ produces the conclusion. Line 4 does derive $\exists x\, \neg\varphi$ from the instance $\neg\varphi[x_0/x]$ , but that instance is the assumption of the box $3\text{–}5$ , used only to clash with line 2 and discharged at line 6. The name $x_0$ is the flagged name of the $\mathrm{\forall I}$ box $3\text{–}6$ : an arbitrary object, not a particular one. Line 4 is unavailable at line 9, and the conclusion there is justified by $\mathrm{RAA}$ from the box $2\text{–}8$ , which names nothing. Under the BHK reading, line 9 asserts “something fails $\varphi$ ” and hands over no object that fails it.

Exercise (B4: Census of the classical results)

(a) Which labeled results of Chapter 2 (propositions and theorems) were derived with $\mathrm{RAA}$ , directly or through $\mathrm{\neg\neg E}$ , $\mathrm{LEM}$ , or a cited result that uses one of them? (b) The same question for Chapters 3 to 7, counting lemmas, corollaries, and the step TAUT of Definition 4.8.1 as well.

Solution.

(a) Seven: Proposition 2.5.1 (b); Proposition 2.5.2; Proposition 2.5.3; Proposition 2.5.5 (d); Proposition 2.5.6 (b), through $\mathrm{LEM}$ ; Theorem 2.5.7, whose proof uses all three: $\mathrm{RAA}$ in ①, $\mathrm{\neg\neg E}$ in ②, $\mathrm{LEM}$ in ③; and Proposition 2.5.4. Every other proposition and theorem of Chapter 2 uses no classical rule, including Theorem 2.2.1, whose box closes by $\mathrm{\neg I}$ .
(b) Chapter 3: the direction $(\Leftarrow)$ of Proposition 3.2.2 (b), whose box closes by $\mathrm{RAA}$ . Chapter 4: Lemma 4.8.3, through $\mathrm{LEM}$ , and with it Theorem 4.8.4 and the direction $(\Leftarrow)$ of Corollary 4.8.5; the step TAUT of Definition 4.8.1, licensed through Corollary 4.8.5; and, in the optional Section 4.10, Lemma 4.10.2, whose key step uses $\mathrm{RAA}$ through Proposition 3.2.2, with Theorem 4.10.5 and Theorem 4.10.6, as the fold after the proof of Theorem 4.10.5 says. Chapter 5: none. In Chapter 6: Proposition 6.2.1 (a); the direction $\vdash$ of Proposition 6.2.2; the direction $\vdash$ of Proposition 6.2.3 (a); the two directions $\dashv$ of Proposition 6.2.7, in (d) and in (e), both through $\mathrm{LEM}$ ; Proposition 6.2.5, as proved, since its box assumes $a \ne b$ and concludes $a = b$ ; and Proposition 6.3.1, through Corollary 4.8.5. Chapter 7: none derived; the classical theorems of Section 7.6, first-order completeness and what rests on it, are stated without proof, so the question does not reach them.

The results of Sections 4.4, 4.5 and 4.9, such as the standard equivalences and monotonicity, are not on the list: they are statements about valuations and derive nothing, and their remarks mention $\mathrm{RAA}$ only as history.

Exercise (B5: Behind two negations, and one instance)

Derive each without $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ , $\mathrm{LEM}$ or TAUT, and without citing a result derived with them.

(a) $\neg(P \wedge Q) \vdash \neg\neg(\neg P \vee \neg Q)$ .
(b) $P \to Q \vdash \neg\neg(\neg P \vee Q)$ .
(c) $\vdash (P \vee \neg P) \to (\neg\neg P \to P)$ .
(d) Which row of the table in “Which laws survive without RAA” does each of (a)–(c) concern?

Solution.

(a) The goal is a negation, so a $\mathrm{\neg I}$ box on $\neg(\neg P \vee \neg Q)$ . That assumption clashes with any disjunction $\neg P \vee \neg Q$ , so we manufacture a side, as in the derivation of $\neg\neg(P \vee \neg P)$ in this section, twice:
1 $\neg (P \wedge Q)$
2 $\neg (\neg P \vee \neg Q)$ asm, for $\mathrm{{\neg}I}$
3 $P$ asm, for $\mathrm{{\neg}I}$
4 $Q$ asm, for $\mathrm{{\neg}I}$
5 $P \wedge Q$ $\mathrm{{\wedge}I}$ 3, 4
6 $\bot$ $\mathrm{{\neg}E}$ 5, 1
7 $\neg Q$ $\mathrm{{\neg}I}$ 4–6
8 $\neg P \vee \neg Q$ $\mathrm{{\vee}I}$ 7
9 $\bot$ $\mathrm{{\neg}E}$ 8, 2
10 $\neg P$ $\mathrm{{\neg}I}$ 3–9
11 $\neg P \vee \neg Q$ $\mathrm{{\vee}I}$ 10
12 $\bot$ $\mathrm{{\neg}E}$ 11, 2
13 $\neg\neg (\neg P \vee \neg Q)$ $\mathrm{{\neg}I}$ 2–12
(b) The same plan, with the premise supplying $Q$ inside the box on $P$ :
1 $P \to Q$
2 $\neg (\neg P \vee Q)$ asm, for $\mathrm{{\neg}I}$
3 $P$ asm, for $\mathrm{{\neg}I}$
4 $Q$ $\mathrm{{{\to}}E}$ 1, 3
5 $\neg P \vee Q$ $\mathrm{{\vee}I}$ 4
6 $\bot$ $\mathrm{{\neg}E}$ 5, 2
7 $\neg P$ $\mathrm{{\neg}I}$ 3–6
8 $\neg P \vee Q$ $\mathrm{{\vee}I}$ 7
9 $\bot$ $\mathrm{{\neg}E}$ 8, 2
10 $\neg\neg (\neg P \vee Q)$ $\mathrm{{\neg}I}$ 2–9
(c) Two implications, so two $\mathrm{{\to}I}$ boxes; inside, the instance of excluded middle is used by cases:
1 $P \vee \neg P$ asm, for $\mathrm{{{\to}}I}$
2 $\neg\neg P$ asm, for $\mathrm{{{\to}}I}$
3 $P$ asm, for $\mathrm{{\vee}E}$
4 $P$ $\mathrm{R}$ 3
5 $\neg P$ asm, for $\mathrm{{\vee}E}$
6 $\bot$ $\mathrm{{\neg}E}$ 5, 2
7 $P$ $\mathrm{{\bot}E}$ 6
8 $P$ $\mathrm{{\vee}E}$ 1, 3–4, 5–7
9 $\neg\neg P \to P$ $\mathrm{{{\to}}I}$ 2–8
10 $(P \vee \neg P) \to (\neg\neg P \to P)$ $\mathrm{{{\to}}I}$ 1–9

Every box closes by $\mathrm{\neg I}$ , $\mathrm{{\to}I}$ or $\mathrm{\vee E}$ . No line uses $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ , and no line cites a result. In (c), line 6 is $\mathrm{\neg E}$ on $\neg P$ (line 5) and $\neg\neg P$ (line 2).
(d)
- (a) concerns De Morgan (d): it is Glivenko’s double negation of that row’s conclusion. (b) concerns implication as a disjunction (b), in the same way. (c) concerns double negation (b): one instance of excluded middle, taken as a hypothesis, gives double-negation elimination at that instance with no further classical step. (The optional Section 8.8’s Exercise C1 shows that such a step need not run back: one instance of excluded middle gives Peirce’s law for that letter, and that instance of Peirce’s law does not give the instance of excluded middle.)

Marking scheme. (10 points) - 3: (a). - 3: (b). - 3: (c). - 1: (d). - For each derivation: 1 for the skeleton (the outer $\mathrm{\neg I}$ or $\mathrm{{\to}I}$ box and its last line); 2 for the inside, each clash named.

Fatal errors (0 for that derivation): a line justified by $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ ; a line justified by TAUT (each sequent is a tautology, so one TAUT line would “derive” it, but TAUT rests on completeness, which splits on atoms by $\mathrm{LEM}$ ); citing Proposition 2.5.5 (d), Proposition 2.5.6 (b) or Proposition 2.5.1 (b), each derived with $\mathrm{RAA}$ .

C. Going deeper

Exercise (C1: More witnesses)

This section proved that $\log_2 9$ is irrational; here are variants.

(a) Show that $a = \sqrt 2$ and $b = \log_2 25$ are irrational numbers with $a^b$ rational.
(b) For which integers $m \ge 2$ are $a = \sqrt 2$ and $b = \log_2(m^2)$ irrational numbers with $a^b$ rational? Prove your answer.

Solution (Hint 1). Compute $a^b$ first; it does not depend on whether $b$ is rational. Then write $m = 2^k r$ with $r$ odd.

Solution (Hint 2). Suppose $\log_2(m^2) = p/q$ with integers $p$ and $q \ge 1$ ; then $2^p = m^{2q}$ .

Solution.

(a) First, $a^b = (2^{1/2})^{\log_2 25} = 2^{(\log_2 25)/2} = 2^{\log_2 5} = 5$ , since $\log_2 25 = 2\log_2 5$ ; this is rational. Next, $a = \sqrt 2$ is irrational by Theorem 2.2.1. Finally, suppose that $\log_2 25 = p/q$ with integers $p$ and $q \ge 1$ . Since $25 > 1 = 2^0$ and $t \mapsto 2^t$ is increasing, $\log_2 25 > 0$ , so $p \ge 1$ . Raising $2^{p/q} = 25$ to the power $q$ gives $2^p = 25^q$ . The left side is even because $p \ge 1$ , and the right side is odd, being a product of odd factors. No integer is both, so $\log_2 25$ is irrational.
(b) Answer: exactly the integers $m \ge 2$ that are not powers of $2$ .

For every $m \ge 2$ , $a = \sqrt 2$ is irrational and $a^b = \bigl( 2^{1/2} \bigr)^{\log_2 (m^2)} = 2^{\log_2 m} = m ,$ which is rational. So the question is only when $b = \log_2(m^2) = 2\log_2 m$ is irrational. Write $m = 2^k r$ with $k \in \mathbb{N}$ and $r$ odd, $r \ge 1$ .

If $r = 1$ , then $m = 2^k$ with $k \ge 1$ , and $b = 2k$ is rational: these $m$ fail.

If $r \ge 3$ , suppose that $b = p/q$ with integers $p$ and $q \ge 1$ . Since $m \ge 2 > 1$ , $b > 0$ , so $p \ge 1$ . Raising $2^{p/q} = m^2$ to the power $q$ gives $2^p = m^{2q} = 2^{2kq} r^{2q} .$ Since $r^{2q} \ge 3 > 1$ , the right side exceeds $2^{2kq}$ , so $p > 2kq$ . Dividing by $2^{2kq}$ gives $r^{2q} = 2^{p - 2kq}$ with $p - 2kq \ge 1$ . The left side is odd, a product of odd factors, and the right side is even. No integer is both, so $b$ is irrational: these $m$ work. The smallest are $m = 3, 5, 6, 7$ . The cases $m = 3$ and $m = 5$ are the example of this section and part (a).

Marking scheme. (10 points) - 2: (a) $a^b = 5$ , with the exponent laws used. - 2: (a) $\log_2 25$ irrational, with $p \ge 1$ justified by $\log_2 25 > 0$ and the parity clash $2^p = 25^q$ . - 2: (b) $a^b = m$ for every $m$ , so only the rationality of $b$ matters. - 1: (b) powers of $2$ excluded, with $b = 2k$ rational. - 3: (b) for $m = 2^k r$ , $r \ge 3$ odd, the clash $r^{2q} = 2^{p - 2kq}$ with $p - 2kq \ge 1$ (or an equivalent comparison of the odd parts of $2^p$ and $m^{2q}$ ). Fatal errors (0 for the step): concluding irrationality of $b$ from “ $m$ is irrational” or “ $\log_2 m$ is not an integer”; a parity clash with $p$ possibly $0$ or negative left unaddressed.

Exercise (C2: Modus ponens survives Kolmogorov’s translation)

For statements built from letters by $\wedge$ , $\vee$ , $\to$ , and $\neg$ , define the translation $K$ by putting $\neg\neg$ in front of every subformula: $KP = \neg\neg P \ \text{for a letter } P, \qquad K(\varphi \circ \psi) = \neg\neg(K\varphi \circ K\psi), \qquad K(\neg\varphi) = \neg\neg\neg K\varphi ,$ where $\circ$ is any of $\wedge$ , $\vee$ , $\to$ . Chapter 2’s Exercise (B1: With and without the new rule, used later) (a) derives $\neg\neg P, \ \neg\neg(P \to Q) \vdash \neg\neg Q$ without $\mathrm{RAA}$ (in its printed solution).

(a) Show that every $K\psi$ has the form $\neg\neg X$ for some statement $X$ .
(b) Deduce that $K(\varphi \to \psi), \ K\varphi \vdash K\psi$ without $\mathrm{RAA}$ , for all statements $\varphi$ and $\psi$ .

Solution (Hint 1). Put $K\varphi$ and $K\psi$ in for $P$ and $Q$ in the Chapter 2 sequent. Which of its two premises is $K(\varphi \to \psi)$ ?

Solution (Hint 2). The conclusion you get has two negations too many. Look for a result of Section 2.2 that removes negations without $\mathrm{\neg\neg E}$ .

Solution.

(a) By the definition, each of the three clauses produces a statement whose first two symbols are $\neg\neg$ : $KP = \neg\neg P$ , $K(\varphi \circ \psi) = \neg\neg(K\varphi \circ K\psi)$ , and $K(\neg\varphi) = \neg\neg(\neg K\varphi)$ . So $K\psi = \neg\neg X$ , with $X$ the letter, $K\varphi \circ K\psi$ , or $\neg K\varphi$ , respectively. No induction is needed, since the outermost clause alone decides the first two symbols.
(b) Three steps, each without $\mathrm{RAA}$ .

① The derivation of Exercise (B1: With and without the new rule, used later) (a) uses no $\mathrm{RAA}$ , so its sequent may be used as a derived rule (Definition 2.3.1) with the statements $K\varphi$ and $K\psi$ in place of $P$ and $Q$ : $\neg\neg K\varphi, \ \neg\neg(K\varphi \to K\psi) \vdash \neg\neg K\psi .$ Its second premise is $K(\varphi \to \psi)$ itself, by the clause for $\to$ .

② The first premise follows from $K\varphi$ by $\mathrm{\neg\neg I}$ (Proposition 2.5.1 (a), derived without $\mathrm{RAA}$ ): a box on $\neg K\varphi$ clashes at once with $K\varphi$ .

③ By (a), $K\psi = \neg\neg X$ , so the conclusion of ① is $\neg\neg\neg\neg X = \neg\neg\neg(\neg X)$ . Example (Three negations become one) derives $\neg\neg\neg P \vdash \neg P$ without $\mathrm{RAA}$ ; with $\neg X$ in place of $P$ it gives $\neg\neg\neg(\neg X) \vdash \neg(\neg X)$ , that is, $\neg\neg K\psi \vdash K\psi$ .

Chaining ②, ①, and ③ gives $K(\varphi \to \psi), \ K\varphi \vdash K\psi$ , and no step is $\mathrm{RAA}$ : the derived rules used were all derived without it. In words, modus ponens survives the translation intuitionistically. (This is the translation that puts $\neg\neg$ in front of every subformula. In the Gödel–Gentzen translation of the history above, $\varphi \to \psi$ translates without an outer $\neg\neg$ , and modus ponens survives trivially.)

Marking scheme. (10 points) - 2: (a) every clause of $K$ begins with $\neg\neg$ , read off the outermost clause. - 3: (b) the Chapter 2 sequent instantiated with $K\varphi$ , $K\psi$ , and its second premise recognized as $K(\varphi \to \psi)$ . - 2: (b) $\neg\neg K\varphi$ from $K\varphi$ by $\mathrm{\neg\neg I}$ , named as RAA-free. - 3: (b) $\neg\neg K\psi \vdash K\psi$ by the triple-negation result applied to $\neg X$ , using (a). Fatal errors (0 for the step): removing the extra negations by $\mathrm{\neg\neg E}$ (a classical step); assuming $K\psi$ is a letter.

R. Review

Exercise (R1)

A set $A$ of real numbers has a maximum if some element $m$ of $A$ satisfies $a \le m$ for every $a \in A$ . Write “ $A$ has no maximum” in positive form, with no $\neg$ in front of a quantifier, and prove that the interval $(0, 1)$ has no maximum.

Solution. This uses the method of Chapter 6, Section 6.2: negate quantifier by quantifier, keeping the bounds (Proposition 6.2.3; compare Example (Three negations from analysis)). In symbols, “ $A$ has a maximum” is $\exists m \in A \; \forall a \in A \; (a \le m)$ . Its negation becomes, step by step, $\begin{aligned} \neg\exists m \in A \; \forall a \in A \; (a \le m) &\dashv\vdash \forall m \in A \; \neg\forall a \in A \; (a \le m) \\ &\dashv\vdash \forall m \in A \; \exists a \in A \; \neg(a \le m), \end{aligned}$ by part (b) of Proposition 6.2.3, and then part (a) used under the $\forall$ , as Proposition 6.2.4 of Section 6.2 allows. For real numbers $\neg(a \le m)$ says $a > m$ . So the positive form is $\forall m \in A \; \exists a \in A \; (a > m):$ every element of $A$ is exceeded by some element of $A$ .

Now let $A = (0, 1)$ and let $m \in (0, 1)$ . Take $a \mathrel{:=} (m + 1)/2$ , which depends on $m$ . Then $a - m = \frac{1 - m}{2} > 0 \quad \text{and} \quad 1 - a = \frac{1 - m}{2} > 0,$ since $m < 1$ , so $m < a < 1$ ; with $m > 0$ this gives $0 < a < 1$ . So $a \in (0, 1)$ and $a > m$ . Since $m \in (0, 1)$ was arbitrary, the positive form holds for $(0, 1)$ , and by the interderivability above, $(0, 1)$ has no maximum. Going back from the positive form needs no classical step, but not by the route through Proposition 6.2.4, which uses both directions of (a). Go directly instead. Fix $m$ with $m \in A$ , as the flagged name of a $\mathrm{\forall I}$ box. The positive form gives $\exists a \in A \; (a > m)$ by $\mathrm{\forall E}$ and $\mathrm{{\to}E}$ ; inside an $\mathrm{\exists E}$ box, $a > m$ gives $\neg(a \le m)$ by trichotomy, and $\mathrm{\exists I}$ gives $\exists a \in A \; \neg(a \le m)$ . The direction $\dashv$ of (a) gives $\neg\forall a \in A \; (a \le m)$ , and $\mathrm{{\to}I}$ and $\mathrm{\forall I}$ give $\forall m \in A \; \neg\forall a \in A \; (a \le m)$ . The direction $\dashv$ of (b) then gives $\neg\exists m \in A \; \forall a \in A \; (a \le m)$ . Both directions $\dashv$ are derived without $\mathrm{RAA}$ , so this half of the argument uses no classical step beyond the order axioms.

Exercise (R2)

Give a Fitch derivation of $P \to (Q \vee R), \ Q \to S, \ R \to S \vdash P \to S$ , and write it as one sentence of prose.

Solution. This uses Chapter 1’s rules: $\mathrm{{\to}I}$ (Definition 1.4.1), $\mathrm{{\to}E}$ (Definition 1.3.1), and $\mathrm{\vee E}$ (Definition 1.6.1). The goal is an implication, so a box on $P$ with the goal $S$ . Inside it, the first premise gives $Q \vee R$ , which we use by cases; each case reaches $S$ through one of the other premises.

P \to (Q \vee R)

Q \to S

R \to S

P

asm, for

\mathrm{{{\to}}I}

Q \vee R

\mathrm{{{\to}}E}

1, 4

Q

asm, for

\mathrm{{\vee}E}

S

\mathrm{{{\to}}E}

2, 6

R

asm, for

\mathrm{{\vee}E}

S

\mathrm{{{\to}}E}

3, 8

S

\mathrm{{\vee}E}

5, 6–7, 8–9

P \to S

\mathrm{{{\to}}I}

4–10

Line 10 may cite line 5, since both lie in the box of line 4, which is still open; the case boxes end with $S$ as lines of their own. In prose: “Suppose $P$ ; then $Q$ or $R$ holds by the first premise, and $S$ follows in the case $Q$ by the second premise and in the case $R$ by the third, so $P$ implies $S$ .” Each premise is cited where it is used, as Definition 8.3.2 requires for every $\mathrm{{\to}E}$ on a hypothesis; the first premise is also the reason the two cases exhaust. The closing “so $P$ implies $S$ ” is the closing line of $\mathrm{{\to}I}$ , which Definition 8.3.2 allows to go unsaid.

Exercise (R3)

Decide with a truth table whether $(P \to Q) \to Q \models P \vee Q$ , reading $P$ and $Q$ as atoms. If the entailment holds, give a derivation of $(P \to Q) \to Q \vdash P \vee Q$ .

Solution. This item reaches back within this volume, since there is no earlier one: it uses the tables of Chapter 4 and the derivations of Chapter 2.

The table. Work backwards from F, as in Example (Working backwards from F) and the entailments of Definition 4.5.3. A refuting row needs $P \vee Q$ false, so $P$ and $Q$ are both false. In that row $P \to Q$ is true, so the premise $(P \to Q) \to Q$ is “T $\to$ F”, which is false. So no row makes the premise true and the conclusion false, and the entailment holds. The full table agrees: $\begin{array}{cc|ccc} P & Q & P \to Q & (P \to Q) \to Q & P \vee Q \\ \hline \mathrm{T} & \mathrm{T} & \mathrm{T} & \mathrm{T} & \mathrm{T} \\ \mathrm{T} & \mathrm{F} & \mathrm{F} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{T} & \mathrm{T} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{F} & \mathrm{T} & \mathrm{F} & \mathrm{F} \end{array}$

The derivation. The goal is a disjunction with neither side in hand, and the premise gives $Q$ only once $P \to Q$ is available. We are stuck, so we open an $\mathrm{RAA}$ box on $\neg(P \vee Q)$ (Definition 2.5.1). Inside it, $P \to Q$ is built by a box on $P$ : $\mathrm{\vee I}$ gives $P \vee Q$ , which clashes with the assumption, and $\mathrm{\bot E}$ writes $Q$ . Then the premise gives $Q$ , and $\mathrm{\vee I}$ clashes again.

(P \to Q) \to Q

\neg (P \vee Q)

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\to}}I}

P \vee Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

4, 2

Q

\mathrm{{\bot}E}

P \to Q

\mathrm{{{\to}}I}

3–6

Q

\mathrm{{{\to}}E}

1, 7

P \vee Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

9, 2

P \vee Q

\mathrm{RAA}

2–10

The one classical line is line 11. Closing the same box by $\mathrm{\neg I}$ instead gives $\neg\neg(P \vee Q)$ , and then the derivation is intuitionistic: the premise yields the double negation of its classical conclusion, the pattern of Glivenko’s theorem in the remark of this section.

No derivation of this sequent avoids $\mathrm{RAA}$ or one of its equivalents; the optional Section 8.8 proves it with a two-stage model. (With $\bot$ in place of $Q$ , the sequent would turn $\neg\neg P$ into $P$ without any further classical step, and Chapter 4’s optional theorem in Section 4.7 shows that $\neg\neg P \vdash P$ needs $\mathrm{RAA}$ .)

Exercise (R4)

Prove that for every integer $n$ , $n^3 - n$ is divisible by $3$ .

Solution. The tool is proof by cases on the remainder of $n$ on division by $3$ : every integer $n$ is $3k$ , $3k + 1$ , or $3k + 2$ for some integer $k$ . This is a school fact, of the same kind as “every integer is even or odd” in Chapter 2. It is $\mathrm{\vee E}$ with three cases (Definition 1.6.1, used twice), and in each case $\mathrm{\exists I}$ (Definition 5.5.1) with an explicit witness. First factor: $n^3 - n = (n - 1)\, n\, (n + 1) .$ Let $n$ be an integer, and let $k$ be an integer with $n = 3k$ , $n = 3k + 1$ , or $n = 3k + 2$ .

Case $n = 3k$ . Then $n^3 - n = 3 \cdot \bigl( (3k - 1)\, k\, (3k + 1) \bigr)$ .

Case $n = 3k + 1$ . Then $n^3 - n = (3k)(3k + 1)(3k + 2) = 3 \cdot \bigl( k\, (3k + 1)(3k + 2) \bigr)$ .

Case $n = 3k + 2$ . Then $n^3 - n = (3k + 1)(3k + 2)(3k + 3) = 3 \cdot \bigl( (3k + 1)(3k + 2)(k + 1) \bigr)$ .

In each case $n^3 - n = 3j$ for the integer $j$ in brackets, so $3 \mid n^3 - n$ . Since $n$ was arbitrary, this holds for every integer $n$ .

Why the look-alikes are worse. A proof by contradiction (“suppose $3 \nmid n^3 - n$ …”) would have to reach exactly this case analysis and then clash with its assumption at the last line: a direct proof in costume (Example (A direct proof in costume)). Induction is closer, but it fits the statement badly: with base case $P(0)$ and the step from $n$ to $n + 1$ (Axiom 4.2.1) it proves the claim only for $n \in \mathbb{N}$ , and the negative integers $n = -m$ , $m \in \mathbb{Z}_{>0}$ , need a second argument, for instance $(-m)^3 - (-m) = -(m^3 - m)$ . The case split covers all integers at once.