4.7 Soundness

Chapter 3 ended on a question it could not answer. Section 3.1 searched for a derivation of $P \to Q \vdash Q \to P$ , and every route came back to the same gap; but a search that fails proves nothing, since a cleverer derivation might exist. The row that refutes affirming the consequent in Section 4.5, $p = \mathrm{F}$ and $q = \mathrm{T}$ , finds what the search could not: it makes $p \to q$ true and $q \to p$ false, and the search of Section 4.6 finds such rows whenever they exist. This section proves the theorem that turns such a row into a proof that no derivation exists. It is called soundness: whatever the rules derive is true in every row where the premises are true. The proof is the book’s first long proof about proofs, and it is an induction on the lines of a derivation.

4.7.1. What must be proved, and why it is not obvious

Remark. Two levels. This section speaks about the calculus from outside it.

Object level: written in the language	Meta level: claims about it, proved in ordinary mathematics
formulas; derivations, with their lines, boxes, justifications and printed purposes (“asm, for →I”, which the proof reads as the rule whose case applies)	“ $\Gamma \vdash \psi$ ”, “ $\Gamma \models \psi$ ”, “line $k$ is justified by $\mathrm{\vee E}$ ”, “ $\Gamma_k \models \varphi_k$ ”

Section 4.2’s checklist reads: objects, the lines of one derivation; property, $\Gamma_k \models \varphi_k$ (contexts are defined below); base cases, the premises and assumptions, which cite nothing; steps, one for each rule; principle, Theorem 4.2.2.

Second readingIs the proof circular?

The proof below argues by cases (“if $v(\varphi) = \mathrm{F}$ … if $v(\varphi) = \mathrm{T}$ ”) and by contradiction, in the metalanguage: the very patterns that $\mathrm{\vee E}$ and $\mathrm{RAA}$ record in the object language. That is not circular. The theorem is not meant to persuade someone who rejects reasoning by cases. It is a theorem of ordinary mathematics about a calculus, and what it rules out is a mismatch between the rules and the tables, of the kind the connective in the fold of Section 4.4 has.

Chapters 1 and 2 checked each rule as it arrived. $\mathrm{\wedge I}$ is safe because two true statements make a true conjunction (Section 1.2); $\mathrm{{\to}E}$ is safe because that is what “if … then” asserts (Section 1.3). Section 1.2 said once that Chapter 4 would prove it for every rule of Chapters 1 and 2 at once. Why is that more than collecting the separate checks?

The first attempt at a proof is: go down a derivation, line by line, and show that each line is true in every row in which the premises are true. For a derivation without boxes this works. Each line is a premise, or comes from earlier lines by a rule, and the rule turns true lines into a true line. But it fails at the first box. Here is the derivation of Proposition 2.3.2, written with atoms:

p \to q

\neg q

asm, for

\mathrm{{{\to}}I}

p

asm, for

\mathrm{{\neg}I}

q

\mathrm{{{\to}}E}

1, 3

\bot

\mathrm{{\neg}E}

4, 2

\neg p

\mathrm{{\neg}I}

3–5

\neg q \to \neg p

\mathrm{{{\to}}I}

2–6

Line 3 is $p$ , and the row $p = \mathrm{F}$ , $q = \mathrm{F}$ makes the premise $p \to q$ true and line 3 false. Line 5 is $\bot$ , which is false in every row. So the lines inside a box are not true in the rows where the premises are true, and the first attempt collapses. Yet the derivation is correct, and its last line $\neg q \to \neg p$ is true in every row making $p \to q$ true (Example (An implication and its contrapositive)).

What goes wrong is that a line inside a box is not claimed on the strength of the premises alone. Line 4 says: if $p \to q$ , $\neg q$ and $p$ all hold, then $q$ holds. That is a true claim about rows. Every line depends on the premises and on the assumptions of the boxes around it, and a correct statement about each line must mention both. Below we give this list a name: the context of the line.

4.7.2. Derivations of formulas

From now on the lines of a derivation carry formulas in the sense of Definition 4.1.1, with atoms $p, q, r, \dots$ . Nothing in the rules changes. Every rule was stated as a schema, whose letters $\varphi, \psi, \chi$ stand for arbitrary statements (Definition 1.2.1), so it applies to formulas as it stands, and Definition 1.4.2 and Definition 1.2.3 read the same with “formula” for “statement”. As Section 4.1 said, a derivation written with Chapter 2’s letters $P, Q$ is a pattern, and reading its letters as atoms, or as any formulas, gives a derivation of formulas.

Two conventions for the rest of the section. The primitive rules are those of Chapters 1 and 2 collected in Section 3.1: $\mathrm{R}$ , $\mathrm{\wedge I}$ , $\mathrm{\wedge E}$ , $\mathrm{{\to}I}$ , $\mathrm{{\to}E}$ , $\mathrm{\vee I}$ , $\mathrm{\vee E}$ , $\mathrm{\neg I}$ , $\mathrm{\neg E}$ , $\mathrm{\bot E}$ , $\mathrm{RAA}$ , $\mathrm{{\leftrightarrow}I}$ and $\mathrm{{\leftrightarrow}E}$ . The box rules among them are the five that cite a box: $\mathrm{{\to}I}$ , $\mathrm{\neg I}$ , $\mathrm{RAA}$ , $\mathrm{\vee E}$ and $\mathrm{{\leftrightarrow}I}$ . The other eight, $\mathrm{R}$ included, cite only lines; we call them the one-step rules.

A derivation may also use derived rules such as $\mathrm{MT}$ and $\mathrm{LEM}$ . A line citing one abbreviates a stretch of derivation in rules proved earlier, with the letters replaced by formulas (Definition 2.3.1), and Section 2.3 showed how to write it out: repeat the cited lines, then paste the derivation of the derived rule below them. Every chain of derived rules ends in primitive rules. So whenever $\Gamma \vdash \psi$ , there is also a derivation of $\psi$ from premises in $\Gamma$ that uses primitive rules only. That is the only kind of derivation the proof below has to consider.

4.7.3. The context of a line

Let a derivation have lines $1, \dots, n$ . We write $\varphi_k$ for the formula on line $k$ . The length of a derivation is its number of lines. The context of line $k$ is the list of the premises together with the assumptions of every box containing line $k$ : the statements the line depends on. We write it $\Gamma_k$ . The context of the last line is just the premises, since by Definition 1.4.2 the last line lies in no box. For lists of formulas $\Delta$ and $\Delta'$ , we write $\Delta \subseteq \Delta'$ when every formula of $\Delta$ occurs in $\Delta'$ .

Exercise C4 of Section 1.4 (Exercise (C4: The assumptions a line depends on, used later)) wrote such lists by hand, as sets of line numbers; its part (c) observed what Lemma 4.7.1 below proves.

The context of a line is everything that line depends on: the premises, and every assumption still open where the line stands.

In the derivation of Proposition 2.3.2 above, the boxes are $2\text{–}6$ and $3\text{–}5$ , and the contexts are:

Line	Formula	Boxes containing it	Context
1	$p \to q$	none	$p \to q$
2	$\neg q$	$2\text{–}6$	$p \to q, \ \neg q$
3, 4, 5	$p$ , $q$ , $\bot$	$2\text{–}6$ , $3\text{–}5$	$p \to q, \ \neg q, \ p$
6	$\neg p$	$2\text{–}6$	$p \to q, \ \neg q$
7	$\neg q \to \neg p$	none	$p \to q$

Quick check. In that derivation, which lines have $p$ in their context?

Solution. Lines 3, 4 and 5, the lines of the box opened by $p$ .

Now look at each line through its context. Line 3 is one of the formulas in its own context, so every row making the context true makes line 3 true. Line 4: every row making $p \to q$ and $p$ true makes $q$ true. Line 5: no row makes $p \to q$ , $\neg q$ , and $p$ all true (the first and third force $q$ ), so the context is unsatisfiable and it entails even $\bot$ (Section 4.5). Line 6: every row making $p \to q$ and $\neg q$ true makes $p$ false. Line 7: its context is the premise, and we know $p \to q \models \neg q \to \neg p$ . So on this derivation, every line $k$ satisfies $\Gamma_k \models \varphi_k .$ This is the statement that survives the boxes, and it is the one we shall prove for every line of every derivation.

Two facts about contexts, read off the scope rule, do the bookkeeping. The first says that citing an available line never involves an assumption the citing line does not have. The second says exactly what the context of a box’s last line is, when the box is cited by a box rule.

Lemma 4.7.1 (Contexts in a Derivation)

Let lines $i$ , $k$ and $a \le b$ belong to a derivation, and let $\Gamma_j$ denote the context of line $j$ .

(a) If line $i$ is available at line $k$ , then $\Gamma_i \subseteq \Gamma_k$ .
(b) If line $k$ is justified by a box rule citing the box whose first line is $a$ and whose last line is $b$ , then the formulas of $\Gamma_b$ are exactly those of $\Gamma_k$ together with $\varphi_a$ , the assumption of that box. We write this $\Gamma_b = \Gamma_k, \varphi_a$ .

Diagram. Labels: premises and the boxes around line k, a, varphi_a, b, varphi_b, k, varphi_k, context Gamma_k, varphi_a, context Gamma_k

Part (b): the last line of a cited box depends on everything line $k$ depends on, and on the box’s own assumption. The arrow is the citation.

Idea. Both parts compare two sets of boxes, since contexts differ only in the assumptions of the boxes around a line. For (a), the scope rule says that the boxes around line $i$ are among the boxes around line $k$ . For (b), the boxes around line $b$ should be the cited box itself and the boxes around line $k$ ; the danger is a further box inside the cited box that also ends on line $b$ , and the box rules forbid exactly that.

The proof reads both parts off the scope rule; it is in the fold below.

Second readingThe proof: reading the scope rule

Proof. (a) The premises belong to every context. Any other formula of $\Gamma_i$ is the assumption of a box containing line $i$ . Since line $i$ is available at line $k$ , every box containing line $i$ also contains line $k$ , by the scope rule of Definition 1.4.2. So that assumption belongs to $\Gamma_k$ .

(b) Let $B$ be the box from line $a$ to line $b$ . Since line $k$ cites $B$ , the box $B$ is available at line $k$ . By the scope rule, it ends before line $k$ , and the boxes containing $B$ are exactly the boxes containing line $k$ .

We find the boxes containing line $b$ . Every box containing line $k$ contains $B$ , and so contains line $b$ ; and $B$ contains line $b$ . Conversely, let $C$ be a box containing line $b$ . By Definition 1.4.2, two boxes are either disjoint or one inside the other; $C$ and $B$ share line $b$ , so $C = B$ , or $C$ contains $B$ , or $C$ lies inside $B$ . The last is impossible: then line $b$ , the last line of $B$ , would be a line of a box inside $B$ , and every box rule requires the last line of its box to be a line of that box itself, not of a box inside it (Definition 1.4.1, Definition 2.2.1, Definition 2.5.1, Definition 1.6.1, Definition 2.4.1). So $C = B$ , or $C$ is one of the boxes containing $B$ , which are the boxes containing line $k$ .

Hence the boxes containing line $b$ are $B$ and the boxes containing line $k$ . The assumption of $B$ is $\varphi_a$ , so $\Gamma_b$ consists of the premises, the assumptions of the boxes containing line $k$ , and $\varphi_a$ , which is $\Gamma_k$ together with $\varphi_a$ .

In the derivation of Proposition 2.3.2, line 6 cites the box $3\text{–}5$ by $\mathrm{\neg I}$ , and $\Gamma_5 = p \to q, \ \neg q, \ p$ is $\Gamma_6 = p \to q, \ \neg q$ with the assumption $p$ added, as (b) says. Line 5 cites lines 4 and 2, both available there, and $\Gamma_4$ and $\Gamma_2$ are contained in $\Gamma_5$ , as (a) says.

Second readingA box that ends inside another

Warning. Part (b) needs the box to be cited by a box rule. Definition 1.4.2 allows a box to end on the same line as a box inside it, and then its last line has a larger context. In the derivation below, the box $2\text{–}4$ is available at line 5, but $\Gamma_4 = p, \ q, \ r$ contains $r$ , the assumption of the inner box, as well as $q$ . No box rule may cite $2\text{–}4$ : its last line lies inside the box $3\text{–}4$ , not in $2\text{–}4$ itself. (This is why the derivation of Example (Regrouping a disjunction) needs its line 11.)

p

q

r

p

\mathrm{R}

p

\mathrm{R}

Quick check. In the derivation of Proposition 2.3.2 above, which case of the soundness claim handles line 5? Which lines’ contexts are involved, and why does $\Gamma_5 \models \bot$ hold?

Solution. Line 5 is $\bot$ , by $\mathrm{\neg E}$ citing lines 4 and 2: a one-step rule. Lines 4 and 2 are available at line 5, so by Lemma 4.7.1 (a), $\Gamma_4 = p \to q, \ \neg q, \ p$ and $\Gamma_2 = p \to q, \ \neg q$ are contained in $\Gamma_5 = p \to q, \ \neg q, \ p$ . The claim for the earlier lines gives $\Gamma_4 \models q$ and $\Gamma_2 \models \neg q$ . So a valuation making $\Gamma_5$ true would make both $q$ and $\neg q$ true, which clause (V2) of Definition 4.4.2 forbids. No valuation makes $\Gamma_5$ true, and $\Gamma_5 \models \bot$ holds because there is no row to check.

4.7.4. The soundness theorem

We can now state the theorem that Chapters 1 and 2 kept pointing to.

Theorem 4.7.2 (Soundness)

Let $\Gamma$ be a list of formulas and $\psi$ a formula. If $\Gamma \vdash \psi$ , then $\Gamma \models \psi$ .

Try it first (ten minutes): suppose line $k$ is $\varphi \to \psi$ , by $\mathrm{{\to}I}$ from a box that opens with $\varphi$ and ends with $\psi$ . Suppose you already know that every row making the context of line $k$ and $\varphi$ true makes $\psi$ true. Why is $\varphi \to \psi$ true in every row making the context of line $k$ true? What happens in the rows where $\varphi$ is false?

Idea. An attempt at the $\mathrm{{\to}I}$ case runs into two things. First, knowledge about the box’s last line is knowledge about rows making its own context true, which contains the assumption $\varphi$ ; that is why the claim must carry contexts, and why Lemma 4.7.1 (b) is needed. Second, the rows in which $\varphi$ is false are not covered by the box at all, and they need nothing: there $\varphi \to \psi$ is true by (V5). The same two moves handle every box rule. The Step roadmap:

① Prove the stronger claim $\Gamma_k \models \varphi_k$ for every line $k$ of a derivation in primitive rules.

② Use strong induction on $k$ (Theorem 4.2.2): a rule may cite any earlier line, not only the line just above, so the hypothesis must be available for all earlier lines at once.

③ Split on how line $k$ is justified. A premise or an assumption belongs to its own context. A one-step rule: apply the hypothesis to the cited lines, move their contexts into $\Gamma_k$ by Lemma 4.7.1 (a), and use one clause of Definition 4.4.2. A box rule: apply the hypothesis to each box’s last line, whose context is $\Gamma_k$ plus the box’s assumption by Lemma 4.7.1 (b), and argue about the rows where that assumption is true or false.

④ The last line lies in no box, so its context is the premises, all in $\Gamma$ ; adding the other formulas of $\Gamma$ keeps the entailment.

Before reading on: in the case of $\mathrm{RAA}$ (Claim 3 below), where does the proof use that $v(\neg\varphi)$ is $\mathrm{F}$ exactly when $v(\varphi)$ is $\mathrm{T}$ , and which half of that fact does it use?

Proof. Step 1 (reduction to primitive rules). Suppose $\Gamma \vdash \psi$ . As shown in the subsection on derivations of formulas, there is a derivation of $\psi$ whose premises all belong to $\Gamma$ and which uses primitive rules only. Fix one, with lines $1, \dots, n$ ; let $\varphi_k$ be the formula on line $k$ and $\Gamma_k$ its context.

Step 2 (the induction). For $k \in \mathbb{N}$ , let $S(k)$ be the statement: if $1 \le k \le n$ , then $\Gamma_k \models \varphi_k$ . We prove $S(k)$ for every $k$ by Theorem 4.2.2. So let $k \in \mathbb{N}$ , and assume $S(j)$ for every $j < k$ . If $k = 0$ or $k > n$ , there is nothing to prove, so let $1 \le k \le n$ . Every line and every box that line $k$ cites is available at line $k$ , and so lies before line $k$ (Definition 1.4.2). Hence the induction hypothesis $\Gamma_j \models \varphi_j$ holds for every line $j$ that line $k$ cites, and for the last line of every box it cites.

Let $v$ be a valuation that makes every formula of $\Gamma_k$ true. We show $v(\varphi_k) = \mathrm{T}$ ; since $v$ is arbitrary, this proves $\Gamma_k \models \varphi_k$ . By Definition 1.4.2, line $k$ is a premise, an assumption, or the conclusion of one primitive rule, and the three claims below treat these cases.

Step 3 (the cases).

Claim. If line $k$ is a premise or an assumption, then $v(\varphi_k) = \mathrm{T}$ .

Proof of Claim. A premise belongs to every context. An assumption opens a box, that box contains line $k$ , and so its assumption $\varphi_k$ belongs to $\Gamma_k$ . In both cases $\varphi_k$ is one of the formulas that $v$ makes true.

For the one-step rules we first record what the hypothesis gives for a cited line. If line $k$ cites line $i$ , then line $i$ is available at line $k$ , so $\Gamma_i \subseteq \Gamma_k$ by Lemma 4.7.1 (a). Hence $v$ makes every formula of $\Gamma_i$ true, and the induction hypothesis $\Gamma_i \models \varphi_i$ gives $v(\varphi_i) = \mathrm{T} \quad \text{for every line } i \text{ cited by line } k . \tag{$\ast$}$

Claim. If line $k$ is justified by a one-step rule, then $v(\varphi_k) = \mathrm{T}$ .

Proof of Claim. We take the rules one at a time; in each, the cited lines are true under $v$ by $(\ast)$ .

$\mathrm{R}$ . Line $k$ repeats a line $i$ , so $\varphi_k = \varphi_i$ , and $v(\varphi_k) = \mathrm{T}$ .

$\mathrm{\wedge I}$ . Line $k$ is $\varphi \wedge \psi$ , citing lines holding $\varphi$ and $\psi$ . Both are true under $v$ , so $\varphi \wedge \psi$ is true by (V3).

$\mathrm{\wedge E}$ . Line $k$ is $\varphi$ , citing a line holding $\varphi \wedge \psi$ . That line is true under $v$ , so by (V3) both conjuncts are true, and in particular $\varphi$ . The second form, which writes $\psi$ , is the same with the other conjunct, and we skip it.

$\mathrm{{\to}E}$ . Line $k$ is $\psi$ , citing lines holding $\varphi \to \psi$ and $\varphi$ . Both are true under $v$ . By (V5), an implication with a true hypothesis and a false conclusion is false; since $\varphi \to \psi$ is true and $\varphi$ is true, $\psi$ is true.

$\mathrm{\vee I}$ . Line $k$ is $\varphi \vee \psi$ or $\psi \vee \varphi$ , citing a line holding $\varphi$ . That line is true under $v$ , so both disjunctions are true by (V4).

$\mathrm{\neg E}$ . Line $k$ is $\bot$ , citing lines holding $\varphi$ and $\neg\varphi$ . By $(\ast)$ both would be true under $v$ , and by (V2) $\neg\varphi$ is false whenever $\varphi$ is true. So no valuation makes every formula of $\Gamma_k$ true, and there is no $v$ to consider: $\Gamma_k \models \bot$ holds because there is no row to check.

$\mathrm{\bot E}$ . Line $k$ is any formula $\varphi$ , citing a line holding $\bot$ . By $(\ast)$ , $v(\bot) = \mathrm{T}$ , which (V1) forbids. So again no valuation makes every formula of $\Gamma_k$ true, and $\Gamma_k \models \varphi$ holds.

$\mathrm{{\leftrightarrow}E}$ . Line $k$ is $\psi$ , citing lines holding $\varphi \leftrightarrow \psi$ and $\varphi$ . Both are true under $v$ ; by (V6), $v(\psi) = v(\varphi) = \mathrm{T}$ . The second form, which writes $\varphi$ from $\varphi \leftrightarrow \psi$ and $\psi$ , is the same with the sides exchanged, and we skip it.

For the box rules we record what the hypothesis gives for a cited box. If line $k$ cites, by a box rule, the box from line $a$ to line $b$ , then $\Gamma_b = \Gamma_k, \varphi_a$ by Lemma 4.7.1 (b), and the induction hypothesis for line $b$ says $\Gamma_k, \varphi_a \models \varphi_b : \quad \text{every valuation making } \Gamma_k \text{ and } \varphi_a \text{ true makes } \varphi_b \text{ true.} \tag{$\ast\ast$}$

Claim. If line $k$ is justified by a box rule, then $v(\varphi_k) = \mathrm{T}$ .

Proof of Claim. Recall that $v$ makes every formula of $\Gamma_k$ true.

$\mathrm{{\to}I}$ . Line $k$ is $\varphi \to \psi$ , citing a box that opens with $\varphi$ and ends with $\psi$ . By $(\ast\ast)$ , every valuation making $\Gamma_k$ and $\varphi$ true makes $\psi$ true. If $v(\varphi) = \mathrm{F}$ , then $v(\varphi \to \psi) = \mathrm{T}$ by (V5). If $v(\varphi) = \mathrm{T}$ , then $v$ makes $\Gamma_k$ and $\varphi$ true, so $v(\psi) = \mathrm{T}$ , and again $v(\varphi \to \psi) = \mathrm{T}$ by (V5).

$\mathrm{\neg I}$ . Line $k$ is $\neg\varphi$ , citing a box that opens with $\varphi$ and ends with $\bot$ . By $(\ast\ast)$ , every valuation making $\Gamma_k$ and $\varphi$ true makes $\bot$ true; since (V1) makes $\bot$ false under every valuation, no valuation makes $\Gamma_k$ and $\varphi$ true. As $v$ makes $\Gamma_k$ true, it must make $\varphi$ false, and then $v(\neg\varphi) = \mathrm{T}$ by (V2).

$\mathrm{RAA}$ . Line $k$ is $\varphi$ , citing a box that opens with $\neg\varphi$ and ends with $\bot$ . By $(\ast\ast)$ and (V1), as in the previous case, no valuation makes $\Gamma_k$ and $\neg\varphi$ true. Suppose $v(\varphi) = \mathrm{F}$ . Then $v(\neg\varphi) = \mathrm{T}$ by (V2), so $v$ makes $\Gamma_k$ and $\neg\varphi$ true, which is impossible. Hence $v(\varphi) = \mathrm{T}$ .

$\mathrm{\vee E}$ . Line $k$ is $\chi$ , citing a line $i$ holding $\varphi \vee \psi$ , a box that opens with $\varphi$ and ends with $\chi$ , and a box that opens with $\psi$ and ends with $\chi$ . By $(\ast)$ , $v(\varphi \vee \psi) = \mathrm{T}$ , so by (V4), $v(\varphi) = \mathrm{T}$ or $v(\psi) = \mathrm{T}$ . By $(\ast\ast)$ for the first box, every valuation making $\Gamma_k$ and $\varphi$ true makes $\chi$ true; for the second, every valuation making $\Gamma_k$ and $\psi$ true makes $\chi$ true. If $v(\varphi) = \mathrm{T}$ , then $v$ makes $\Gamma_k$ and $\varphi$ true, so $v(\chi) = \mathrm{T}$ . If $v(\psi) = \mathrm{T}$ , the second box gives $v(\chi) = \mathrm{T}$ in the same way.

$\mathrm{{\leftrightarrow}I}$ . Line $k$ is $\varphi \leftrightarrow \psi$ , citing a box that opens with $\varphi$ and ends with $\psi$ , and one that opens with $\psi$ and ends with $\varphi$ . By $(\ast\ast)$ , every valuation making $\Gamma_k$ and $\varphi$ true makes $\psi$ true, and every valuation making $\Gamma_k$ and $\psi$ true makes $\varphi$ true. If $v(\varphi) = \mathrm{T}$ , the first box gives $v(\psi) = \mathrm{T}$ . If $v(\varphi) = \mathrm{F}$ , then $v(\psi) = \mathrm{F}$ too, since $v(\psi) = \mathrm{T}$ would give $v(\varphi) = \mathrm{T}$ by the second box. In both cases $v(\varphi) = v(\psi)$ , so $v(\varphi \leftrightarrow \psi) = \mathrm{T}$ by (V6).

The three claims cover every way line $k$ can be justified, so $S(k)$ holds. By Theorem 4.2.2, $S(k)$ holds for every $k \in \mathbb{N}$ : every line $k$ of the derivation satisfies $\Gamma_k \models \varphi_k$ .

Step 4 (the last line). The last line $n$ of a derivation lies in no box (Definition 1.4.2), so its context $\Gamma_n$ consists of the premises alone, and $\varphi_n = \psi$ . By the induction of Steps 2 and 3, $\Gamma_n \models \psi$ . Every premise belongs to $\Gamma$ (Definition 1.2.3), so a valuation making every formula of $\Gamma$ true makes every formula of $\Gamma_n$ true, and hence makes $\psi$ true. This proves $\Gamma \models \psi$ .

The proof is long, but each case is one step of the truth-table reasoning of Section 4.4, placed in the right context. Every primitive rule has passed. So has every derived rule, since each abbreviates primitive ones. The rules never lead from truth to falsehood, not merely line by line but for every derivation that can ever be written.

Second readingWhy induction on the position of a line

Why strong induction and the position $k$ of a line? A rule may cite any available line, however far back: line 7 of the derivation of Proposition 2.3.2 cites the box that begins at line 2. So the hypothesis is needed for all earlier lines at once. A different route would induct on the length of the whole derivation, removing its last line. But the lines above the last line need not form a derivation, since a box may still be open there (in the derivation of Proposition 2.3.2, lines 1–6 end inside the box $2\text{–}6$ ), and that route has to cut boxes open. Carrying the context of every line avoids the surgery.

Example (Running the claim on a case split)

Here is a derivation of $p \vee q \vdash q \vee p$ . List the context of each line, and check $\Gamma_k \models \varphi_k$ for each $k$ , naming the case of the proof that handles it.

p \vee q

p

asm, for

\mathrm{{\vee}E}

q \vee p

\mathrm{{\vee}I}

q

asm, for

\mathrm{{\vee}E}

q \vee p

\mathrm{{\vee}I}

q \vee p

\mathrm{{\vee}E}

1, 2–3, 4–5

Solution. The boxes are $2\text{–}3$ and $4\text{–}5$ .

Line	Context $\Gamma_k$	Case	Why $\Gamma_k \models \varphi_k$
1	$p \vee q$	premise	$\varphi_1$ is in its context
2	$p \vee q, \ p$	assumption	$\varphi_2$ is in its context
3	$p \vee q, \ p$	$\mathrm{\vee I}$ citing 2	$\Gamma_2 \subseteq \Gamma_3$ ; a row making $p$ true makes $q \vee p$ true
4	$p \vee q, \ q$	assumption	$\varphi_4$ is in its context
5	$p \vee q, \ q$	$\mathrm{\vee I}$ citing 4	as for line 3, with $q$
6	$p \vee q$	$\mathrm{\vee E}$ citing 1 and both boxes	see below

For line 6: by Lemma 4.7.1 (b), $\Gamma_3 = \Gamma_6, p$ and $\Gamma_5 = \Gamma_6, q$ , and the claim for lines 3 and 5 says that rows making $p \vee q$ and $p$ true, and rows making $p \vee q$ and $q$ true, make $q \vee p$ true. A row making $\Gamma_6$ true makes $p \vee q$ true, so it makes $p$ or $q$ true, and one of the two boxes applies. Line 6 is the last line, and its context is the premise: so $p \vee q \models q \vee p$ , as soundness promises.

4.7.5. Every rule, checked against the tables

Rule	Introduced	Case	Clause	Wrong version; its derivation; refuting row
$\mathrm{R}$	1.4 (clause (D3))	Claim 2	none: the line is repeated
$\mathrm{\wedge I}$ , $\mathrm{\wedge E}$	1.2	Claim 2	(V3)
$\mathrm{{\to}E}$	1.3	Claim 2	(V5)
$\mathrm{{\to}I}$	1.4	Claim 3	(V5)	“a box from $\varphi$ to $\psi$ gives $\psi \to \varphi$ ”; the box $p \wedge q$ , $p$ would give $\vdash p \to (p \wedge q)$ ; row $p = \mathrm{T}$ , $q = \mathrm{F}$
$\mathrm{\vee I}$	1.5	Claim 2	(V4)
$\mathrm{\vee E}$	1.6	Claim 3	(V4)	“the two boxes may end in different lines; write the first box’s”; from $p \vee q$ , the boxes $p$ and $q$ would give $p \vee q \vdash p$ ; row $p = \mathrm{F}$ , $q = \mathrm{T}$
$\mathrm{\neg E}$ , $\mathrm{\bot E}$	2.1	Claim 2	(V2); (V1)
$\mathrm{\neg I}$	2.2	Claim 3	(V1), (V2)	“a box from $\varphi$ to any line gives $\neg\varphi$ ”; the one-line box $p$ would give $\vdash \neg p$ ; row $p = \mathrm{T}$
$\mathrm{{\leftrightarrow}I}$ , $\mathrm{{\leftrightarrow}E}$	2.4	Claim 3; Claim 2	(V6)
$\mathrm{RAA}$	2.5	Claim 3	(V1), (V2)	“a box from $\varphi$ to $\bot$ gives $\varphi$ ”; from $\neg p$ , the box $p$ , $\bot$ (by $\mathrm{\neg E}$ ) would give $\neg p \vdash p$ ; row $p = \mathrm{F}$

The thirteen primitive rules, with the case and clause each uses. Each wrong version changes one condition, and its case fails there: the row makes the premises true and the line false.

Second readingThe four wrong derivations, written out

Here are the four derivations the wrong versions would license, written as patterns with Chapter 2’s letters; read $P$ and $Q$ as the atoms $p$ and $q$ for the rows of the table. Each is correct except at its last line, which only the wrong version allows. Wrong $\mathrm{{\to}I}$ reverses the implication its box proves; wrong $\mathrm{\vee E}$ closes on a line that only the first box reaches; wrong $\mathrm{\neg I}$ closes a box that never reached $\bot$ ; wrong $\mathrm{RAA}$ opens its box with $\varphi$ instead of $\neg\varphi$ .

P \wedge Q

asm, for

\mathrm{{{\to}}I}

P

\mathrm{{\wedge}E}

P \to (P \wedge Q)

\mathrm{{{\to}}I}

1–2

P \vee Q

P

asm, for

\mathrm{{\vee}E}

Q

asm, for

\mathrm{{\vee}E}

P

\mathrm{{\vee}E}

1, 2–2, 3–3

P

asm, for

\mathrm{{\neg}I}

\neg P

\mathrm{{\neg}I}

1–1

\neg P

P

asm, for

\mathrm{RAA}

\bot

\mathrm{{\neg}E}

2, 1

P

\mathrm{RAA}

2–3

4.7.6. Refuting with one row

Soundness is most often used backwards. If the conclusion can be false while the premises are true, no derivation can exist.

Corollary 4.7.3 (Refuting Row)

Let $\Gamma$ be a list of formulas and $\psi$ a formula. If some valuation makes every formula of $\Gamma$ true and $\psi$ false, then $\Gamma \nvdash \psi$ .

Proof. Let $v$ make every formula of $\Gamma$ true and $\psi$ false. Then $\Gamma \models \psi$ fails (Definition 4.5.3). If $\Gamma \vdash \psi$ held, Theorem 4.7.2 would give $\Gamma \models \psi$ . So $\Gamma \vdash \psi$ does not hold.

Here $\Gamma \nvdash \psi$ means that there is no derivation of $\psi$ from premises in $\Gamma$ : not with the primitive rules, not with any derived rule, not in a thousand lines. One row has settled a question about infinitely many derivations.

Quick check. Does the row $p = q = \mathrm{T}$ refute $p \to q \vdash q$ ? Does the row $p = q = \mathrm{F}$ ?

Solution. The first does not, since its conclusion $q$ is true. The second does: $p \to q$ is T and $q$ is F. So $p \to q \nvdash q$ , by Corollary 4.7.3.

Chapter 3’s question. Section 3.1 searched for a derivation of $P \to Q \vdash Q \to P$ and stalled. The row $p = \mathrm{F}$ , $q = \mathrm{T}$ makes $p \to q$ true (false hypothesis) and $q \to p$ false (true hypothesis, false conclusion). By Corollary 4.7.3, $p \to q \nvdash q \to p .$ The letters of Chapter 3 stood for arbitrary statements, and the search asked for a derivation of the pattern: one derivation, written with $P$ and $Q$ , that works whatever they are. Such a derivation, with $P$ and $Q$ read as the atoms $p$ and $q$ , would derive $p \to q \vdash q \to p$ , which we have just ruled out. So the pattern has no derivation, and the search was right to fail. (Particular instances can be derivable: with $P$ and $Q$ the same statement, $P \to P \vdash P \to P$ takes one line. A refuting row for atoms speaks about the pattern, as the warning after Lemma 4.5.3 said.)

What soundness certifies. Soundness turns every break this book has made into a proof that no derivation exists. Section 1.1 called a form bad when some choice of statements makes its counterexample set true (Definition 1.1.3). For a propositional form, a row making the counterexample set true is such a choice, and by Corollary 4.7.3 no derivation of the form exists, with any rule of Chapters 1 and 2. Chapter 1 promised exactly this, in Section 1.3, for affirming the consequent: the row $p = \mathrm{F}$ , $q = \mathrm{T}$ of Example (Affirming the consequent is not valid) makes $p \to q$ and $q$ true and $p$ false, so $p \to q, \ q \nvdash p .$ So the repair of Argument B that Section 1.4 considered is not merely unjustified: it is impossible. The same holds for every break in the derive-or-break items from Section 1.5 on, for each claim of Section 3.2 that the search of Section 4.6 refuted, the four breaks of Exercise (B3: Derive or break, used later) among them, and for every refuting row of Sections 4.5 and 4.6. A break by statements about a number certifies the same: the truth values of those statements form a row, and since the connectives are truth-functional (Section 4.4), that row makes the counterexample set true.

Warning. A refuting row must make every premise true. For $p \to q, \ p \vdash q$ , the row $p = \mathrm{F}$ , $q = \mathrm{F}$ makes the conclusion false, but it also makes the premise $p$ false, so it refutes nothing; and the sequent is derivable, by one line of $\mathrm{{\to}E}$ . A row in which some premise fails is simply not one of the rows Definition 4.5.3 looks at.

Warning. Soundness goes one way. It says that derivable sequents are valid; it does not say that a formula true in the row you happened to check is derivable. The atom $p$ is true under the all-T valuation, but $\nvdash p$ : the all-F valuation makes it false, so Corollary 4.7.3 (with $\Gamma$ empty) applies. Whether every valid sequent is derivable is a separate question, answered in Section 4.8.

Quick check. Give a row showing $p \to r \nvdash (p \vee q) \to r$ .

Solution. Take $p = \mathrm{F}$ , $q = \mathrm{T}$ , $r = \mathrm{F}$ . The premise $p \to r$ is true, since $p$ is false. The conclusion has hypothesis $p \vee q$ , which is true, and conclusion $r$ , which is false, so it is false. By Corollary 4.7.3, no derivation exists. (The rows with $p$ true fail: they make the premise force $r$ true, or make the premise false.)

Satisfiable lists are consistent. Section 4.5 kept two words apart, and soundness joins them in one direction. A satisfiable list $\Delta$ is consistent (Definition 3.2.1): if $\Delta \vdash \bot$ , soundness would give $\Delta \models \bot$ , but a row making $\Delta$ true makes $\bot$ false. With Proposition 3.2.2 (b) this is Corollary 4.7.3 once more: a row making the counterexample set $\Gamma, \neg\psi$ true shows it consistent, and so $\Gamma \nvdash \psi$ , as Exercise B4 of Section 3.2 anticipated. Section 4.8 proves the converse.

4.7.7. Test the subgoal

Section 3.1’s search works on subgoals: a goal, and the lines available for it. Soundness gives it a test. Before chasing a subgoal, look for a row making the available lines true and the subgoal false. If there is one, no line standing at this point can hold the subgoal: its context, the premises and the open assumptions, is among the available lines, so the row makes that context true and the subgoal false, while the proof of Theorem 4.7.2 showed that every line $k$ satisfies $\Gamma_k \models \varphi_k$ . This is the move test the subgoal. Section 3.1 met it without the name (“Choosing a side of $\vee$ can leave a goal that does not follow”): from $p \vee q$ , the goal $q \vee p$ tempts $\mathrm{\vee I}$ from $q$ , and the row $p = \mathrm{T}$ , $q = \mathrm{F}$ makes $p \vee q$ true and $q$ false, so the search must split $p \vee q$ first.

Chapter 2 met a harder case. Section 2.5 did not aim at $\mathrm{\vee I}$ for the De Morgan direction $\neg(P \wedge Q) \vdash \neg P \vee \neg Q$ , because the step from the premise to either disjunct can be broken. Now such a break is a proof: the row $p = \mathrm{T}$ , $q = \mathrm{F}$ makes $\neg(p \wedge q)$ true and $\neg p$ false, so $\neg(p \wedge q) \nvdash \neg p$ , and the row $p = \mathrm{F}$ , $q = \mathrm{T}$ gives $\neg(p \wedge q) \nvdash \neg q$ . Both subgoals fail the test, so a derivation of Proposition 2.5.5 (d) cannot end with $\mathrm{\vee I}$ , which is why Section 2.5 reached for $\mathrm{RAA}$ . The test only refutes. A subgoal that passes it may still be hard to reach; whether it can be reached at all is Section 4.8’s question.

Quick check. A search for $p \to q, \ \neg q \vdash \neg p$ opens a box $p$ for $\mathrm{\neg I}$ , with the goal $\bot$ . Does the subgoal $q$ pass the test?

Solution. Yes, trivially. The available lines $p \to q$ , $\neg q$ , $p$ are made true by no row at all ( $p$ and $p \to q$ force $q$ ), so no row refutes any subgoal there; and indeed $q$ follows by $\mathrm{{\to}E}$ , then $\bot$ by $\mathrm{\neg E}$ . An unsatisfiable context lets every subgoal pass.

Remark (Looking ahead). Chapter 8 says what reductio asserts that the other rules do not, and who objected to it.

4.7.8. Exercises

A. Check your understanding

Exercise (A1)

These parts are about the proof of Theorem 4.7.2. Part (c) uses the derivation of Proposition 2.1.2, written with atoms:

\neg p

p

asm, for

\mathrm{{{\to}}I}

\bot

\mathrm{{\neg}E}

2, 1

q

\mathrm{{\bot}E}

p \to q

\mathrm{{{\to}}I}

2–4

(a) Why does the proof use strong induction on $k$ , rather than ordinary induction from line $k$ to line $k + 1$ ?
(b) In the $\mathrm{\vee E}$ case, the induction hypothesis is applied to the last lines $b$ and $d$ of the two boxes. What does it say about each, and which part of Lemma 4.7.1 identifies the contexts?
(c) List the context of each of the five lines of the derivation above, and check $\Gamma_k \models \varphi_k$ for each.
(d) Suppose a rule “from $\varphi \to \psi$ and $\psi$ , infer $\varphi$ ” were added to the primitive rules. Which part of the proof would fail? Give a valuation showing it.
(e) Where does Step 4 use that the last line of a derivation lies in no box?

Solution. (a) A rule may cite any available line, however far back, and the last line of a box that closed long ago. The hypothesis must therefore be available for every earlier line, not just for line $k - 1$ . For example, line 7 of the derivation of Proposition 2.3.2 uses the claim for line 6, and line 6 uses it for line 5; but line 5 uses it for line 2, three lines back.

(b) It says $\Gamma_b \models \chi$ and $\Gamma_d \models \chi$ . By Lemma 4.7.1 (b), $\Gamma_b = \Gamma_k, \varphi$ and $\Gamma_d = \Gamma_k, \psi$ : every row making $\Gamma_k$ and $\varphi$ true makes $\chi$ true, and every row making $\Gamma_k$ and $\psi$ true makes $\chi$ true. It is not $\Gamma_k \models \chi$ , which is what we are trying to prove.

(c) The box is $2\text{–}4$ .

Line	Context	Check
1	$\neg p$	premise, in its context
2	$\neg p, \ p$	assumption, in its context
3	$\neg p, \ p$	no row makes $\neg p$ and $p$ true, so it entails $\bot$
4	$\neg p, \ p$	the same unsatisfiable context entails $q$
5	$\neg p$	a row making $\neg p$ true makes $p$ false, so $p \to q$ true

Line 3 is the $\mathrm{\neg E}$ case, line 4 the $\mathrm{\bot E}$ case, and line 5 the $\mathrm{{\to}I}$ case, with $\Gamma_4 = \Gamma_5, p$ by Lemma 4.7.1 (b).

(d) Claim 2, the one-step rules: it would need a new case, and the case is false. From $v(\varphi \to \psi) = \mathrm{T}$ and $v(\psi) = \mathrm{T}$ nothing follows about $v(\varphi)$ . The valuation with $v(p) = \mathrm{F}$ , $v(q) = \mathrm{T}$ makes $p \to q$ and $q$ true and $p$ false; with the new rule, the three-line derivation of $p$ from $p \to q$ and $q$ would have a last line whose context does not entail it.

(e) It concludes that the context of the last line is just the premises. Without that, the last line could depend on an undischarged assumption, and $\Gamma_n \models \psi$ would say nothing about the rows making the premises true.

Exercise (A2: Drill)

The parts run from reading off a refuting row, through contexts, to testing a subgoal and deciding a claim.

(a) Give a refuting row for $p \vee q \vdash p$ .
(b) Give one for $p \to q, \ \neg p \vdash \neg q$ .
(c) Does $p = \mathrm{T}$ , $q = \mathrm{F}$ refute $p \wedge q \vdash q$ ?
(d) Is there a refuting row for $p, \ p \to q \vdash q$ ?
(e) Refute $\vdash p \vee q$ .
(f) Refute $p \to (q \vee r) \vdash p \to q$ .
(g) Line 5 of a derivation lies in the boxes opened at lines 2 and 4, and line 1 is the only premise. What is $\Gamma_5$ ?
(h) Line $k$ is justified by $\mathrm{\neg I}$ citing the box 3–6. What is $\Gamma_6$ , in terms of $\Gamma_k$ ?
(i) A search for $p \vee q \vdash q \vee p$ considers ending with $\mathrm{\vee I}$ from $q$ . Test the subgoal $q$ .
(j) The list $p \to q, \ q \to \neg p$ is satisfiable: give a row, and say what follows about $\vdash$ .
(k) Which clause of Definition 4.4.2 does the $\mathrm{\vee E}$ case of the proof of Theorem 4.7.2 use?
(l) Derive or refute: $(p \wedge q) \to r \vdash (p \to r) \wedge (q \to r)$ .

Solution.

(a) $p = \mathrm{F}$ , $q = \mathrm{T}$ .
(b) $p = \mathrm{F}$ , $q = \mathrm{T}$ .
(c) No: it makes the premise false.
(d) No. The only row making both premises true has $q$ true. (The sequent is derivable, by one line of $\mathrm{{\to}E}$ .)
(e) $p = q = \mathrm{F}$ . With no premises, every row qualifies.
(f) $p = \mathrm{T}$ , $q = \mathrm{F}$ , $r = \mathrm{T}$ .
(g) $\varphi_1, \varphi_2, \varphi_4$ .
(h) $\Gamma_k, \varphi_3$ , by Lemma 4.7.1 (b).
(i) The row $p = \mathrm{T}$ , $q = \mathrm{F}$ makes $p \vee q$ true and $q$ false: $p \vee q \nvdash q$ (Corollary 4.7.3), so the subgoal is dead.
(j) $p = \mathrm{F}$ , $q = \mathrm{T}$ (or both F). So the list is consistent: $p \to q, \ q \to \neg p \nvdash \bot$ . (It is the list of Exercise (B4: Derive ⊥, or make every member true, used later) (a) without its third member $p$ ; with $p$ , Section 3.2 derived $\bot$ .)
(k) (V4).
(l) Refute: $p = \mathrm{T}$ , $q = \mathrm{F}$ , $r = \mathrm{F}$ makes the premise true (false hypothesis) and $p \to r$ false, so the conclusion false; by Corollary 4.7.3 no derivation exists.

B. Practice

Exercise (B1: Derivable or not)

Determine which of the following are derivable. Justify your answer.

(a) $(p \wedge q) \to r \vdash p \to r$ .
(b) $\neg(p \wedge q) \vdash \neg p$ .
(c) $p \leftrightarrow q, \ q \vee r \vdash p$ .
(d) $p \to (q \vee r) \vdash (p \to q) \vee (p \to r)$ .

Solution. (a) Not derivable. The row $p = \mathrm{T}$ , $q = \mathrm{F}$ , $r = \mathrm{F}$ makes the premise true (its hypothesis $p \wedge q$ is false) and the conclusion $p \to r$ false. By Corollary 4.7.3 there is no derivation.

(b) Not derivable. The row $p = \mathrm{T}$ , $q = \mathrm{F}$ makes $p \wedge q$ false, so $\neg(p \wedge q)$ true, and $\neg p$ false. By Corollary 4.7.3 there is no derivation.

(c) Not derivable. The row $p = \mathrm{F}$ , $q = \mathrm{F}$ , $r = \mathrm{T}$ makes $p \leftrightarrow q$ true (both sides false) and $q \vee r$ true, and $p$ false.

(d) Derivable: Example (Choosing a side too early) in Section 3.1 derives it, with $\mathrm{LEM}$ on $q$ . So no row can refute it: by Theorem 4.7.2 it is valid. A search for a refuting row confirms this. The conclusion is false only if both $p \to q$ and $p \to r$ are false, that is, $p = \mathrm{T}$ and $q = r = \mathrm{F}$ ; but then $q \vee r$ is false and the premise is false.

The trap is (d). Its conclusion looks stronger than the premise, since it seems to decide in advance which disjunct follows from $p$ ; but a derivation exists, and trying to refute it by a row is bound to fail.

Exercise (B2: Ordering the

\vee

E case)

Here are nine lines. Seven of them, in the right order, form the $\mathrm{\vee E}$ case of the proof of Theorem 4.7.2. Line $k$ is $\chi$ , by $\mathrm{\vee E}$ citing line $i$ (holding $\varphi \vee \psi$ ), the box from line $a$ to line $b$ (opening with $\varphi$ , ending with $\chi$ ), and the box from line $c$ to line $d$ (opening with $\psi$ , ending with $\chi$ ). Give an admissible order, and say why each of the other two lines cannot be used.

(i) By the induction hypothesis for lines $b$ and $d$ , which come before line $k$ , $\Gamma_b \models \chi$ and $\Gamma_d \models \chi$ .
(ii) Hence $v(\chi) = \mathrm{T}$ in either case; since $v$ was arbitrary, $\Gamma_k \models \chi$ .
(iii) Let $v$ be a valuation making every formula of $\Gamma_k$ true.
(iv) If $v(\psi) = \mathrm{T}$ , then $v$ makes every formula of $\Gamma_d$ true, so $v(\chi) = \mathrm{T}$ .
(v) By Lemma 4.7.1 (a), $\Gamma_i \subseteq \Gamma_k$ , so $v$ makes every formula of $\Gamma_i$ true; by the induction hypothesis for line $i$ , $v(\varphi \vee \psi) = \mathrm{T}$ , so $v(\varphi) = \mathrm{T}$ or $v(\psi) = \mathrm{T}$ .
(vi) By the induction hypothesis for line $k$ , $\Gamma_k \models \chi$ .
(vii) By Lemma 4.7.1 (b), $\Gamma_b$ is $\Gamma_k$ with $\varphi$ added, and $\Gamma_d$ is $\Gamma_k$ with $\psi$ added.
(viii) If $v(\varphi) = \mathrm{T}$ , then $v$ makes every formula of $\Gamma_b$ true, so $v(\chi) = \mathrm{T}$ .
(ix) Line $b$ is inside the box, and the box was cited at line $k$ , so the context of line $b$ is $\Gamma_k$ ; the induction hypothesis for line $b$ then gives $\Gamma_k \models \chi$ directly.

Solution. An admissible order: (iii), (v), (vii), (i), (viii), (iv), (ii).

What each line needs: (v) and (viii), (iv) use the valuation fixed in (iii); (viii) and (iv) use (vii) and (i); (ii) uses the case split of (v) and both of (viii) and (iv). So any order is admissible in which (iii) comes before (v), (viii), and (iv); (vii) and (i) come before (viii) and (iv); (v) comes before (ii); and (viii) and (iv) come before (ii). For instance (vii), (i), (iii), (v), (iv), (viii), (ii) is also admissible: (vii) and (i) do not mention $v$ , and the two cases may be taken in either order.

Line (vi) applies the induction hypothesis to line $k$ itself. The hypothesis of Theorem 4.2.2 covers only the lines $j < k$ ; (vi) assumes what is to be proved.

Line (ix) uses the context of the citing line for the box’s last line. It is false: line $b$ lies inside the box, whose assumption $\varphi$ is part of its context, so $\Gamma_b = \Gamma_k, \varphi$ , not $\Gamma_k$ . In the derivation of Example (Running the claim on a case split), line 3 has context $p \vee q, \ p$ , while line 6 has context $p \vee q$ , and $p \vee q \models q \vee p$ could not be read off from line 3 directly.

Exercise (B3: Derive or refute)

For each claim, give a derivation, or a refuting row and the result that makes it a proof of non-derivability.

(a) $p \leftrightarrow q \vdash \neg p \leftrightarrow \neg q$ .
(b) $p \leftrightarrow \neg q \vdash \neg(p \wedge q)$ .
(c) $p \to q, \ q \to r \vdash r \to p$ .
(d) $\neg p \vee q \vdash p \to q$ .
(e) $p \leftrightarrow q, \ \neg q \vdash p$ .
(f) $\neg(p \to q) \vdash q \to p$ .

Solution.

(a) Derive.
1 $p \leftrightarrow q$
2 $\neg p$ asm, for $\mathrm{{{\leftrightarrow}}I}$
3 $q$ asm, for $\mathrm{{\neg}I}$
4 $p$ $\mathrm{{{\leftrightarrow}}E}$ 1, 3
5 $\bot$ $\mathrm{{\neg}E}$ 4, 2
6 $\neg q$ $\mathrm{{\neg}I}$ 3–5
7 $\neg q$ asm, for $\mathrm{{{\leftrightarrow}}I}$
8 $p$ asm, for $\mathrm{{\neg}I}$
9 $q$ $\mathrm{{{\leftrightarrow}}E}$ 1, 8
10 $\bot$ $\mathrm{{\neg}E}$ 9, 7
11 $\neg p$ $\mathrm{{\neg}I}$ 8–10
12 $\neg p \leftrightarrow \neg q$ $\mathrm{{{\leftrightarrow}}I}$ 2–6, 7–11
(b) Derive.
1 $p \leftrightarrow \neg q$
2 $p \wedge q$ asm, for $\mathrm{{\neg}I}$
3 $p$ $\mathrm{{\wedge}E}$ 2
4 $q$ $\mathrm{{\wedge}E}$ 2
5 $\neg q$ $\mathrm{{{\leftrightarrow}}E}$ 1, 3
6 $\bot$ $\mathrm{{\neg}E}$ 4, 5
7 $\neg (p \wedge q)$ $\mathrm{{\neg}I}$ 2–6
(c) Refute. $p = \mathrm{F}$ , $q = \mathrm{F}$ , $r = \mathrm{T}$ : both premises have false hypotheses, and $r \to p$ is $\mathrm{T} \to \mathrm{F}$ . By Corollary 4.7.3, no derivation exists.
(d) Derive.

1 $\neg p \vee q$
2 $p$ asm, for $\mathrm{{{\to}}I}$
3 $\neg p$ asm, for $\mathrm{{\vee}E}$
4 $\bot$ $\mathrm{{\neg}E}$ 2, 3
5 $q$ $\mathrm{{\bot}E}$ 4
6 $q$ asm, for $\mathrm{{\vee}E}$
7 $q$ $\mathrm{{\vee}E}$ 1, 3–5, 6–6
8 $p \to q$ $\mathrm{{{\to}}I}$ 2–7
(e) Refute. $p = q = \mathrm{F}$ : $p \leftrightarrow q$ is T, $\neg q$ is T, and $p$ is F. By Corollary 4.7.3, no derivation exists.
(f) Derive, without $\mathrm{RAA}$ .

\neg (p \to q)

q

asm, for

\mathrm{{{\to}}I}

p

asm, for

\mathrm{{{\to}}I}

q

\mathrm{R}

p \to q

\mathrm{{{\to}}I}

3–4

\bot

\mathrm{{\neg}E}

5, 1

p

\mathrm{{\bot}E}

q \to p

\mathrm{{{\to}}I}

2–7

(c) is the converse of the chain, a way of affirming a conclusion; (e) is a look-alike of $p \leftrightarrow q, \ \neg q \vdash \neg p$ , which (a) gives by $\mathrm{{\leftrightarrow}E}$ ; (f) looks paradoxical and is not: its premise is false in every row but one, and there $q \to p$ is true.

Exercise (B4: Test the subgoal)

A search for $p \to (q \vee r), \ \neg q \vdash p \to r$ has reached this stage:

p \to (q \vee r)

\neg q

p

asm, for

\mathrm{{{\to}}I}

\vdots

r

p \to r

\mathrm{{{\to}}I}

3–9

A student plans to reach $r$ by deriving $q$ first.

(a) Test that subgoal.
(b) Name the move that works, then complete it.

Solution.

(a) The available lines are $p \to (q \vee r)$ , $\neg q$ , $p$ , and the subgoal is $q$ . The row $p = \mathrm{T}$ , $q = \mathrm{F}$ , $r = \mathrm{T}$ makes the three lines true and $q$ false. So no line of the box itself, whose context is $p \to (q \vee r), \ \neg q, \ p$ , can hold $q$ : every line satisfies $\Gamma_k \models \varphi_k$ , by the proof of Theorem 4.7.2. The plan is dead. ( $q$ may still stand as the assumption of a case box inside it, whose lines have a larger context; that is how (b) uses it.)
(b) Use the premise by its main connective: $\mathrm{{\to}E}$ gives $q \vee r$ ; split it, closing the case $q$ by the clash with $\neg q$ .

p \to (q \vee r)

\neg q

p

asm, for

\mathrm{{{\to}}I}

q \vee r

\mathrm{{{\to}}E}

1, 3

q

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

5, 2

r

\mathrm{{\bot}E}

r

asm, for

\mathrm{{\vee}E}

r

\mathrm{{\vee}E}

4, 5–7, 8–8

p \to r

\mathrm{{{\to}}I}

3–9

(Proposition 2.3.4 gives line 9 from lines 4 and 2 in one step, as a derived rule; either is correct.)

C. Going deeper

Exercise (C1: A safe rule and an unsafe one)

(a) Add to the primitive rules a one-step rule $\mathsf{X}$ : from a line $\varphi \wedge \psi$ , infer $\varphi \vee \psi$ . Show that Theorem 4.7.2 still holds for derivations that may use $\mathsf{X}$ .
(b) Add instead a one-step rule $\mathsf{Y}$ : from a line $\varphi \vee \psi$ , infer $\varphi \wedge \psi$ . Show that soundness fails: name the case of the proof that breaks, give a derivation using $\mathsf{Y}$ of a sequent with a refuting row, and give the row.

Solution (Hint 1). The proof of Theorem 4.7.2 treats one rule per case. Adding a rule adds one case to Claim 2 and changes nothing else.

Solution (Hint 2). For (b), start a derivation from the premise $p$ , and look for a way to write $p \vee q$ first.

Solution. (a) The proof of Theorem 4.7.2 goes through with one more case in Claim 2. Every other part is unchanged: Step 1 and Step 4 do not look at the rules, Lemma 4.7.1 (a) holds for any cited line, and (b) concerns only box rules, and $\mathsf{X}$ is not one. The case $\mathsf{X}$ . Line $k$ is $\varphi \vee \psi$ , citing a line $i$ holding $\varphi \wedge \psi$ . By $(\ast)$ , $v(\varphi \wedge \psi) = \mathrm{T}$ , so $v(\varphi) = \mathrm{T}$ by (V3), and $v(\varphi \vee \psi) = \mathrm{T}$ by (V4). So every line of a derivation with $\mathsf{X}$ still satisfies $\Gamma_k \models \varphi_k$ , and soundness holds.

(b) The new case of Claim 2 fails: from $v(\varphi \vee \psi) = \mathrm{T}$ , (V4) gives only that one disjunct is true, and (V3) needs both. With $\mathsf{Y}$ , this is a derivation of $p \vdash q$ :

p

p \vee q

\mathrm{{\vee}I}

p \wedge q

Y 2

q

\mathrm{{\wedge}E}

The row $p = \mathrm{T}$ , $q = \mathrm{F}$ makes the premise true and the conclusion false, so $p \not\models q$ , although $p \vdash q$ with $\mathsf{Y}$ . The failure is at line 3: its context is $p$ , and the row makes $p$ and line 2 true but line 3 false.

Marking scheme. (10 points)

2: (a) says that only one case is added, and why the rest of the proof (Steps 1 and 4, Lemma 4.7.1) is unaffected.
3: (a) the case for $\mathsf{X}$ , using the hypothesis for the cited line through Lemma 4.7.1 (a) and the clauses (V3), (V4).
2: (b) names the failing case, with the reason (one true disjunct does not give a true conjunction).
3: (b) a correct derivation with $\mathsf{Y}$ and a refuting row for its sequent.

Fatal errors (0 for the step): a “refuting row” that makes a premise false; in (a), checking $\mathsf{X}$ only on atoms without the context argument.

Exercise (C2: Exit check: soundness)

Close the section first, and write from memory.

Write out, in full, the $\mathrm{{\to}I}$ , $\mathrm{\neg I}$ and $\mathrm{\vee E}$ cases of the proof of Theorem 4.7.2: state the claim being proved for every line, set up the induction, and prove the three cases, naming the reason for each step.

Solution. The claim. Fix a derivation in primitive rules with lines $1, \dots, n$ , and write $\varphi_k$ for the formula on line $k$ and $\Gamma_k$ for its context (the premises and the assumptions of the boxes containing line $k$ ). We prove $\Gamma_k \models \varphi_k$ for every $k$ with $1 \le k \le n$ , by Theorem 4.2.2 applied to “if $1 \le k \le n$ , then $\Gamma_k \models \varphi_k$ ” (for $k = 0$ it holds vacuously): fix $k$ with $1 \le k \le n$ , assume $\Gamma_j \models \varphi_j$ for every line $j < k$ , and let $v$ be a valuation making every formula of $\Gamma_k$ true. Every line and box that line $k$ cites lies before line $k$ , so the hypothesis applies to the cited lines and to the last lines of the cited boxes. We show $v(\varphi_k) = \mathrm{T}$ .

$\mathrm{{\to}I}$ . Line $k$ is $\varphi \to \psi$ , citing the box from line $a$ (the assumption $\varphi$ ) to line $b$ (the formula $\psi$ ). By Lemma 4.7.1 (b), $\Gamma_b = \Gamma_k, \varphi$ . Since $b < k$ , the hypothesis gives $\Gamma_k, \varphi \models \psi$ . If $v(\varphi) = \mathrm{F}$ , then $v(\varphi \to \psi) = \mathrm{T}$ by (V5). If $v(\varphi) = \mathrm{T}$ , then $v$ makes every formula of $\Gamma_k, \varphi$ true, so $v(\psi) = \mathrm{T}$ , and $v(\varphi \to \psi) = \mathrm{T}$ by (V5).

$\mathrm{\neg I}$ . Line $k$ is $\neg\varphi$ , citing the box from line $a$ (the assumption $\varphi$ ) to line $b$ (the formula $\bot$ ). By Lemma 4.7.1 (b) and the hypothesis for line $b$ , $\Gamma_k, \varphi \models \bot$ . Since $v(\bot) = \mathrm{F}$ under every valuation (V1), no valuation makes all of $\Gamma_k, \varphi$ true. As $v$ makes $\Gamma_k$ true, $v(\varphi) = \mathrm{F}$ , so $v(\neg\varphi) = \mathrm{T}$ by (V2).

$\mathrm{\vee E}$ . Line $k$ is $\chi$ , citing line $i$ (holding $\varphi \vee \psi$ ) and the boxes from $a$ to $b$ ( $\varphi$ to $\chi$ ) and from $c$ to $d$ ( $\psi$ to $\chi$ ). Line $i$ is available at line $k$ , so $\Gamma_i \subseteq \Gamma_k$ by Lemma 4.7.1 (a); $v$ makes $\Gamma_i$ true, and the hypothesis for line $i$ gives $v(\varphi \vee \psi) = \mathrm{T}$ , so $v(\varphi) = \mathrm{T}$ or $v(\psi) = \mathrm{T}$ by (V4). By Lemma 4.7.1 (b), $\Gamma_b = \Gamma_k, \varphi$ and $\Gamma_d = \Gamma_k, \psi$ , and the hypothesis for lines $b$ and $d$ gives $\Gamma_k, \varphi \models \chi$ and $\Gamma_k, \psi \models \chi$ . If $v(\varphi) = \mathrm{T}$ , then $v$ makes $\Gamma_k, \varphi$ true, so $v(\chi) = \mathrm{T}$ ; if $v(\psi) = \mathrm{T}$ , likewise by the second box.

Conclusion. With the other cases, the induction gives $\Gamma_k \models \varphi_k$ for every line. The last line lies in no box, so its context is the premises, which all belong to $\Gamma$ ; a valuation making $\Gamma$ true makes the premises true, and so makes the last line $\psi$ true: $\Gamma \models \psi$ .

Marking scheme. (10 points)

2: states the claim $\Gamma_k \models \varphi_k$ for every line, with contexts.
2: uses the course-of-values hypothesis on earlier lines only, and says why the cited lines and boxes are earlier.
2: identifies the context of each box’s last line as $\Gamma_k$ plus the box’s assumption, citing Lemma 4.7.1 (b) (and (a) for the cited line in $\vee$ E).
1 + 1 + 1: the semantic step in each of the three cases (the rows where the assumption is false for $\to$ I; no row satisfies the box’s context for $\neg$ I; the split on which disjunct is true for $\vee$ E).
1: the conclusion for the last line.

A proof that inducts on the length of the derivation instead, and handles open boxes correctly, earns the same points step for step. Fatal errors (0 for the step): applying the hypothesis to line $k$ itself; using $\Gamma_k$ as the context of a box’s last line.

Exercise (C3: A changed table)

Replace (V4) by: $v(\varphi \vee \psi) = \mathrm{T}$ exactly when exactly one of $v(\varphi)$ , $v(\psi)$ is $\mathrm{T}$ . Keep every other clause and every rule.

(a) Which cases of the proof of Theorem 4.7.2 still go through?
(b) For each rule whose case fails, give a derivation and a row that is a counterexample for the new table.
(c) Is $p \vdash p \vee q$ still derivable? Is it valid for the new table? What does this show?

Solution.

(a) Every case except $\mathrm{\vee I}$ . The rules that do not mention $\vee$ use other clauses, which are unchanged. The $\mathrm{\vee E}$ case needs only that a true disjunction has a true side, and that still holds: exactly one side is true.
(b) $\mathrm{\vee I}$ : the derivation 1 $p$ ; 2 $p \vee q$ , $\mathrm{\vee I}$ 1. The row $p = q = \mathrm{T}$ makes $p$ true and, for the new table, $p \vee q$ false.
(c) Derivable: the rules did not change. Not valid for the new table: the row of (b). So soundness is a fact about the rules and the tables together; change a table, and the same rules can lead from truth to falsehood.

Marking scheme. (10 points)

4: (a), with the argument for the $\mathrm{\vee E}$ case.
4: (b), the derivation and the row, checked.
2: (c), both answers and the conclusion.

Fatal errors (0 for the step): in (a), declaring the $\mathrm{\vee E}$ case broken without a row that breaks it.

Exercise (C4: Challenge: ⊥ read as a letter)

Read $\bot$ as an ordinary letter. A letter valuation $w$ gives $\mathrm{T}$ or $\mathrm{F}$ to every atom and to $\bot$ , computes $\wedge$ , $\vee$ , $\to$ , $\leftrightarrow$ by (V3)–(V6), and sets $w(\neg\varphi) = \mathrm{T}$ exactly when $w(\varphi) = \mathrm{F}$ or $w(\bot) = \mathrm{T}$ . Write $\Gamma \models_\ell \psi$ when every letter valuation making every formula of $\Gamma$ true makes $\psi$ true.

(a) Show that every line of a derivation that uses no $\mathrm{\bot E}$ and no $\mathrm{RAA}$ , and cites no derived rule whose own derivation uses them, satisfies $\Gamma_k \models_\ell \varphi_k$ . Give the cases $\mathrm{\neg E}$ and $\mathrm{\neg I}$ , and say why the others are those of Theorem 4.7.2.
(b) Deduce that $\bot \vdash p$ has no derivation without $\mathrm{\bot E}$ and $\mathrm{RAA}$ (and without derived rules derived with them).
(c) Derive $\bot \vdash p$ with $\mathrm{RAA}$ and without $\mathrm{\bot E}$ , and say why (b) must exclude $\mathrm{RAA}$ as well.

Solution.

(a) Step 1 of the proof expands each line citing a derived rule into a pasted derivation of that rule, which by hypothesis uses neither $\mathrm{\bot E}$ nor $\mathrm{RAA}$ ; so the expanded derivation is in the remaining primitive rules (and a derived rule derived from derived rules of this kind expands the same way, one layer at a time). Steps 1, 2 and 4 do not look at the clauses, and the cases of premises, assumptions, $\mathrm{R}$ and the rules for $\wedge$ , $\vee$ , $\to$ , $\leftrightarrow$ use only (V3)–(V6), which are unchanged; they go through word for word with $w$ for $v$ .
$\mathrm{\neg E}$ : $w$ makes $\Gamma_k$ true, so by $(\ast)$ it makes $\varphi$ and $\neg\varphi$ true. Now $w(\neg\varphi) = \mathrm{T}$ with $w(\varphi) = \mathrm{T}$ forces $w(\bot) = \mathrm{T}$ , and line $k$ is $\bot$ .

$\mathrm{\neg I}$ : by $(\ast\ast)$ , every letter valuation making $\Gamma_k$ and $\varphi$ true makes $\bot$ true. If $w(\varphi) = \mathrm{F}$ , then $w(\neg\varphi) = \mathrm{T}$ . If $w(\varphi) = \mathrm{T}$ , then $w$ makes $\Gamma_k$ and $\varphi$ true, so $w(\bot) = \mathrm{T}$ , and again $w(\neg\varphi) = \mathrm{T}$ .
(b) The letter valuation with $w(\bot) = \mathrm{T}$ and $w(p) = \mathrm{F}$ makes the premise true and the conclusion false. So $\bot \models_\ell p$ fails, and by (a) no derivation of $\bot \vdash p$ without $\mathrm{\bot E}$ and $\mathrm{RAA}$ , and without derived rules derived with them, exists. (Many derived rules of Chapter 2 use one of the two, Proposition 2.5.1 (b) (with $\mathrm{RAA}$ ) and Proposition 2.1.1 (with $\mathrm{\bot E}$ ) among them; a derivation that avoids the two only on its face is not covered.)
(c)

\bot

\neg p

asm, for

\mathrm{RAA}

\bot

\mathrm{R}

p

\mathrm{RAA}

2–3

So with $\mathrm{RAA}$ the rule $\mathrm{\bot E}$ is derivable, and (a) must fail for $\mathrm{RAA}$ . It does: with $w(\bot) = \mathrm{T}$ , every negation is true, so the box of lines 2–3 satisfies $(\ast\ast)$ , and yet $w(p) = \mathrm{F}$ .

Marking scheme. (10 points)

2: the carried-over cases named, with the reason (Steps 1, 2, 4 and the clauses (V3)–(V6) unchanged), and Step 1’s restriction to derived rules derived without $\mathrm{\bot E}$ and $\mathrm{RAA}$ .
2: the $\mathrm{\neg E}$ case.
3: the $\mathrm{\neg I}$ case, both values of $w(\varphi)$ .
1: (b), the letter valuation and the conclusion.
2: (c), the derivation and the failing case.

Fatal errors (0 for the step): in (b), using the ordinary valuations, under which $\bot \models p$ holds.

Exercise (C5: Challenge: two three-valued tables)

A Kleene valuation $u_{\mathrm{K}}$ assigns one of the values $0$ , $\frac12$ , $1$ to each atom and is extended by $u_{\mathrm{K}}(\bot) = 0$ , $u_{\mathrm{K}}(\neg\varphi) = 1 - u_{\mathrm{K}}(\varphi)$ , $u_{\mathrm{K}}(\varphi \wedge \psi) = \min\{ u_{\mathrm{K}}(\varphi), u_{\mathrm{K}}(\psi) \}$ , $u_{\mathrm{K}}(\varphi \vee \psi) = \max\{ u_{\mathrm{K}}(\varphi), u_{\mathrm{K}}(\psi) \}$ , $u_{\mathrm{K}}(\varphi \to \psi) = \max\{ 1 - u_{\mathrm{K}}(\varphi), u_{\mathrm{K}}(\psi) \}$ . (This extension differs from the three-valued valuation of the optional excursion below, whose $\neg$ gives $\neg\varphi$ the value $0$ at $\frac12$ .) For a set $D$ of designated values, say that $\Gamma$ $D$ -entails $\psi$ if every Kleene valuation $u_{\mathrm{K}}$ giving every formula of $\Gamma$ a value in $D$ gives $\psi$ a value in $D$ .

(a) For $D = \{ 1 \}$ , show that the case $\mathrm{{\to}I}$ fails: give a box that is correct for $D$ -entailment and a $u_{\mathrm{K}}$ at which the line that $\mathrm{{\to}I}$ writes is undesignated.
(b) For $D = \{ \frac12, 1 \}$ , show that the case $\mathrm{{\to}E}$ fails.
(c) Is $p \vee \neg p$ designated under every $u_{\mathrm{K}}$ in (a)? In (b)?

Solution.

(a) The one-line box $p$ : $p$ $D$ -entails $p$ . $\mathrm{{\to}I}$ writes $p \to p$ , and at $u_{\mathrm{K}}(p) = \frac12$ , $u_{\mathrm{K}}(p \to p) = \max\{ \frac12, \frac12 \} = \frac12 \notin D$ .
(b) The premises $p \to q$ , $p$ and the conclusion $q$ , at $u_{\mathrm{K}}(p) = \frac12$ , $u_{\mathrm{K}}(q) = 0$ : $u_{\mathrm{K}}(p \to q) = \max\{ \frac12, 0 \} = \frac12 \in D$ and $u_{\mathrm{K}}(p) = \frac12 \in D$ , but $u_{\mathrm{K}}(q) = 0 \notin D$ .
(c) In (a), no: $u_{\mathrm{K}}(p \vee \neg p) = \max\{ \frac12, \frac12 \} = \frac12$ at $u_{\mathrm{K}}(p) = \frac12$ . In (b), yes: $\max\{ x, 1 - x \} \ge \frac12$ for each of the three values $x$ .

So the first choice of $D$ loses excluded middle and the box rule for $\to$ ; the second keeps excluded middle and loses modus ponens.

Marking scheme. (10 points)

4: (a), the box, the valuation and the computation.
3: (b), the valuation and the three values.
3: (c), both parts, with the computation.

Fatal errors (0 for the step): a “failure” in (a) or (b) at a valuation that does not designate every premise.

4.7.9. Optional excursion: reductio says something new

Optional: nothing later depends on this excursion. It answers a question Chapter 2 raised.

A three-valued valuation $u$ assigns to each atom one of the values $0$ , $\frac12$ , $1$ , ordered $0 < \frac12 < 1$ . Think of $1$ as “true”, $0$ as “false”, and $\frac12$ as “not yet settled”.

$\begin{array}{c|ccc} u(\varphi \to \psi) & u(\psi) = 0 & u(\psi) = \tfrac12 & u(\psi) = 1 \\ \hline u(\varphi) = 0 & 1 & 1 & 1 \\ u(\varphi) = \tfrac12 & 0 & 1 & 1 \\ u(\varphi) = 1 & 0 & \tfrac12 & 1 \end{array} \qquad \begin{array}{c|c} u(\varphi) & u(\neg\varphi) \\ \hline 0 & 1 \\ \tfrac12 & 0 \\ 1 & 0 \end{array}$ An implication gets $1$ when its conclusion is at least as true as its hypothesis, and otherwise the value of its conclusion; a negation is $1$ only on $0$ .

Chapter 2 introduced $\mathrm{RAA}$ in Section 2.5 because the rules before it stalled on $\neg\neg P \vdash P$ , and said that Chapter 4 would prove that no derivation of $P$ from $\neg\neg P$ avoids $\mathrm{RAA}$ . Truth tables cannot do it. The row method only proves non-derivability from all the rules, and with $\mathrm{RAA}$ the sequent is derivable, so no two-valued row refutes it. The trick is to run the proof of Theorem 4.7.2 with a different notion of truth, one with three values, under which every rule except $\mathrm{RAA}$ still passes.

A three-valued valuation is extended to all formulas by recursion (Theorem 4.3.4): $\begin{aligned} u(\bot) &= 0, \qquad u(\neg\varphi) = u(\varphi \to \bot), \\ u(\varphi \wedge \psi) &= \min\{ u(\varphi), u(\psi) \}, \qquad u(\varphi \vee \psi) = \max\{ u(\varphi), u(\psi) \}, \\ u(\varphi \to \psi) &= \begin{cases} 1 & \text{if } u(\varphi) \le u(\psi), \\ u(\psi) & \text{otherwise,} \end{cases} \\ u(\varphi \leftrightarrow \psi) &= \min\{ u(\varphi \to \psi), u(\psi \to \varphi) \} . \end{aligned}$ So $u(\neg\varphi) = 1$ if $u(\varphi) = 0$ , and $u(\neg\varphi) = 0$ otherwise. On the values $0$ and $1$ alone these are exactly the tables of Definition 4.4.2, with $1$ for $\mathrm{T}$ and $0$ for $\mathrm{F}$ . For a list $\Gamma$ , let $u(\Gamma)$ be the least of the values $u(\gamma)$ for $\gamma$ in $\Gamma$ , and $u(\Gamma) = 1$ if $\Gamma$ is empty. Write $\Gamma \models_3 \psi$ if $u(\Gamma) \le u(\psi)$ for every three-valued valuation $u$ : the conclusion is at least as true as the weakest premise.

Theorem 4.7.4 (Reductio Is Not Derivable from the Other Rules) Optional: nothing later depends on this.

Neither $\neg\neg p \vdash p$ nor $\vdash p \vee \neg p$ has a derivation that uses only the primitive rules other than $\mathrm{RAA}$ (and derived rules derived from those).

Idea. Repeat the proof of Theorem 4.7.2 with $\models_3$ in place of $\models$ : every line of a derivation without $\mathrm{RAA}$ satisfies $\Gamma_k \models_3 \varphi_k$ . Then show that both sequents fail for $\models_3$ , at $u(p) = \frac12$ . The one case that breaks is $\mathrm{RAA}$ , and that is the point.

Proof. As in Step 1 of the proof of Theorem 4.7.2, a derived rule derived without $\mathrm{RAA}$ abbreviates a pasted derivation in the primitive rules other than $\mathrm{RAA}$ , so it is enough to consider those. Fix a derivation that uses only the primitive rules other than $\mathrm{RAA}$ , with lines $1, \dots, n$ , formulas $\varphi_k$ and contexts $\Gamma_k$ . We show $\Gamma_k \models_3 \varphi_k$ for every $k$ with $1 \le k \le n$ , by Theorem 4.2.2 exactly as in Step 2 of the proof of Theorem 4.7.2, the cases $k = 0$ and $k > n$ being vacuous. Fix $k$ , assume the claim for all earlier lines, and fix a three-valued valuation $u$ ; write $m = u(\Gamma_k)$ . We must show $m \le u(\varphi_k)$ . Two facts do the bookkeeping. If line $k$ cites line $i$ , then $\Gamma_i \subseteq \Gamma_k$ (Lemma 4.7.1 (a)), and the least value over a longer list is at most the least over a shorter one, so $m \le u(\Gamma_i) \le u(\varphi_i)$ . If line $k$ cites a box from line $a$ to line $b$ by a box rule, then $\Gamma_b = \Gamma_k, \varphi_a$ (Lemma 4.7.1 (b)), so the hypothesis for line $b$ says $\min\{ m, u(\varphi_a) \} \le u(\varphi_b)$ . Below, $x = u(\varphi)$ , $y = u(\psi)$ , $z = u(\chi)$ .

Premises and assumptions: $\varphi_k$ is in $\Gamma_k$ , so $m \le u(\varphi_k)$ . $\mathrm{R}$ : $m \le u(\varphi_i) = u(\varphi_k)$ . $\mathrm{\wedge I}$ : $m \le x$ and $m \le y$ , so $m \le \min\{x, y\}$ . $\mathrm{\wedge E}$ : $m \le \min\{x, y\} \le x$ , and likewise $\le y$ . $\mathrm{\vee I}$ : $m \le x \le \max\{x, y\}$ .

$\mathrm{{\to}E}$ : $m \le u(\varphi \to \psi)$ and $m \le x$ . If $x \le y$ , then $m \le x \le y$ . Otherwise $u(\varphi \to \psi) = y$ , so $m \le y$ . $\mathrm{{\leftrightarrow}E}$ : $m \le u(\varphi \leftrightarrow \psi) \le u(\varphi \to \psi)$ and $m \le x$ , so $m \le y$ as for $\mathrm{{\to}E}$ ; the second form is symmetric.

$\mathrm{\neg E}$ : $m \le x$ and $m \le u(\neg\varphi)$ . If $x = 0$ , then $m \le 0$ ; if $x > 0$ , then $u(\neg\varphi) = 0$ and $m \le 0$ . So $m = 0 = u(\bot)$ . $\mathrm{\bot E}$ : $m \le u(\bot) = 0$ , so $m = 0 \le u(\varphi_k)$ .

$\mathrm{{\to}I}$ : the hypothesis gives $\min\{m, x\} \le y$ . If $x \le y$ , then $u(\varphi \to \psi) = 1 \ge m$ . Otherwise $y < x$ and $u(\varphi \to \psi) = y$ ; since $\min\{m, x\} \le y < x$ , the minimum is not $x$ , so it is $m$ , and $m \le y$ . $\mathrm{{\leftrightarrow}I}$ : the same argument for each box gives $m \le u(\varphi \to \psi)$ and $m \le u(\psi \to \varphi)$ , so $m$ is at most their minimum.

$\mathrm{\neg I}$ : the hypothesis gives $\min\{m, x\} \le u(\bot) = 0$ . If $x = 0$ , then $u(\neg\varphi) = 1 \ge m$ . If $x > 0$ , the minimum is $0$ and is not $x$ , so $m = 0 \le u(\neg\varphi)$ .

$\mathrm{\vee E}$ : $m \le \max\{x, y\}$ , and the boxes give $\min\{m, x\} \le z$ and $\min\{m, y\} \le z$ . If $x \ge y$ , then $m \le x$ , so $\min\{m, x\} = m$ and $m \le z$ . If $y > x$ , then $m \le y$ and $m \le z$ from the second box.

This covers every rule used, so $\Gamma_k \models_3 \varphi_k$ for every line, and in particular for the last line, whose context is the premises. As in Step 4 of the proof of Theorem 4.7.2, a list containing all the premises has least value at most theirs, so every sequent $\Gamma \vdash \psi$ derived without $\mathrm{RAA}$ satisfies $\Gamma \models_3 \psi$ .

Now let $u(p) = \frac12$ . Then $u(\neg p) = 0$ , since $\frac12 > 0$ , and $u(\neg\neg p) = 1$ , since $u(\neg p) = 0$ . So $u(\neg\neg p) = 1 > \frac12 = u(p)$ , and $\neg\neg p \models_3 p$ fails. Also $u(p \vee \neg p) = \max\{ \frac12, 0 \} = \frac12 < 1$ , the value of the empty list, so $\models_3 p \vee \neg p$ fails. Hence neither sequent is derivable without $\mathrm{RAA}$ .

The case that was not written is $\mathrm{RAA}$ itself. Its box would give $\min\{m, u(\neg\varphi)\} \le 0$ , and we would need $m \le x$ . At $u(\varphi) = \frac12$ the box gives nothing, since $u(\neg\varphi) = 0$ already, while $m$ may be $1$ . This is the three-valued face of the question asked in the Idea of Theorem 4.7.2: the two-valued $\mathrm{RAA}$ case used that $v(\varphi) = \mathrm{F}$ forces $v(\neg\varphi) = \mathrm{T}$ , and with a third value, $\varphi$ and $\neg\varphi$ can both fail to be true.

Remark. The same values settle Peirce’s law, $((p \to q) \to p) \to p$ , which Section 2.5 derived with $\mathrm{RAA}$ (Proposition 2.5.4): at $u(p) = \frac12$ , $u(q) = 0$ , we get $u(p \to q) = 0$ , $u((p \to q) \to p) = 1$ , and the whole formula has value $\frac12$ , so it too needs $\mathrm{RAA}$ . The values do not refute everything Chapter 2 derived with $\mathrm{RAA}$ : the De Morgan direction $\neg(p \wedge q) \vdash \neg p \vee \neg q$ passes this test, and so does $\vdash (p \to q) \vee (q \to p)$ . Neither of these is derivable without $\mathrm{RAA}$ either, but showing that needs a different kind of model, and this book states it without proof, as Section 2.5’s Looking-ahead box announced. $\mathrm{RAA}$ says something the other rules cannot.

A technique, named. The proof is an instance of a general technique: to show that a rule cannot be derived from the others, find a new notion of “true” under which the other rules are sound and that rule is not. Here the notion has three values; Exercise C4 uses two values with $\bot$ read as an ordinary letter, and Exercise C5 two other three-valued tables. Each notion is a different semantics. For the two-valued tables the rules are not only sound but complete, which is Section 4.8’s theorem.