4.8 Completeness

Soundness (Theorem 4.7.2) says that the rules of Chapters 1 and 2 never lead from true premises to a false conclusion: whatever can be derived is true in every row where the premises are. That answers half of the chapter’s question. The other half is the converse. Could the rules be too weak, so that some sequent is true in every row and yet no derivation of it exists? This section proves that they are not: every truth-table consequence has a derivation. The proof reads a derivation off the truth table, one row at a time, and then glues the rows together with excluded middle.

4.8.1. The question soundness leaves open

Recall the two relations from Section 4.5. $\Gamma \vdash \psi$ says that there is a derivation of $\psi$ from premises in $\Gamma$ (Definition 1.2.3). $\Gamma \models \psi$ says that every valuation making all of $\Gamma$ true makes $\psi$ true (Definition 4.5.3). Soundness is the implication $\Gamma \vdash \psi \ \Rightarrow \ \Gamma \models \psi .$ Its converse is not automatic. The rules are a list that people wrote down, and a list can leave something out. Suppose, as a thought experiment, that we struck $\mathrm{RAA}$ (Definition 2.5.1) from the list. Every derivation that remains is still a derivation, so soundness still holds. But the tautology $p \vee \neg p$ would then have no derivation (this is the optional Theorem 4.7.4 of Section 4.7). So a sound list of rules can be too short. The question is whether our list is long enough.

Here is a sequent to keep in mind. The formula $(p \to q) \vee (q \to p)$ is a tautology: if $q$ is true then $p \to q$ is true, and if $q$ is false then $q \to p$ is true. Chapter 3 found a derivation of it (Exercise (C2: A disjunction from nothing)), but only after reaching for $\mathrm{LEM}$ , and nothing in Chapter 3 proved that a derivation would be there to find. We want a theorem that promises it in advance, for every tautology and every valid sequent.

We are going to prove:

If $\Gamma$ is a list of formulas and $\Gamma \models \psi$ , then $\Gamma \vdash \psi$ .

The plan has two ideas, one per row and one for all the rows together.

One row gives one derivation. Fix a row of the truth table, that is, a valuation $v$ . Write each atom as it stands in that row: $p$ if $v$ makes $p$ true, $\neg p$ if $v$ makes it false. From these signed atoms we will derive the formula $\psi$ if $\psi$ is true in the row, and $\neg\psi$ if it is false. The derivation climbs the parse tree of $\psi$ , one connective at a time.
The rows are glued by excluded middle. If $\Gamma \models \psi$ , the first idea gives $\psi$ from $\Gamma$ and the signed atoms of each row. Two rows that differ only at the atom $p$ have derivations from “ $\ldots, p$ ” and from “ $\ldots, \neg p$ ”. The rule $\mathrm{\vee E}$ applied to $p \vee \neg p$ merges them into one derivation that no longer mentions $p$ . Removing the atoms one at a time leaves a derivation from $\Gamma$ alone.

We keep the premises $\Gamma$ throughout, and we isolate the two ingredients as lemmas so that each can be checked on its own. Before either, we need a little bookkeeping about derivations.

Second readingWhere the route comes from

The first idea is known as Kalmár’s lemma, and gluing rows by excluded middle is the standard way to finish; the route is the classical one.

4.8.2. Bookkeeping: adding premises and chaining derivations

In Chapter 2 we learned to use a proved sequent as a single line (Definition 2.3.1), and Section 2.3 proved what that gives, Lemma 2.3.3: (a) extra premises never hurt; (b) a statement already derived may be used as a premise; (c) a sequent already proved may be applied to statements already derived. The completeness proof uses (a) and (c) dozens of times. They also made Step 1 of the proof of Theorem 4.7.2 honest: for whole derivations, part (c) is the precise form of “abbreviates”.

Quick check. Suppose $\Gamma \vdash \alpha$ and $\Gamma \vdash \neg\alpha$ . Which part of Lemma 2.3.3, applied to which proved sequent, gives $\Gamma \vdash \chi$ for every formula $\chi$ ?

Solution. Part (c) with $m = 2$ , $\alpha_1 = \alpha$ , $\alpha_2 = \neg\alpha$ and $\beta = \chi$ , applied to Proposition 2.1.1, $P, \neg P \vdash Q$ , with $\alpha$ for $P$ and $\chi$ for $Q$ .

4.8.3. The rules prove their own truth tables

Each line of the truth table of a connective says something like “with $\alpha$ true and $\beta$ false, $\alpha \to \beta$ comes out false”. Read with signs, that line is a sequent: from $\alpha$ and $\neg\beta$ , conclude $\neg(\alpha \to \beta)$ . If every such sequent is derivable, then the rules know the truth tables. This is the key to the first idea of the plan. Section 4.4 began by reading the tables off the rules; the lemma below makes that reading exact: every line of every table is a derivable sequent.

Lemma 4.8.1 (The Rules Prove the Truth Tables)

For all formulas $\alpha$ and $\beta$ , the following sequents are derivable, by derivations that do not use $\mathrm{RAA}$ .

(i) $(\neg 1)$ $\alpha \vdash \neg\neg\alpha$ , and $(\bot 1)$ $\vdash \neg\bot$ .
(ii) $(\wedge 1)$ $\alpha, \beta \vdash \alpha \wedge \beta$ ; $(\wedge 2)$ $\neg\alpha \vdash \neg(\alpha \wedge \beta)$ ; $(\wedge 3)$ $\neg\beta \vdash \neg(\alpha \wedge \beta)$ .
(iii) $(\vee 1)$ $\alpha \vdash \alpha \vee \beta$ ; $(\vee 2)$ $\beta \vdash \alpha \vee \beta$ ; $(\vee 3)$ $\neg\alpha, \neg\beta \vdash \neg(\alpha \vee \beta)$ .
(iv) $({\to}1)$ $\neg\alpha \vdash \alpha \to \beta$ ; $({\to}2)$ $\beta \vdash \alpha \to \beta$ ; $({\to}3)$ $\alpha, \neg\beta \vdash \neg(\alpha \to \beta)$ .
(v) $({\leftrightarrow}1)$ $\alpha, \beta \vdash \alpha \leftrightarrow \beta$ ; $({\leftrightarrow}2)$ $\neg\alpha, \neg\beta \vdash \alpha \leftrightarrow \beta$ ; $({\leftrightarrow}3)$ $\alpha, \neg\beta \vdash \neg(\alpha \leftrightarrow \beta)$ ; $({\leftrightarrow}4)$ $\neg\alpha, \beta \vdash \neg(\alpha \leftrightarrow \beta)$ .

Here are the tables of Definition 4.4.2 again, with each row tagged by the sequent of the lemma that derives it from the signed parts. Where two sequents fit a row, the tag is the one the proof of the next lemma uses.

$\alpha$	$\beta$	$\alpha \wedge \beta$	$\alpha \vee \beta$	$\alpha \to \beta$	$\alpha \leftrightarrow \beta$
T	T	T $(\wedge 1)$	T $(\vee 1)$	T $({\to}2)$	T $({\leftrightarrow}1)$
T	F	F $(\wedge 3)$	T $(\vee 1)$	F $({\to}3)$	F $({\leftrightarrow}3)$
F	T	F $(\wedge 2)$	T $(\vee 2)$	T $({\to}1)$	F $({\leftrightarrow}4)$
F	F	F $(\wedge 2)$	F $(\vee 3)$	T $({\to}1)$	T $({\leftrightarrow}2)$

Beside it: $\alpha$ T gives $\neg\alpha$ F, tagged $(\neg 1)$ ; $\alpha$ F gives $\neg\alpha$ T, and no sequent is needed, since the signed part $\neg\alpha$ is already the signed whole; $\bot$ is always F, tagged $(\bot 1)$ .

Each sequent has as premises only the parts it needs, each as itself or negated. For instance, $\alpha \wedge \beta$ is false as soon as $\alpha$ is false, whatever $\beta$ is, and $(\wedge 2)$ has the single premise $\neg\alpha$ . This economy will matter: when the proof of the next lemma uses a row, it needs to know something only about the parts the row mentions.

Idea. Most of the sequents are already in the book: rules of Chapter 1, or results of Chapter 2 with $\alpha$ and $\beta$ put in for the letters. The others are short derivations of the kinds Chapter 2 practiced: a box that repeats a premise, or a $\mathrm{\neg I}$ box that reaches a clash. The only thing to watch is that no step, and no cited result, uses $\mathrm{RAA}$ .

The derivations, with a check that none uses $\mathrm{RAA}$ , are in the fold below.

Second readingThe fifteen derivations

Proof. The table lists, for each sequent, the rows of the truth table it covers (by Definition 4.4.2) and where its derivation comes from. The letters of the Chapter 2 results are replaced by $\alpha$ and $\beta$ , as Definition 2.3.1 allows.

Tag	Rows covered	Sequent	Derivation
$(\neg 1)$	$\alpha$ T, so $\neg\alpha$ F	$\alpha \vdash \neg\neg\alpha$	Example (Two negations from one premise) (a)
$(\bot 1)$	$\bot$ is always F	$\vdash \neg\bot$	printed below
$(\wedge 1)$	T, T give T	$\alpha, \beta \vdash \alpha \wedge \beta$	$\mathrm{\wedge I}$ (Definition 1.2.5)
$(\wedge 2)$	F, anything give F	$\neg\alpha \vdash \neg(\alpha \wedge \beta)$	$\mathrm{\vee I}$ gives $\neg\alpha \vee \neg\beta$ , then Proposition 2.5.5 (c)
$(\wedge 3)$	anything, F give F	$\neg\beta \vdash \neg(\alpha \wedge \beta)$	$\mathrm{\vee I}$ gives $\neg\alpha \vee \neg\beta$ , then Proposition 2.5.5 (c)
$(\vee 1)$	T, anything give T	$\alpha \vdash \alpha \vee \beta$	$\mathrm{\vee I}$ (Definition 1.5.1)
$(\vee 2)$	anything, T give T	$\beta \vdash \alpha \vee \beta$	$\mathrm{\vee I}$
$(\vee 3)$	F, F give F	$\neg\alpha, \neg\beta \vdash \neg(\alpha \vee \beta)$	$\mathrm{\wedge I}$ gives $\neg\alpha \wedge \neg\beta$ , then Proposition 2.5.5 (b)
$({\to}1)$	F, anything give T	$\neg\alpha \vdash \alpha \to \beta$	Proposition 2.1.2
$({\to}2)$	anything, T give T	$\beta \vdash \alpha \to \beta$	printed below
$({\to}3)$	T, F give F	$\alpha, \neg\beta \vdash \neg(\alpha \to \beta)$	printed below
$({\leftrightarrow}1)$	T, T give T	$\alpha, \beta \vdash \alpha \leftrightarrow \beta$	printed below
$({\leftrightarrow}2)$	F, F give T	$\neg\alpha, \neg\beta \vdash \alpha \leftrightarrow \beta$	printed below
$({\leftrightarrow}3)$	T, F give F	$\alpha, \neg\beta \vdash \neg(\alpha \leftrightarrow \beta)$	printed below
$({\leftrightarrow}4)$	F, T give F	$\neg\alpha, \beta \vdash \neg(\alpha \leftrightarrow \beta)$	printed below

In the second column, “F, anything give F” means: if $\alpha$ is F, then $\alpha \wedge \beta$ is F whatever the value of $\beta$ .

The seven printed derivations follow. First $({\to}2)$ and $({\to}3)$ (the first is the derivation of Exercise (B2: An assumption that is not used) (a), printed again because a proof does not rest on an exercise): an implication whose conclusion we already have, and the refutation of an implication by a true hypothesis with a false conclusion.

\beta

\alpha

asm, for

\mathrm{{{\to}}I}

\beta

\mathrm{R}

\alpha \to \beta

\mathrm{{{\to}}I}

2–3

\alpha

\neg \beta

\alpha \to \beta

asm, for

\mathrm{{\neg}I}

\beta

\mathrm{{{\to}}E}

3, 1

\bot

\mathrm{{\neg}E}

4, 2

\neg (\alpha \to \beta)

\mathrm{{\neg}I}

3–5

Next $({\leftrightarrow}1)$ and $({\leftrightarrow}2)$ . In the first, each box repeats the premise it needs; in the second, each box reaches a clash and closes by $\mathrm{\bot E}$ .

\alpha

\beta

\alpha

asm, for

\mathrm{{{\leftrightarrow}}I}

\beta

\mathrm{R}

\beta

asm, for

\mathrm{{{\leftrightarrow}}I}

\alpha

\mathrm{R}

\alpha \leftrightarrow \beta

\mathrm{{{\leftrightarrow}}I}

3–4, 5–6

\neg \alpha

\neg \beta

\alpha

asm, for

\mathrm{{{\leftrightarrow}}I}

\bot

\mathrm{{\neg}E}

3, 1

\beta

\mathrm{{\bot}E}

\beta

asm, for

\mathrm{{{\leftrightarrow}}I}

\bot

\mathrm{{\neg}E}

6, 2

\alpha

\mathrm{{\bot}E}

\alpha \leftrightarrow \beta

\mathrm{{{\leftrightarrow}}I}

3–5, 6–8

Then $({\leftrightarrow}3)$ , $({\leftrightarrow}4)$ and $(\bot 1)$ . The first two assume the biconditional and use it in the direction that clashes with a premise; the last is a box whose assumption $\bot$ is already the $\bot$ that $\mathrm{\neg I}$ asks for, the degenerate box of Section 2.2.

\alpha

\neg \beta

\alpha \leftrightarrow \beta

asm, for

\mathrm{{\neg}I}

\beta

\mathrm{{{\leftrightarrow}}E}

3, 1

\bot

\mathrm{{\neg}E}

4, 2

\neg (\alpha \leftrightarrow \beta)

\mathrm{{\neg}I}

3–5

\neg \alpha

\beta

\alpha \leftrightarrow \beta

asm, for

\mathrm{{\neg}I}

\alpha

\mathrm{{{\leftrightarrow}}E}

3, 2

\bot

\mathrm{{\neg}E}

4, 1

\neg (\alpha \leftrightarrow \beta)

\mathrm{{\neg}I}

3–5

\bot

asm, for

\mathrm{{\neg}I}

\neg \bot

\mathrm{{\neg}I}

1–1

None of these derivations uses $\mathrm{RAA}$ : their boxes close by $\mathrm{{\to}I}$ , $\mathrm{\neg I}$ and $\mathrm{{\leftrightarrow}I}$ . Nor do the cited results: Proposition 2.1.2 and Example (Two negations from one premise) come from Sections 2.1 and 2.2, before $\mathrm{RAA}$ was introduced, and Chapter 2 derived De Morgan’s laws (b) and (c) without it (it says so right after the derivations of Proposition 2.5.5). This proves the lemma.

The $\neg$ connective needs only one sequent. When $\alpha$ is false, $\neg\alpha$ is true, and the “sequent” $\neg\alpha \vdash \neg\alpha$ is a one-line derivation; only the other row, $(\neg 1)$ , needs a proof.

Warning. The sequents of Lemma 4.8.1 go from the parts to the whole. Read backwards they are false. For instance $\alpha \vee \beta \vdash \alpha$ is not derivable in general: the row $p = \mathrm{F}$ , $q = \mathrm{T}$ makes $p \vee q$ true and $p$ false, so $p \vee q \nvdash p$ by Corollary 4.7.3. A row of a table tells us the value of the whole from the values of the parts, never the other way round.

Quick check. Which tagged sequent covers $\alpha$ F, $\beta$ T for $\to$ ? And for $\leftrightarrow$ ?

Solution. $({\to}1)$ , $\neg\alpha \vdash \alpha \to \beta$ . (The row also fits $({\to}2)$ .) For $\leftrightarrow$ : $({\leftrightarrow}4)$ , $\neg\alpha, \beta \vdash \neg(\alpha \leftrightarrow \beta)$ .

4.8.4. One row, one derivation

A row of a truth table can be written as a list of premises: each atom as it stands in the row, itself if true, negated if false.

$p$	$q$	$r$	the row, as premises
T	F	T	$p, \ \neg q, \ r$

We now name the formulas that “write down a row”.

A signed formula is a formula as it stands in one row: itself if the row makes it true, its negation if the row makes it false.

For a valuation $v$ and a formula $\varphi$ , the signed formula $\varphi^{v}$ is $\varphi^{v} \mathrel{:=} \begin{cases} \varphi & \text{if } v(\varphi) = \mathrm{T}, \\ \neg\varphi & \text{if } v(\varphi) = \mathrm{F}. \end{cases}$ The superscript $v$ is a label naming the row, not an exponent. In particular, for an atom $p$ , the signed atom $p^{v}$ is $p$ or $\neg p$ . For example, if $v(p) = \mathrm{T}$ and $v(q) = \mathrm{F}$ , then $p^{v} = p$ , $q^{v} = \neg q$ , $(p \to q)^{v} = \neg(p \to q)$ and $(q \to p)^{v} = q \to p$ . Whatever $v$ is, $v(\varphi^{v}) = \mathrm{T}$ : the signed formula is always the true one of $\varphi$ and $\neg\varphi$ , by the clause for $\neg$ in Definition 4.4.2.

The signed atoms $p_1^{v}, \dots, p_n^{v}$ describe the row of $v$ completely, as far as $p_1, \dots, p_n$ go. The next lemma says they are enough premises to derive the signed version of any formula built from these atoms.

Lemma 4.8.2 (One Row of the Truth Table Is Derivable)

Let $\varphi$ be a formula, let $p_1, \dots, p_n$ ( $n \ge 0$ ) be atoms among which are all the atoms of $\varphi$ , and let $v$ be a valuation. Then $p_1^{v}, \dots, p_n^{v} \vdash \varphi^{v} .$

In words: in each row of the truth table of $\varphi$ , the value of $\varphi$ can be derived from the values of its atoms, where “value T” is written as the formula and “value F” as its negation.

Idea. Climb the parse tree. At an atom, $\varphi^{v}$ is one of the premises. At a connective, the induction hypothesis gives the signed parts $\alpha^{v}$ , $\beta^{v}$ , and Lemma 4.8.1 has a sequent from (some of) those signed parts to the signed whole. So structural induction (Theorem 4.3.1), with Lemma 2.3.3 (c) to chain, does the whole job. The only care is to pick, for each pair of values, the row whose premises are the signs we actually have.

Proof. Fix the atoms $p_1, \dots, p_n$ and the valuation $v$ , and write $\Sigma$ for the list $p_1^{v}, \dots, p_n^{v}$ . We prove, by structural induction (Theorem 4.3.1), that every formula $\varphi$ has the property

if every atom of $\varphi$ is among $p_1, \dots, p_n$ , then $\Sigma \vdash \varphi^{v}$ .

Every atom of an immediate part $\alpha$ or $\beta$ of a formula is an atom of the formula itself, so when $\varphi$ satisfies the “if”, so do its immediate parts, and the induction hypothesis applies to them.

Atoms. Let $\varphi$ be an atom among $p_1, \dots, p_n$ , say $\varphi = p_i$ . Then $\varphi^{v} = p_i^{v}$ is a member of $\Sigma$ , and the one-line derivation whose only line is the premise $p_i^{v}$ shows $\Sigma \vdash \varphi^{v}$ .

The formula $\bot$ . By Definition 4.4.2, $v(\bot) = \mathrm{F}$ , so $\bot^{v} = \neg\bot$ . By $(\bot 1)$ of Lemma 4.8.1, $\vdash \neg\bot$ , and weakening (Lemma 2.3.3 (a)) gives $\Sigma \vdash \neg\bot$ .

Negation. Let $\varphi = \neg\alpha$ , and assume $\Sigma \vdash \alpha^{v}$ .

Case $v(\alpha) = \mathrm{T}$ . Then $\alpha^{v} = \alpha$ , and $v(\neg\alpha) = \mathrm{F}$ , so $\varphi^{v} = \neg\neg\alpha$ . From $\Sigma \vdash \alpha$ and $(\neg 1)$ , $\alpha \vdash \neg\neg\alpha$ , chaining (Lemma 2.3.3 (c)) gives $\Sigma \vdash \neg\neg\alpha$ .
Case $v(\alpha) = \mathrm{F}$ . Then $\alpha^{v} = \neg\alpha$ , and $v(\neg\alpha) = \mathrm{T}$ , so $\varphi^{v} = \neg\alpha = \alpha^{v}$ . The hypothesis is already the claim.

Conjunction. Let $\varphi = \alpha \wedge \beta$ , and assume $\Sigma \vdash \alpha^{v}$ and $\Sigma \vdash \beta^{v}$ . By Definition 4.4.2, $v(\alpha \wedge \beta) = \mathrm{T}$ exactly when $v(\alpha) = v(\beta) = \mathrm{T}$ .

Case $v(\alpha) = v(\beta) = \mathrm{T}$ . Then $\varphi^{v} = \alpha \wedge \beta$ , $\alpha^{v} = \alpha$ , $\beta^{v} = \beta$ . Chaining $\Sigma \vdash \alpha$ and $\Sigma \vdash \beta$ with $(\wedge 1)$ , $\alpha, \beta \vdash \alpha \wedge \beta$ , gives $\Sigma \vdash \alpha \wedge \beta$ .
Case $v(\alpha) = \mathrm{F}$ . Then $\varphi^{v} = \neg(\alpha \wedge \beta)$ and $\alpha^{v} = \neg\alpha$ . Chaining $\Sigma \vdash \neg\alpha$ with $(\wedge 2)$ , $\neg\alpha \vdash \neg(\alpha \wedge \beta)$ , gives $\Sigma \vdash \neg(\alpha \wedge \beta)$ . The hypothesis for $\beta$ is not used.
Case $v(\alpha) = \mathrm{T}$ , $v(\beta) = \mathrm{F}$ . Then $\varphi^{v} = \neg(\alpha \wedge \beta)$ and $\beta^{v} = \neg\beta$ , and chaining $\Sigma \vdash \neg\beta$ with $(\wedge 3)$ gives $\Sigma \vdash \neg(\alpha \wedge \beta)$ .

Implication. Let $\varphi = \alpha \to \beta$ , and assume $\Sigma \vdash \alpha^{v}$ and $\Sigma \vdash \beta^{v}$ . By Definition 4.4.2, $v(\alpha \to \beta) = \mathrm{F}$ exactly when $v(\alpha) = \mathrm{T}$ and $v(\beta) = \mathrm{F}$ .

Case $v(\alpha) = \mathrm{F}$ . Then $\varphi^{v} = \alpha \to \beta$ and $\alpha^{v} = \neg\alpha$ . Chaining $\Sigma \vdash \neg\alpha$ with $({\to}1)$ , $\neg\alpha \vdash \alpha \to \beta$ , gives $\Sigma \vdash \alpha \to \beta$ .
Case $v(\alpha) = \mathrm{T}$ , $v(\beta) = \mathrm{T}$ . Then $\varphi^{v} = \alpha \to \beta$ and $\beta^{v} = \beta$ . Chaining $\Sigma \vdash \beta$ with $({\to}2)$ , $\beta \vdash \alpha \to \beta$ , gives $\Sigma \vdash \alpha \to \beta$ .
Case $v(\alpha) = \mathrm{T}$ , $v(\beta) = \mathrm{F}$ . Then $\varphi^{v} = \neg(\alpha \to \beta)$ , $\alpha^{v} = \alpha$ and $\beta^{v} = \neg\beta$ . Chaining $\Sigma \vdash \alpha$ and $\Sigma \vdash \neg\beta$ with $({\to}3)$ , $\alpha, \neg\beta \vdash \neg(\alpha \to \beta)$ , gives $\Sigma \vdash \neg(\alpha \to \beta)$ .

Disjunction and biconditional. These go as for implication. For each pair of values of $\alpha$ and $\beta$ , the table in the proof of Lemma 4.8.1 names a sequent whose premises are among $\alpha^{v}$ , $\beta^{v}$ and whose conclusion is $\varphi^{v}$ : for $\vee$ , $(\vee 1)$ if $v(\alpha) = \mathrm{T}$ , $(\vee 2)$ if $v(\alpha) = \mathrm{F}$ and $v(\beta) = \mathrm{T}$ , $(\vee 3)$ if both are F; for $\leftrightarrow$ , $({\leftrightarrow}1)$ to $({\leftrightarrow}4)$ for the value pairs T T, F F, T F, F T. Chaining the induction hypotheses for those premises with that sequent gives $\Sigma \vdash \varphi^{v}$ .

The atoms and $\bot$ have the property, and each formation clause preserves it, so by Theorem 4.3.1 every formula has it. This proves the lemma.

Each case used the induction hypothesis only for the parts named in the premises of its sequent: the conjunction case with $\alpha$ false never looked at $\beta$ . That is the economy of Lemma 4.8.1 at work. The disjunction and biconditional cases are written out in Exercise (C1: The remaining cases).

Here is the lemma run on one formula, with every chained sequent written as a line.

Example (Deriving one row)

Let $\varphi = p \to (q \wedge \neg p)$ and let $v(p) = v(q) = \mathrm{T}$ . Find $\varphi^{v}$ , and write the derivation of $p^{v}, q^{v} \vdash \varphi^{v}$ that the proof of Lemma 4.8.2 produces.

Solution. Compute up the parse tree: $v(\neg p) = \mathrm{F}$ , so $v(q \wedge \neg p) = \mathrm{F}$ , and since $v(p) = \mathrm{T}$ , $v(\varphi) = \mathrm{F}$ . So $\varphi^{v} = \neg(p \to (q \wedge \neg p))$ , and the premises are $p^{v} = p$ and $q^{v} = q$ .

The proof climbs the same tree. At $\neg p$ with $v(p) = \mathrm{T}$ , it is the negation case with $\alpha$ true: $(\neg 1)$ gives $\neg\neg p$ . At $q \wedge \neg p$ , the values are T and F: $(\wedge 3)$ gives $\neg(q \wedge \neg p)$ from $(\neg p)^{v} = \neg\neg p$ . At the root, the values are T and F: $({\to}3)$ gives the goal from $p$ and $\neg(q \wedge \neg p)$ . Written as a derivation, with each sequent of Lemma 4.8.1 cited as a derived rule:

p

q

\neg\neg p

(\neg 1)

\neg (q \wedge \neg p)

(\wedge 3)

\neg (p \to (q \wedge \neg p))

({\to}3)

1, 4

The premise $q$ is never cited. It was used only in computing which case applies: the $\wedge$ case with $\beta = \neg p$ false needs only $\beta$ ’s sign, not $q$ ’s. A derivation need not use every premise (Definition 1.2.3).

Quick check. Let $\varphi = p \to \neg q$ and $v(p) = v(q) = \mathrm{T}$ . What sequent does Lemma 4.8.2 provide, and which sequent of Lemma 4.8.1 does the proof use at the root?

Solution. Here $v(\neg q) = \mathrm{F}$ , so $v(\varphi) = \mathrm{F}$ , and the lemma gives $p, q \vdash \neg(p \to \neg q)$ . At the root the values are T and F, so the proof uses $({\to}3)$ , $\alpha, \neg\beta \vdash \neg(\alpha \to \beta)$ , with $\alpha = p$ and $\beta = \neg q$ . Its premise $\neg\beta = \neg\neg q$ comes from the negation case below it: $q \vdash \neg\neg q$ , by $(\neg 1)$ .

4.8.5. Gluing the rows: splitting on an atom

Lemma 4.8.2 derives a formula from the signed atoms of one row. A sequent $\Gamma \vdash \psi$ mentions no row at all. The signed atoms must be removed, and the tool for that is excluded middle.

Lemma 4.8.3 (Splitting on an Atom)

Let $\Delta$ be a list of formulas, $p$ an atom and $\psi$ a formula. If $\Delta, p \vdash \psi$ and $\Delta, \neg p \vdash \psi$ , then $\Delta \vdash \psi$ .

Idea. This is proof by cases on $p \vee \neg p$ . Proposition 2.5.3 gives $p \vee \neg p$ with no premises, and $\mathrm{\vee E}$ (Definition 1.6.1) needs a box that reaches $\psi$ from $p$ and a box that reaches $\psi$ from $\neg p$ . The two given derivations are exactly the contents of those boxes, once their premise $p$ (or $\neg p$ ) is replaced by the box’s assumption.

Before reading on: this is the only place in the completeness proof where a classical rule enters. Where exactly, and why could the $\mathrm{\neg I}$ of Chapter 2 not do the job?

Proof. Let $D$ be a derivation of $\psi$ with premises in $\Delta, p$ , and $E$ one with premises in $\Delta, \neg p$ . Build a list of lines as follows.

As premises, every premise of $D$ or of $E$ that is a member of $\Delta$ .
The line $p \vee \neg p$ , justified by Proposition 2.5.3 ( $\mathrm{LEM}$ ) with $p$ for $P$ ; it cites nothing.
A box that opens with the assumption $p$ , followed by the lines of $D$ that are not premises, with their boxes. A citation of a premise of $D$ that is in $\Delta$ now cites the premise line of step 1; a citation of the premise $p$ now cites the assumption. If the last line of $D$ is itself a premise, the box is shorter: if that premise is $p$ , the box is the assumption alone, which is then its last line; otherwise the box is the assumption followed by $\psi$ , by $\mathrm{R}$ , citing the premise line carrying $\psi$ .
A second box, built from $E$ in the same way, opening with the assumption $\neg p$ .
The line $\psi$ , by $\mathrm{\vee E}$ , citing line 2 of this list and the two boxes.

This is a derivation (Definition 1.4.2). The premises lie in no box and come first, so they are available everywhere. Inside the first box, the lines of $D$ keep their boxes, which now sit inside the new box, and they cite the same lines and boxes as before, or a premise line, or the assumption, which is available at every line of its own box. As in the proof of Lemma 2.3.3, each line is still an instance of its rule. The last line of the first box is $\psi$ , and it is a line of that box itself and not of a box inside it: it was the last line of $D$ , which lies in no box of $D$ (or it is the assumption itself, or the repetition line). The same holds for the second box. Both boxes and the line $p \vee \neg p$ lie in no box, and neither does the last line, so they are available at it. Hence the last line is an instance of $\mathrm{\vee E}$ , and the list is a derivation of $\psi$ whose premises are all in $\Delta$ . So $\Delta \vdash \psi$ .

Here is its shape, with $\Delta$ standing for the premise lines:

h

\Delta

i

p \vee \neg p

\mathrm{LEM}

a

p

asm, for

\mathrm{{\vee}E}

\vdots

b

\psi

c

\neg p

asm, for

\mathrm{{\vee}E}

\vdots

d

\psi

k

\psi

\mathrm{{\vee}E}

i

a

–

b

c

–

d

The answer to the prompt: the classical rule enters at line $i$ . Proposition 2.5.3 was derived in Chapter 2 with $\mathrm{RAA}$ , and nothing else in the proof of this lemma is classical. $\mathrm{\neg I}$ could not replace it: $\mathrm{\neg I}$ produces a negation, and here we need a disjunction with no premises to split on. Nothing in the proof uses that $p$ is an atom; the lemma holds for any formula in place of $p$ , but atoms are all we shall split on.

4.8.6. The completeness theorem

Now the plan of the opening can be carried out.

Theorem 4.8.4 (Completeness)

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

A list is finite, as in Definition 1.2.3. That matters: the proof works with the atoms that occur in $\Gamma$ and $\psi$ , and it needs them to be finitely many.

Idea. Step roadmap. ① List the atoms $p_1, \dots, p_n$ of $\Gamma$ and $\psi$ . ② Claim: for every valuation $v$ , $\Gamma, p_1^{v}, \dots, p_n^{v} \vdash \psi$ . If $v$ makes all of $\Gamma$ true, then $\psi$ is true in that row, and Lemma 4.8.2 derives it. If $v$ makes some premise $\gamma$ false, the lemma derives $\neg\gamma$ , which clashes with the premise $\gamma$ . ③ Remove the signed atoms one at a time, the last first, by Lemma 4.8.3: an induction on the number of atoms removed. To remove $p_j$ we need derivations from both $p_j$ and $\neg p_j$ with the same other signed atoms: two rows that differ only at $p_j$ . That is why the Claim must hold for every valuation, not just one.

Let us run the method of the roadmap on the tautology of the opening.

Example (The method on a tautology)

Run the roadmap of Theorem 4.8.4 on $\models (p \to q) \vee (q \to p)$ , and write the derivation it produces, citing the sequents of Lemma 4.8.1 as derived rules.

Solution. Write $\chi$ for $(p \to q) \vee (q \to p)$ . The list $\Gamma$ is empty and the atoms are $p_1 = p$ , $p_2 = q$ . Every valuation makes $\chi$ true (if $v(q) = \mathrm{T}$ the left side is true; otherwise the right side is), so the Claim ② always falls in its first case (the row makes the premises, here none, true), and Lemma 4.8.2 produces four short derivations, one per row:

$p, q \vdash \chi$ : $p \to q$ by $({\to}2)$ from $q$ , then $\mathrm{\vee I}$ ;
$p, \neg q \vdash \chi$ : $q \to p$ by $({\to}1)$ from $\neg q$ , then $\mathrm{\vee I}$ ;
$\neg p, q \vdash \chi$ and $\neg p, \neg q \vdash \chi$ : $p \to q$ by $({\to}1)$ from $\neg p$ , then $\mathrm{\vee I}$ .

(In the row $p = \mathrm{F}$ , $q = \mathrm{T}$ , both $({\to}1)$ and $({\to}2)$ would do; the proof of Lemma 4.8.2 uses $({\to}1)$ whenever $\alpha$ is false.) ③ first splits on $q = p_2$ , twice: once with $p$ and once with $\neg p$ among the premises. Then it splits on $p = p_1$ , once. Three uses of Lemma 4.8.3 in two rounds. Pasting as in its proof, the last split is the outermost:

$Diagram. Labels: q, neg q, p, neg p, vdash chi : line 20, veeE on line 1, box 2--10, box 4--6:\\ (to 2), veeI, box 7--9:\\ (to 1), veeI, box 11--19, box 13--15:\\ (to 1), veeI, box 16--18:\\ (to 1), veeI$

Each leaf is one row of the table; each inner node is one use of Lemma 4.8.3.

p \vee \neg p

\mathrm{LEM}

p

asm, for

\mathrm{{\vee}E}

q \vee \neg q

\mathrm{LEM}

q

asm, for

\mathrm{{\vee}E}

p \to q

({\to}2)

(p \to q) \vee (q \to p)

\mathrm{{\vee}I}

\neg q

asm, for

\mathrm{{\vee}E}

q \to p

({\to}1)

(p \to q) \vee (q \to p)

\mathrm{{\vee}I}

(p \to q) \vee (q \to p)

\mathrm{{\vee}E}

3, 4–6, 7–9

\neg p

asm, for

\mathrm{{\vee}E}

q \vee \neg q

\mathrm{LEM}

q

asm, for

\mathrm{{\vee}E}

p \to q

({\to}1)

(p \to q) \vee (q \to p)

\mathrm{{\vee}I}

\neg q

asm, for

\mathrm{{\vee}E}

p \to q

({\to}1)

(p \to q) \vee (q \to p)

\mathrm{{\vee}I}

(p \to q) \vee (q \to p)

\mathrm{{\vee}E}

12, 13–15, 16–18

(p \to q) \vee (q \to p)

\mathrm{{\vee}E}

1, 2–10, 11–19

The derivation has 20 lines. The one found by search in Exercise (C2: A disjunction from nothing) has 13, and splits only once. Here the split on $q$ inside the box of $\neg p$ (lines 12–19) is wasted: both of its boxes do the same thing, because in the rows with $p$ false the value of $q$ does not matter. The proof is a method that always works, not a recipe for short derivations; to find a short one, search as in Section 3.1.

Quick check. In the tree, which two leaves do the same thing, and why?

Solution. The boxes 13–15 and 16–18. Both write $p \to q$ by $({\to}1)$ from $\neg p$ on line 11, because in a row with $p$ false, $p \to q$ is true whatever $q$ is.

Proof. Step 1. The list $\Gamma$ is finite and each formula has finitely many symbols, so only finitely many atoms occur in $\Gamma$ or $\psi$ . List them without repetition as $p_1, \dots, p_n$ , where $n \ge 0$ .

Step 2.

Claim. For every valuation $v$ , $\ \Gamma, p_1^{v}, \dots, p_n^{v} \vdash \psi$ .

Proof of Claim. Let $v$ be a valuation, and write $\Sigma$ for $p_1^{v}, \dots, p_n^{v}$ .

Case 1: $v(\gamma) = \mathrm{T}$ for every member $\gamma$ of $\Gamma$ . Since $\Gamma \models \psi$ , by Definition 4.5.3 $v(\psi) = \mathrm{T}$ , so $\psi^{v} = \psi$ . Every atom of $\psi$ is among $p_1, \dots, p_n$ , so Lemma 4.8.2 gives $\Sigma \vdash \psi$ , and weakening (Lemma 2.3.3 (a)) gives $\Gamma, \Sigma \vdash \psi$ .

Case 2: $v(\gamma) = \mathrm{F}$ for some member $\gamma$ of $\Gamma$ . Then $\gamma^{v} = \neg\gamma$ . Every atom of $\gamma$ is among $p_1, \dots, p_n$ , so Lemma 4.8.2 gives $\Sigma \vdash \neg\gamma$ , and by weakening $\Gamma, \Sigma \vdash \neg\gamma$ . Also $\Gamma, \Sigma \vdash \gamma$ , by the one-line derivation whose only line is the premise $\gamma$ . By Proposition 2.1.1, $\gamma, \neg\gamma \vdash \psi$ . Chaining (Lemma 2.3.3 (c)) gives $\Gamma, \Sigma \vdash \psi$ .

Step 3. For each integer $j$ with $0 \le j \le n$ , let $S(j)$ be the statement $\text{for every valuation } v, \quad \Gamma, p_1^{v}, \dots, p_j^{v} \vdash \psi ,$ where for $j = 0$ the list of signed atoms is empty. The Claim is $S(n)$ .

Claim. If $1 \le j \le n$ and $S(j)$ holds, then $S(j - 1)$ holds.

Proof of Claim. Let $v$ be a valuation. Let $v^{+}$ be the valuation that agrees with $v$ at every atom except that $v^{+}(p_j) = \mathrm{T}$ , and $v^{-}$ the one that agrees with $v$ except that $v^{-}(p_j) = \mathrm{F}$ ; by Definition 4.4.1, a valuation may assign any value to each atom, so both exist. The atoms $p_1, \dots, p_{j-1}$ are different from $p_j$ , so $v^{+}$ and $v^{-}$ agree with $v$ on them, and $p_i^{v^{+}} = p_i^{v^{-}} = p_i^{v}$ for $i < j$ . Also $p_j^{v^{+}} = p_j$ and $p_j^{v^{-}} = \neg p_j$ . Applying $S(j)$ to $v^{+}$ and to $v^{-}$ gives, with $\Delta$ standing for the list $\Gamma, p_1^{v}, \dots, p_{j-1}^{v}$ , $\Delta, p_j \vdash \psi \quad\text{and}\quad \Delta, \neg p_j \vdash \psi .$ By Lemma 4.8.3, $\Delta \vdash \psi$ . Since $v$ was arbitrary, this is $S(j - 1)$ .

Step 2 is $S(n)$ . Applying the Claim with $j = n$ , then $j = n - 1$ , and so on down to $j = 1$ , removes the signed atoms one at a time and reaches $S(0)$ . This descent is an induction on the number of atoms removed; the fold after the proof writes it out.

Step 4. $S(0)$ says that $\Gamma \vdash \psi$ , for every valuation $v$ ; there is at least one valuation (for instance the one making every atom true), so $\Gamma \vdash \psi$ . This proves the theorem.

Second readingThe descent, as an induction

It remains to go down from $S(n)$ to $S(0)$ , which takes $n$ applications of the Claim. We count the applications made: for $m \in \mathbb{N}$ , let $T(m)$ say “if $m \le n$ , then $S(n - m)$ holds”. $T(0)$ says that $S(n)$ holds, which is Step 2. Suppose $T(m)$ holds, and let $m + 1 \le n$ . Then $m \le n$ , so $S(n - m)$ holds by $T(m)$ ; and $j \mathrel{:=} n - m$ satisfies $1 \le j \le n$ , because $0 \le m \le n - 1$ . The Claim gives $S(j - 1) = S(n - (m + 1))$ , which is $T(m + 1)$ . By Axiom 4.2.1, $T(m)$ holds for every $m \in \mathbb{N}$ , and $T(n)$ is $S(0)$ .

If $n = 0$ , the formulas of $\Gamma$ and $\psi$ are built from $\bot$ alone, and Step 3 does nothing: $S(0)$ is the Claim itself.

Warning. Completeness promises a derivation, not a short one. For a sequent with $n$ atoms, the proof builds $2^n$ row derivations and glues them with $2^n - 1$ splittings: with $n = 10$ atoms, that is 1024 row derivations and 1023 uses of $\mathrm{LEM}$ . The theorem answers “is there a derivation?”, not “how short is the shortest?”.

With soundness, completeness closes the circle.

Corollary 4.8.5 (Derivable Means Valid)

For every list of formulas $\Gamma$ and every formula $\psi$ , $\Gamma \vdash \psi \iff \Gamma \models \psi .$ In particular, whether $\Gamma \vdash \psi$ holds can be decided by checking the $2^n$ rows of a truth table, where $n$ is the number of atoms occurring in $\Gamma$ and $\psi$ .

Proof. $(\Rightarrow)$ is Theorem 4.7.2 and $(\Leftarrow)$ is Theorem 4.8.4. For the second sentence, let $p_1, \dots, p_n$ be the atoms occurring in $\Gamma$ and $\psi$ . By Lemma 4.4.1, the values of the members of $\Gamma$ and of $\psi$ under a valuation depend only on its values at $p_1, \dots, p_n$ , so $\Gamma \models \psi$ holds exactly when it holds in each of the $2^n$ rows of the joint truth table. That is a finite check, and by the first sentence it decides $\Gamma \vdash \psi$ .

So a question that looks as if it needs a search through infinitely many possible derivations can be settled by a finite table. The search for a derivation may still be the quicker way to a yes, and one row is the quickest way to a no (Corollary 4.7.3), but neither is needed.

Consistent and satisfiable coincide. Section 4.7 showed that a satisfiable list is consistent. Completeness gives the converse. If $\Delta$ is unsatisfiable, no row makes $\Delta$ true, so $\Delta \models \bot$ (there is no row to check), and $\Delta \vdash \bot$ by Theorem 4.8.4: $\Delta$ is inconsistent. So a finite list is consistent exactly when it is satisfiable. The word of Section 3.2 and the word of Section 4.5 pick out the same lists, though one speaks of derivations and the other of rows; Section 3.2’s task “derive $\bot$ ” and Section 4.6’s search on a list always give the same answer.

Second readingWhy two definitions of ‘follows’ are enough

Before Chapter 1, “ $\psi$ follows from $\Gamma$ ” had only an informal meaning: whatever a careful mathematician accepts as a valid inference, by any means. That is not a definition, but two things about it are clear for propositional forms. If $\Gamma \vdash \psi$ , then $\psi$ follows informally: each rule is an inference every mathematician accepts, and a chain of accepted inferences is accepted. If $\psi$ follows informally from $\Gamma$ by form alone, then $\Gamma \models \psi$ : an inference valid by its form cannot have a row, which is one way of reading the atoms, making the premises true and the conclusion false. So the informal notion is squeezed between $\vdash$ and $\models$ , and completeness makes the two ends meet: for propositional forms, the informal notion coincides with both. An argument of this shape is due to Georg Kreisel.

Second readingInfinitely many premises

We defined $\Gamma \vdash \psi$ only for a list, that is, for finitely many premises. One may allow an infinite collection $\Gamma$ of premises and say $\Gamma \vdash \psi$ when $\psi$ is derivable from finitely many members of $\Gamma$ (a derivation has finitely many lines, so it can only use finitely many). The equivalence with $\Gamma \models \psi$ still holds for infinite $\Gamma$ (completeness for infinitely many premises); together with the finiteness of derivations it gives the compactness theorem of propositional logic. The optional Section 4.10 proves both; nothing in the core depends on them. Our proof does not reach infinite $\Gamma$ : Step 1 needs finitely many atoms.

4.8.7. Two columns that agree

Section 4.5 set the two meanings of “follows” side by side. Here is the full table, now that both theorems are proved: they agree row by row (Corollary 4.8.5 and the paragraph on consistency above).

Notion	In terms of derivations	In terms of rows
follows	$\Gamma \vdash \psi$ (Definition 1.2.3, Section 1.2)	$\Gamma \models \psi$ (Definition 4.5.3, Section 4.5)
true by form alone	a theorem, $\vdash \varphi$	a tautology, $\models \varphi$ (Definition 4.5.1)
say the same	provably equivalent (Definition 2.4.2, Section 2.4)	semantically equivalent (Definition 4.5.4)
cannot hold together	inconsistent, $\Gamma \vdash \bot$ (Definition 3.2.1, Section 3.2)	unsatisfiable (Definition 4.5.2)
shown to hold by	one derivation	every row, or a closed search tree (Proposition 4.6.1)
shown to fail by	one refuting row (Corollary 4.7.3)	one refuting row
more premises, cut	Lemma 2.3.3 (Section 2.3): chaining and cut are why a derived rule may be cited	Section 4.5’s structural properties: one line about rows each
tied together by	soundness, $\vdash \Rightarrow \models$ (Theorem 4.7.2)	completeness, $\models \Rightarrow \vdash$ (Theorem 4.8.4)

4.8.8. Two roads to every answer

We now have two independent ways to settle any question “is $\Gamma \vdash \psi$ ?”. One is to search for a derivation, as in Section 3.1. The other is to check a table, and Corollary 4.8.5 says the two always agree. Here are two of Chapter 2’s classical laws settled by the table first.

De Morgan’s law (d). Is $\neg(p \wedge q) \models \neg p \vee \neg q$ ? The four rows: $\begin{array}{cc|c|c} p & q & \neg(p \wedge q) & \neg p \vee \neg q \\ \hline \mathrm{T} & \mathrm{T} & \mathrm{F} & \mathrm{F} \\ \mathrm{T} & \mathrm{F} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{T} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{F} & \mathrm{T} & \mathrm{T} \end{array}$ In every row where the premise is T, so is the conclusion. So $\neg(p \wedge q) \models \neg p \vee \neg q$ , and by Theorem 4.8.4, $\neg(p \wedge q) \vdash \neg p \vee \neg q$ .

Peirce’s law. Is $(p \to q) \to p \models p$ ? Work backwards from F (Section 4.4). A refuting row would need $p$ false. Then $p \to q$ is true, so $(p \to q) \to p$ is “true implies false”, which is false. So no row makes the premise true and the conclusion false: $(p \to q) \to p \models p$ , and by Theorem 4.8.4, $(p \to q) \to p \vdash p$ .

Both answers came before anyone found a derivation. Chapter 2 found both by hand (Proposition 2.5.5 (d), and Proposition 2.5.4, whose $\vdash ((P \to Q) \to P) \to P$ gives the sequent by $\mathrm{{\to}E}$ ), and the derivations there use $\mathrm{RAA}$ . Completeness explains why a search had to succeed; it does not say how.

Second readingWhat the proof used

A common alternative route first turns $\Gamma \models \psi$ into a single tautology, $\models \gamma_1 \to (\gamma_2 \to \cdots \to (\gamma_k \to \psi))$ , proves completeness for tautologies, and then unpacks the implications with $\mathrm{{\to}E}$ . Keeping $\Gamma$ as premises, as Step 2 does, costs one extra case (a false premise) and saves that detour.

Section 4.5 remarked that the tables do not see which of Chapter 2’s laws needed $\mathrm{RAA}$ . Now we can say why they cannot. A table decides $\Gamma \models \psi$ , and by Corollary 4.8.5 that is the same as derivability with all the rules, $\mathrm{RAA}$ included. A table has no column recording which rules a derivation uses. Whether a sequent can be derived without $\mathrm{RAA}$ is a question about a shorter list of rules, and for that list the completeness theorem is false, as the next paragraph explains. So no truth-table check can tell the laws that need $\mathrm{RAA}$ from those that do not.

Which rules did the proof of completeness itself use? Lemma 2.3.3 only pastes derivations. Lemma 4.8.1 uses no $\mathrm{RAA}$ , as its proof checks. Lemma 4.8.2 and the Claim chain those sequents, together with Proposition 2.1.1, which Chapter 2 derived before $\mathrm{RAA}$ appeared. The one classical step is the line $p \vee \neg p$ of Lemma 4.8.3. So the theorem is really about the full list of rules, $\mathrm{RAA}$ included. Without $\mathrm{RAA}$ the list is sound but not complete, as the optional Theorem 4.7.4 shows for $\vdash p \vee \neg p$ and $\neg\neg p \vdash p$ ; the proof above breaks exactly at the splitting.

Warning. Completeness does not say that a tautology has a derivation without $\mathrm{RAA}$ . It says there is a derivation from the rules of Chapters 1 and 2, all of them. The formula $(p \to q) \vee (q \to p)$ is a tautology, and every derivation found for it so far uses $\mathrm{LEM}$ or $\mathrm{RAA}$ . Whether a particular tautology can do without them is a different question, and a table cannot answer it.

4.8.9. A truth-table step: TAUT

Completeness has a practical consequence. Any step from earlier lines to a new one that a truth table confirms can be filled in by a derivation, so the step may be written as one line and the filling left to the theorem.

Definition 4.8.1 (The Step TAUT)

In a derivation of formulas of Definition 4.1.1, a line $\psi$ may be justified by TAUT, citing lines $i_1, \dots, i_m$ ( $m \ge 0$ ) available at it, if $\varphi_{i_1}, \dots, \varphi_{i_m} \models \psi$ : every row that makes the cited lines true makes $\psi$ true. For $m = 0$ , $\psi$ must be a tautology.

A TAUT line abbreviates a derivation in the rules of Chapters 1 and 2: by Corollary 4.8.5, $\varphi_{i_1}, \dots, \varphi_{i_m} \vdash \psi$ , and that derivation is pasted in as a derived rule’s is (Definition 2.3.1; Lemma 2.3.3 for a line in no box). So TAUT derives nothing new, and Theorem 4.7.2 holds for derivations that use it. A TAUT line is checked by a table, not found by a search; its justification reads “TAUT” with the cited lines.

Convention. TAUT is a license, not a style. It is used only for a step that a written proof would pass over without comment, such as a rearrangement of connectives (“so if $p$ , then $q$ ”), never to hide the step an argument is about.

Example (One line for twelve)

Derive $\neg(p \to q) \vdash p \wedge \neg q$ with TAUT, and say what the step abbreviates.

Solution.

\neg (p \to q)

p \wedge \neg q

\mathrm{TAUT}

The check: the premise is true only in the row $p = \mathrm{T}$ , $q = \mathrm{F}$ , since an implication is false only there, and $p \wedge \neg q$ is true in that row. Written out with the rules of Chapter 2, the derivation takes twelve lines (fold below). It is a step a written proof passes over (“an implication fails only with a true hypothesis and a false conclusion”), so the convention allows it.

Second readingThe step written out

An $\mathrm{RAA}$ box on $\neg p$ , in which Proposition 2.1.2 (VI) gives $p \to q$ , clashing with line 1, gives $p$ . A $\mathrm{\neg I}$ box on $q$ , in which an inner box gives $p \to q$ again, gives $\neg q$ . Then $\mathrm{\wedge I}$ . The proof that a TAUT line can always be written out builds a longer derivation still, by the method of Theorem 4.8.4; this one was found by search.

\neg (p \to q)

\neg p

asm, for

\mathrm{RAA}

p \to q

VI 2

\bot

\mathrm{{\neg}E}

3, 1

p

\mathrm{RAA}

2–4

q

asm, for

\mathrm{{\neg}I}

p

asm, for

\mathrm{{{\to}}I}

q

\mathrm{R}

p \to q

\mathrm{{{\to}}I}

7–8

\bot

\mathrm{{\neg}E}

9, 1

\neg q

\mathrm{{\neg}I}

6–10

p \wedge \neg q

\mathrm{{\wedge}I}

5, 11

Quick check. May line 3 be justified by TAUT: 1 $p \vee q$ ; 2 $p \to r$ ; 3 $r \vee q$ , TAUT 1, 2?

Solution. Yes. In a row making lines 1 and 2 true, either $p$ is true, and then $r$ is, or $p$ is false, and then $q$ is; either way $r \vee q$ is true.

Warning (Not allowed: TAUT). The first three steps break a clause of Definition 4.8.1, named in the tag; the fourth is legal and breaks the convention.

“ $q \to p$ , TAUT 1”, with line 1 $p \to q$ . The row $p = \mathrm{F}$ , $q = \mathrm{T}$ makes line 1 true and the new line false. Clause “every row that makes the cited lines true”.
Citing by TAUT a line inside a box that has closed. Clause “available”: the scope rule of Definition 1.4.2.
TAUT on a line that is not a formula of Definition 4.1.1, such as “for every $x$ , $x^2 \ge 0$ ”. Clause “formulas of Definition 4.1.1”.
“ $\neg p$ , TAUT 1, 2”, with lines $p \to q$ and $\neg q$ , in a proof whose point is that contrapositive step. Convention: legal by the definition, but it hides the step the argument is about; write $\mathrm{MT}$ (Proposition 2.3.1) or the derivation.

Remark (Looking ahead). Chapter 6 extends TAUT to formulas with quantifiers, reading each quantified part as a letter; Chapter 8 names the steps a written proof passes over without comment.

4.8.10. Exercises

A. Check your understanding

Exercise (A1)

These questions are about Lemma 4.8.2 and Theorem 4.8.4.

(a) In the conjunction case of the proof of Lemma 4.8.2, suppose $v(\alpha) = \mathrm{F}$ and $v(\beta) = \mathrm{T}$ . Which sequent of Lemma 4.8.1 is used, and which induction hypotheses?
(b) Where is $\mathrm{RAA}$ used in the proof of Theorem 4.8.4, including inside the results it cites?
(c) State the idea of the proof of Theorem 4.8.4 in two sentences.
(d) Run Step 2 of the proof for $\Gamma = p$ , $\psi = p \vee q$ and the valuation with $v(p) = \mathrm{F}$ , $v(q) = \mathrm{T}$ : which case applies, and which sequent does it prove?
(e) Step 1 lists the atoms without repetition. Where in the proof is that used?
(f) Which step of the proof fails if $\Gamma$ is allowed to be an infinite collection of formulas, each with its own atoms?

Solution. (a) $(\wedge 2)$ , $\neg\alpha \vdash \neg(\alpha \wedge \beta)$ , and only the hypothesis for $\alpha$ , $\Sigma \vdash \neg\alpha$ . The hypothesis for $\beta$ is not needed, because $\alpha \wedge \beta$ is false once $\alpha$ is.

(b) Only inside Lemma 4.8.3, at the line $p \vee \neg p$ : Proposition 2.5.3 was derived with $\mathrm{RAA}$ . The sequents of Lemma 4.8.1 are derived without it, Lemma 2.3.3 only pastes derivations, and Proposition 2.1.1 comes before $\mathrm{RAA}$ in Chapter 2.

(c) Each row of the truth table gives a derivation of the conclusion from the premises and that row’s signed atoms: by Lemma 4.8.2 if the row makes every premise true, and from a clash with a false premise otherwise. Two rows that differ at one atom are merged by excluded middle and proof by cases, and after all the atoms are merged the signed atoms are gone.

(d) The valuation makes the premise $p$ false, so Case 2 applies with $\gamma = p$ . Lemma 4.8.2 gives $\neg p, q \vdash \neg p$ (the atom case), the premise gives $p$ , and Proposition 2.1.1 gives $p \vee q$ . The sequent proved is $p, \neg p, q \vdash p \vee q$ .

(e) In the Claim of Step 3: $v^{+}$ and $v^{-}$ change only the value at $p_j$ , and they agree with $v$ on $p_1, \dots, p_{j-1}$ only because those atoms differ from $p_j$ . If $p_j$ also appeared as some $p_i$ with $i < j$ , then $p_i^{v^{+}} = p_j$ and $p_i^{v^{-}} = \neg p_j$ would differ, and the two sequents would not share the list $\Delta$ that Lemma 4.8.3 needs.

(f) Step 1. Infinitely many atoms may occur, so there is no finite list $p_1, \dots, p_n$ : the Claim would need infinitely many signed atoms as premises, which is not a list, and Step 3’s descent from $S(n)$ has no $n$ to start from.

Exercise (A2: Drill)

The parts run from signed formulas and the steps of the proof, through consistency and the two columns, to judging TAUT lines.

(a) $v(p) = \mathrm{F}$ , $v(q) = \mathrm{T}$ . Write $p^{v}$ , $q^{v}$ , $(p \to q)^{v}$ , $(q \to p)^{v}$ .
(b) $\varphi = \neg p \wedge q$ , $v(p) = v(q) = \mathrm{T}$ . Which sequent does Lemma 4.8.2 give?
(c) In (b), which tagged sequent does the proof use at the root, and where does its premise come from?
(d) A sequent has three atoms. How many row derivations and how many uses of Lemma 4.8.3 does the method build?
(e) In the step from $S(j)$ to $S(j - 1)$ , which signed atom disappears?
(f) $\Gamma = q$ , $\psi = p \vee q$ , $v(p) = v(q) = \mathrm{F}$ . Which case of the Claim of Step 2 applies?
(g) Is this TAUT line legal: 2 $p \vee q$ ; 3 $\neg p$ ; 5 $q$ , TAUT 2, 3?
(h) Is this one legal: 1 $p \to q$ ; 4 $q \to p$ , TAUT 1?
(i) Is the list $p \vee q, \ \neg p, \ \neg q$ consistent?
(j) In the table “Two columns that agree”, what is the twin of “a theorem”?
(k) May $\neg(p \wedge \neg p)$ be written by TAUT citing no line?
(l) A list is satisfiable. What does completeness add to what soundness already says about it?

Solution.

(a) $\neg p$ , $q$ , $p \to q$ , $\neg(q \to p)$ .
(b) $p, q \vdash \neg(\neg p \wedge q)$ .
(c) $(\wedge 2)$ with $\alpha = \neg p$ : $\neg\neg p \vdash \neg(\neg p \wedge q)$ . The premise $\neg\neg p$ comes from $p$ by $(\neg 1)$ .
(d) $8$ and $7$ .
(e) $p_j^{v}$ .
(f) Case 2, with $\gamma = q$ , which $v$ makes false.
(g) Yes: every row making $p \vee q$ and $\neg p$ true makes $q$ true.
(h) No: the row $p = \mathrm{F}$ , $q = \mathrm{T}$ makes line 1 true and line 4 false.
(i) No. It is unsatisfiable, so inconsistent (“Consistent and satisfiable coincide”); directly, $\mathrm{\vee E}$ on $p \vee q$ with $\mathrm{\neg E}$ in each box gives $\bot$ .
(j) A tautology.
(k) Yes: it is a tautology ( $m = 0$ ).
(l) Nothing about this list: soundness already makes it consistent. Completeness speaks of unsatisfiable lists: they are inconsistent.

B. Practice

Exercise (B1: Three rows from the primitive rules)

The table in the proof of Lemma 4.8.1 obtains $(\wedge 2)$ , $(\wedge 3)$ and $(\vee 3)$ from De Morgan’s laws. Derive $\neg\alpha \vdash \neg(\alpha \wedge \beta), \qquad \neg\beta \vdash \neg(\alpha \wedge \beta), \qquad \neg\alpha, \neg\beta \vdash \neg(\alpha \vee \beta)$ directly from the primitive rules, and say which of your derivations use $\mathrm{RAA}$ .

Solution. Each goal is a negation, so each derivation opens a $\mathrm{\neg I}$ box on the unnegated formula and hunts for a clash.

\neg \alpha

\alpha \wedge \beta

asm, for

\mathrm{{\neg}I}

\alpha

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

3, 1

\neg (\alpha \wedge \beta)

\mathrm{{\neg}I}

2–4

\neg \beta

\alpha \wedge \beta

asm, for

\mathrm{{\neg}I}

\beta

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

3, 1

\neg (\alpha \wedge \beta)

\mathrm{{\neg}I}

2–4

For the disjunction, the assumption $\alpha \vee \beta$ is used by $\mathrm{\vee E}$ with the goal $\bot$ , and each case clashes with one premise.

\neg \alpha

\neg \beta

\alpha \vee \beta

asm, for

\mathrm{{\neg}I}

\alpha

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

4, 1

\beta

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

6, 2

\bot

\mathrm{{\vee}E}

3, 4–5, 6–7

\neg (\alpha \vee \beta)

\mathrm{{\neg}I}

3–8

The three derivations have 5, 5 and 9 lines, and none uses $\mathrm{RAA}$ : every box closes by $\mathrm{\neg I}$ or $\mathrm{\vee E}$ .

Exercise (B2: The method on modus ponens)

Apply the method of Theorem 4.8.4 to $p, \ p \to q \models q$ : list the four rows and the case of Step 2 that each falls under, and write the derivation that the proof produces, citing $\mathrm{LEM}$ and the sequents of Lemma 4.8.1 as single lines. (It is long; that is expected, and the usual length of an exercise answer does not apply.) Compare it with the derivation by $\mathrm{{\to}E}$ .

Solution. The atoms are $p_1 = p$ and $p_2 = q$ . The rows:

$p = \mathrm{T}$ , $q = \mathrm{T}$ : both premises true, Case 1; $q^{v} = q$ is itself a premise.
$p = \mathrm{T}$ , $q = \mathrm{F}$ : the premise $p \to q$ is false, Case 2 with $\gamma = p \to q$ ; Lemma 4.8.2 gives $p, \neg q \vdash \neg(p \to q)$ by $({\to}3)$ .
$p = \mathrm{F}$ , $q$ either value: the premise $p$ is false, Case 2 with $\gamma = p$ ; the lemma gives $\neg p$ (an atom case).

In Case 2, the clash is $\mathrm{\neg E}$ followed by $\mathrm{\bot E}$ , which is the derivation of Proposition 2.1.1 written out. Splitting on $q$ inside each case of a split on $p$ , the derivation has this shape:

$Diagram. Labels: q, neg q, p, neg p, line 21, veeE on line 3, box 4--11\\ (veeE at 11 on line 5), box 6--6:\\ the goal is\\ the assumption, box 7--10: (to 3),\\ clash with line 2,\\ botE, box 12--20\\ (veeE at 20 on line 13), box 14--16:\\ clash of lines\\ 1 and 12, botE, box 17--19:\\ the same clash$

Written out:

p

p \to q

p \vee \neg p

\mathrm{LEM}

p

asm, for

\mathrm{{\vee}E}

q \vee \neg q

\mathrm{LEM}

q

asm, for

\mathrm{{\vee}E}

\neg q

asm, for

\mathrm{{\vee}E}

\neg (p \to q)

({\to}3)

4, 7

\bot

\mathrm{{\neg}E}

2, 8

q

\mathrm{{\bot}E}

q

\mathrm{{\vee}E}

5, 6–6, 7–10

\neg p

asm, for

\mathrm{{\vee}E}

q \vee \neg q

\mathrm{LEM}

q

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

1, 12

q

\mathrm{{\bot}E}

\neg q

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

1, 12

q

\mathrm{{\bot}E}

q

\mathrm{{\vee}E}

13, 14–16, 17–19

q

\mathrm{{\vee}E}

3, 4–11, 12–20

The box at line 6 has one line: in the row $p = q = \mathrm{T}$ the goal $q$ is the signed atom itself, so, as in the proof of Lemma 4.8.3, the box is its assumption alone. The result has 21 lines. The derivation by $\mathrm{{\to}E}$ has 3: the two premises and $q$ by $\mathrm{{\to}E}$ citing lines 2 and 1. The method is uniform, not short: it does the same thing for every valid sequent, and pays for that with a split on every atom.

Exercise (B3: Table first, then a derivation)

Decide by a truth table whether $\neg(p \leftrightarrow q) \models \neg p \leftrightarrow q$ . If it holds, find a derivation of $\neg(p \leftrightarrow q) \vdash \neg p \leftrightarrow q$ by search, where you may cite the sequents of Lemma 4.8.1 as derived rules. Which rule of your derivation is classical?

Solution. The table: $\begin{array}{cc|c|c} p & q & \neg(p \leftrightarrow q) & \neg p \leftrightarrow q \\ \hline \mathrm{T} & \mathrm{T} & \mathrm{F} & \mathrm{F} \\ \mathrm{T} & \mathrm{F} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{T} & \mathrm{T} & \mathrm{T} \\ \mathrm{F} & \mathrm{F} & \mathrm{F} & \mathrm{F} \end{array}$ The premise is true in rows 2 and 3, and so is the conclusion. So the entailment holds, and by Theorem 4.8.4 a derivation exists.

The search: the goal is a biconditional, so two boxes, one from $\neg p$ to $q$ and one from $q$ to $\neg p$ . In the second, the goal $\neg p$ is a negation: a box on $p$ , and $p$ , $q$ give $p \leftrightarrow q$ by $({\leftrightarrow}1)$ , which clashes with the premise. In the first, the goal $q$ is an atom, the only premise is a negation, and nothing else applies: we are stuck, and assume $\neg q$ . Then $\neg p$ , $\neg q$ give $p \leftrightarrow q$ by $({\leftrightarrow}2)$ , which clashes with the premise.

\neg (p \leftrightarrow q)

\neg p

asm, for

\mathrm{{{\leftrightarrow}}I}

\neg q

asm, for

\mathrm{RAA}

p \leftrightarrow q

({\leftrightarrow}2)

2, 3

\bot

\mathrm{{\neg}E}

4, 1

q

\mathrm{RAA}

3–5

q

asm, for

\mathrm{{{\leftrightarrow}}I}

p

asm, for

\mathrm{{\neg}I}

p \leftrightarrow q

({\leftrightarrow}1)

8, 7

\bot

\mathrm{{\neg}E}

9, 1

\neg p

\mathrm{{\neg}I}

8–10

\neg p \leftrightarrow q

\mathrm{{{\leftrightarrow}}I}

2–6, 7–11

The classical rule is the $\mathrm{RAA}$ at line 6. (Pasting in the derivations of the two cited sequents gives a derivation in the primitive rules of 22 lines.) Whether some other derivation could avoid $\mathrm{RAA}$ is a question the table cannot answer. In fact none can; we state that without proof, as Chapter 2 did for similar sequents, and nothing depends on it.

Exercise (B4: When TAUT is welcome)

(a) Derive $p \to (q \wedge r), \ \neg r \vdash \neg p$ twice: once with a single TAUT line, once with primitive rules.
(b) By the convention of this section, which is the better proof, and why?
(c) In a longer derivation, line 7 holds $\neg(p \wedge \neg q)$ and line 8 holds $p \to q$ . Justify line 8 by TAUT, and say why the convention allows it.

Solution.

(a) With TAUT, line 3 is justified because a row making both premises true has $r$ false, so $q \wedge r$ false, so $p$ false. With primitive rules, a $\mathrm{\neg I}$ box on $p$ :
1 $p \to (q \wedge r)$
2 $\neg r$
3 $\neg p$ $\mathrm{TAUT}$ 1, 2
1 $p \to (q \wedge r)$
2 $\neg r$
3 $p$ asm, for $\mathrm{{\neg}I}$
4 $q \wedge r$ $\mathrm{{{\to}}E}$ 1, 3
5 $r$ $\mathrm{{\wedge}E}$ 4
6 $\bot$ $\mathrm{{\neg}E}$ 5, 2
7 $\neg p$ $\mathrm{{\neg}I}$ 3–6
(b) The primitive one. The TAUT line hides the only idea of the argument, modus tollens through the conjunction, which is exactly what the convention forbids.
(c) 8 $p \to q$ , TAUT 7. The two formulas are equivalent (each is false exactly at $p = \mathrm{T}$ , $q = \mathrm{F}$ ), and the step is a rearrangement a written proof makes without comment.

Marking scheme. (10 points)

3: (a) the TAUT derivation, with the row check.
2: (a) the primitive derivation.
3: (b) the primitive one, because the TAUT line hides the argument’s only idea.
2: (c) the TAUT line, with why the convention allows it.

Exercise (B5: Consistent or not)

Decide whether each list is consistent. Justify “consistent” by a row and the result that makes it a proof; justify “inconsistent” by a derivation of $\bot$ , or by a search and the result that makes it a proof.

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

Solution.

(a) Inconsistent:
1 $p \to q$
2 $q \to r$
3 $p$
4 $\neg r$
5 $q$ $\mathrm{{{\to}}E}$ 1, 3
6 $r$ $\mathrm{{{\to}}E}$ 2, 5
7 $\bot$ $\mathrm{{\neg}E}$ 6, 4
(b) Inconsistent. A search closes: $p \leftrightarrow q$ gives $p, q$ or $\neg p, \neg q$ ; under the first, $\neg p \vee \neg q$ closes both ways; under the second, $p \vee q$ closes both ways. So the list is unsatisfiable (Proposition 4.6.1), hence inconsistent, by Theorem 4.8.4 (“Consistent and satisfiable coincide”).
(c) Consistent. The row with $p$ , $q$ , $r$ all false makes all three members true (false hypotheses), so the list is satisfiable, hence consistent (Section 4.7, by Theorem 4.7.2).

Marking scheme. (10 points)

3: (a) the verdict (1) and the derivation of $\bot$ (2).
4: (b) the verdict (1) and the closed search with the results that make it a proof (3).
3: (c) the verdict (1) and the row with the theorem it rests on (2).

C. Going deeper

Exercise (C1: The remaining cases)

Write out in full the disjunction case and the biconditional case of the proof of Lemma 4.8.2, in the style of the implication case.

Solution. Throughout, $\Sigma$ is $p_1^{v}, \dots, p_n^{v}$ , and the induction hypotheses are $\Sigma \vdash \alpha^{v}$ and $\Sigma \vdash \beta^{v}$ . “Chaining” is Lemma 2.3.3 (c).

Disjunction, $\varphi = \alpha \vee \beta$ . By Definition 4.4.2, $v(\alpha \vee \beta) = \mathrm{F}$ exactly when $v(\alpha) = v(\beta) = \mathrm{F}$ .

Case $v(\alpha) = \mathrm{T}$ . Then $\varphi^{v} = \alpha \vee \beta$ and $\alpha^{v} = \alpha$ . Chaining $\Sigma \vdash \alpha$ with $(\vee 1)$ , $\alpha \vdash \alpha \vee \beta$ , gives $\Sigma \vdash \alpha \vee \beta$ .
Case $v(\alpha) = \mathrm{F}$ , $v(\beta) = \mathrm{T}$ . Then $\varphi^{v} = \alpha \vee \beta$ and $\beta^{v} = \beta$ . Chaining $\Sigma \vdash \beta$ with $(\vee 2)$ gives $\Sigma \vdash \alpha \vee \beta$ .
Case $v(\alpha) = v(\beta) = \mathrm{F}$ . Then $\varphi^{v} = \neg(\alpha \vee \beta)$ , $\alpha^{v} = \neg\alpha$ and $\beta^{v} = \neg\beta$ . Chaining both hypotheses with $(\vee 3)$ , $\neg\alpha, \neg\beta \vdash \neg(\alpha \vee \beta)$ , gives $\Sigma \vdash \neg(\alpha \vee \beta)$ .

Biconditional, $\varphi = \alpha \leftrightarrow \beta$ . By Definition 4.4.2, $v(\alpha \leftrightarrow \beta) = \mathrm{T}$ exactly when $v(\alpha) = v(\beta)$ . Each case uses both hypotheses.

Case T, T. $\varphi^{v} = \alpha \leftrightarrow \beta$ ; chain $\Sigma \vdash \alpha$ , $\Sigma \vdash \beta$ with $({\leftrightarrow}1)$ .
Case F, F. $\varphi^{v} = \alpha \leftrightarrow \beta$ ; chain $\Sigma \vdash \neg\alpha$ , $\Sigma \vdash \neg\beta$ with $({\leftrightarrow}2)$ .
Case T, F. $\varphi^{v} = \neg(\alpha \leftrightarrow \beta)$ ; chain $\Sigma \vdash \alpha$ , $\Sigma \vdash \neg\beta$ with $({\leftrightarrow}3)$ .
Case F, T. $\varphi^{v} = \neg(\alpha \leftrightarrow \beta)$ ; chain $\Sigma \vdash \neg\alpha$ , $\Sigma \vdash \beta$ with $({\leftrightarrow}4)$ .

The cases cover all four pairs of values, so in each the property holds for $\varphi$ .

Marking scheme. (10 points)

4: the $\vee$ case: the three value cases, each with the right sequent of Lemma 4.8.1 and only the hypotheses its premises need.
4: the $\leftrightarrow$ case: the four value cases, each with the right sequent and both hypotheses.
1: names chaining (Lemma 2.3.3 (c)) as the step that combines the hypotheses with the sequent.
1: says that the cases cover every pair of values.

Fatal errors (0 for the step): using a sequent whose premises are not the signed parts $\alpha^{v}$ , $\beta^{v}$ of that case.

Exercise (C2: Exit check: completeness)

Close the section first, and write from memory.

(a) Prove Lemma 4.8.3: if $\Delta, p \vdash \psi$ and $\Delta, \neg p \vdash \psi$ , then $\Delta \vdash \psi$ .
(b) Prove Step 3 of the proof of Theorem 4.8.4 in full: from the Claim of Step 2, for every valuation $v$ , $\Gamma, p_1^{v}, \dots, p_n^{v} \vdash \psi$ , deduce $\Gamma \vdash \psi$ . State the statement you prove by induction, and say which principle of induction you use.

Solution (Hint 1). For (a): excluded middle and proof by cases. For (b): remove the signed atoms from the end of the list, one at a time.

Solution (Hint 2). For (b): let $S(j)$ say “for every valuation $v$ , $\Gamma, p_1^{v}, \dots, p_j^{v} \vdash \psi$ ”, and show that $S(j)$ implies $S(j - 1)$ for $1 \le j \le n$ .

Solution. (a) Let $D$ derive $\psi$ from premises in $\Delta, p$ , and $E$ from premises in $\Delta, \neg p$ . Write, as premises, those of $D$ and $E$ that lie in $\Delta$ ; then $p \vee \neg p$ by $\mathrm{LEM}$ (Proposition 2.5.3, a derived rule with no premises); then a box opening with $p$ containing the non-premise lines of $D$ , in which citations of the premise $p$ now cite the assumption and citations of premises in $\Delta$ cite the premise lines; then a box opening with $\neg p$ , built from $E$ in the same way; then $\psi$ by $\mathrm{\vee E}$ , citing the line $p \vee \neg p$ and the two boxes. (If $D$ or $E$ ends on a premise, its box is the assumption alone when that premise is the assumption’s formula, and otherwise the assumption followed by $\psi$ by $\mathrm{R}$ .) Every copied line keeps its boxes, now inside the new box, and cites lines still available to it. The last line of each box is $\psi$ , as a line of that box itself, because the last line of $D$ or $E$ lay in no box. The two boxes and the $\mathrm{LEM}$ line lie in no box, so they are available at the final line. So the result is a derivation of $\psi$ from premises in $\Delta$ , and $\Delta \vdash \psi$ .

(b) For $0 \le j \le n$ , let $S(j)$ be: for every valuation $v$ , $\Gamma, p_1^{v}, \dots, p_j^{v} \vdash \psi$ . The Claim of Step 2 is $S(n)$ .

The step. Let $1 \le j \le n$ and assume $S(j)$ . Let $v$ be any valuation, and let $v^{+}$ , $v^{-}$ agree with $v$ except that $v^{+}(p_j) = \mathrm{T}$ and $v^{-}(p_j) = \mathrm{F}$ . Since the $p_i$ are distinct, both agree with $v$ on $p_1, \dots, p_{j-1}$ . By $S(j)$ for $v^{+}$ and for $v^{-}$ , with $\Delta \mathrel{:=} \Gamma, p_1^{v}, \dots, p_{j-1}^{v}$ : $\Delta, p_j \vdash \psi$ and $\Delta, \neg p_j \vdash \psi$ . By (a), $\Delta \vdash \psi$ . As $v$ was arbitrary, $S(j - 1)$ holds.

The induction. We use Axiom 4.2.1 on $m \in \mathbb{N}$ with the statement $T(m)$ : “if $m \le n$ , then $S(n - m)$ ”. $T(0)$ is $S(n)$ . If $T(m)$ holds and $m + 1 \le n$ , then $S(n - m)$ holds and $j = n - m$ lies between $1$ and $n$ , so the step gives $S(n - m - 1)$ , which is $T(m + 1)$ . Hence $T(n)$ , which is $S(0)$ : for every valuation, $\Gamma \vdash \psi$ . Valuations exist, so $\Gamma \vdash \psi$ .

(Inducting downwards on $j$ , or on the number of atoms removed, is the same argument; either earns full marks.)

Marking scheme. (10 points)

3: (a) builds one derivation from the two given ones with premises in $\Delta$ (for instance by pasting them into the two boxes of a $\mathrm{\vee E}$ on $p \vee \neg p$ , or by an $\mathrm{RAA}$ box on $\neg\psi$ ), with each premise $p$ or $\neg p$ replaced by an available line, and says why every citation is still available.
1: (a) names the classical step ( $\mathrm{LEM}$ , Proposition 2.5.3, or $\mathrm{RAA}$ ).
3: (b) sets up an induction on the number of atoms removed (or downward on $j$ ) with a statement quantified over every valuation, and names the induction principle.
2: (b) in the step, applies the hypothesis to both valuations that differ at $p_j$ , and notes that they agree with $v$ on the other atoms.
1: (b) concludes $\Gamma \vdash \psi$ from $S(0)$ .

Fatal errors (0 for the step): splitting on an atom using the Claim for a single valuation only; an induction statement that fixes $v$ before the induction, so that the two valuations of the step are not covered by the hypothesis.

Exercise (C3: Exit check: deciding sequents)

For each sequent, decide whether it holds. If it does, justify this by a derivation, or by a truth table and the theorem that turns the table into a derivation; if it does not, give a refuting row and say which theorem turns the row into a proof that no derivation exists.

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

Solution. (a) Derivable. The goal is an implication: a box on $p$ , with the goal $q \vee r$ ; the premise is a disjunction, used by $\mathrm{\vee E}$ inside the box; in each case $\mathrm{{\to}E}$ with $p$ gives one side, and $\mathrm{\vee I}$ gives the goal.

(p \to q) \vee (p \to r)

p

asm, for

\mathrm{{{\to}}I}

p \to q

asm, for

\mathrm{{\vee}E}

q

\mathrm{{{\to}}E}

3, 2

q \vee r

\mathrm{{\vee}I}

p \to r

asm, for

\mathrm{{\vee}E}

r

\mathrm{{{\to}}E}

6, 2

q \vee r

\mathrm{{\vee}I}

q \vee r

\mathrm{{\vee}E}

1, 3–5, 6–8

p \to (q \vee r)

\mathrm{{{\to}}I}

2–9

(b) Not derivable. In the row $p = \mathrm{T}$ , $q = \mathrm{F}$ , $r = \mathrm{F}$ , the premise is true ( $p \to q$ is F, so $(p \to q) \to r$ is T) and the conclusion $p \to r$ is F. By Corollary 4.7.3, $(p \to q) \to r \nvdash p \to r$ .

(c) Not derivable. In the row $p = \mathrm{T}$ , $q = \mathrm{T}$ , $r = \mathrm{F}$ (the value of $q$ does not matter), the premise is true because $p$ is, and the conclusion is false because $r$ is. By Corollary 4.7.3, the sequent fails.

(d) Derivable. Split the premise by $\mathrm{\wedge E}$ , then use $p \vee q$ by $\mathrm{\vee E}$ : the case $p$ clashes with $\neg p$ and closes by $\mathrm{\bot E}$ ; the case $q$ gives the goal by $\mathrm{\vee I}$ .

(p \vee q) \wedge \neg p

p \vee q

\mathrm{{\wedge}E}

\neg p

\mathrm{{\wedge}E}

p

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

4, 3

q \vee r

\mathrm{{\bot}E}

q

asm, for

\mathrm{{\vee}E}

q \vee r

\mathrm{{\vee}I}

q \vee r

\mathrm{{\vee}E}

2, 4–6, 7–8

Neither derivation uses $\mathrm{RAA}$ . As the problem allows, (a) and (d) may instead be justified by a table (or backwards from F) showing the entailment, followed by Theorem 4.8.4.

Marking scheme. (10 points; 2.5 per sequent)

1 per sequent: the correct verdict.
1.5 per sequent: its justification: a derivation in which every line is justified and every citation available, or a table check with Theorem 4.8.4; or a row that makes every premise true and the conclusion false, checked, with Corollary 4.7.3 (or Theorem 4.7.2) cited.

Fatal errors (0 for the sequent’s justification): a “refuting row” that makes some premise false; a derivation citing a line that is not available.

Exercise (C4: Challenge: Strike out ∨I)

Strike $\mathrm{\vee I}$ from the primitive rules.

(a) Which sequents of Lemma 4.8.1 lose the derivations given in its proof (the table of the fold “The fifteen derivations”), and which step of the proof of Theorem 4.8.4 also uses $\mathrm{\vee I}$ , through a result of Chapter 2?
(b) Read $\vee$ as $\wedge$ : a valuation now makes $\varphi \vee \psi$ true exactly when it makes both parts true; every other clause stays. Show that every remaining primitive rule is sound for this reading.
(c) Deduce that neither $p \vdash p \vee q$ nor $\vdash p \vee \neg p$ is derivable without $\mathrm{\vee I}$ (and without derived rules derived with it), although both are valid: the shorter list of rules is sound but not complete.

Solution.

(a) $(\vee 1)$ and $(\vee 2)$ are $\mathrm{\vee I}$ itself; $(\wedge 2)$ and $(\wedge 3)$ are derived by $\mathrm{\vee I}$ and then Proposition 2.5.5 (c). And Lemma 4.8.3 uses Proposition 2.5.3, whose derivation in Section 2.5 uses $\mathrm{\vee I}$ twice; that is Step 3 of the proof, where Lemma 4.8.3 removes the signed atoms.
(b) Only the cases $\mathrm{\vee I}$ and $\mathrm{\vee E}$ of the proof of Theorem 4.7.2 use the clause for $\vee$ , and $\mathrm{\vee I}$ is gone. $\mathrm{\vee E}$ : if a valuation makes $\Gamma_k$ true, it makes $\varphi \vee \psi$ true, hence, in the new reading, both $\varphi$ and $\psi$ ; by the first box it makes $\chi$ true. Every other case is unchanged.
(c) The valuation with $p$ true and $q$ false makes $p$ true and, in the new reading, $p \vee q$ false; every valuation makes $p \vee \neg p$ false in the new reading, since $p$ and $\neg p$ are never both true. By (b), and Step 1 of the proof of Theorem 4.7.2 (a derived rule derived without $\mathrm{\vee I}$ expands, by that step, into a pasted derivation in the remaining primitive rules), neither sequent has a derivation without $\mathrm{\vee I}$ and the derived rules that use it, such as Proposition 2.5.3. Both are valid in the ordinary tables.

Marking scheme. (10 points)

3: (a), all four sequents and the excluded-middle step.
4: (b), with the $\mathrm{\vee E}$ case argued and the other cases said to be unchanged.
3: (c), both valuations and the conclusion, with Step 1’s restriction to derived rules derived without $\mathrm{\vee I}$ .

Fatal errors (0 for the step): in (c), using the ordinary tables.

Exercise (C5: Challenge: From a closed tree to a derivation)

Let a search tree (Section 4.6) for $\Gamma, \neg\psi$ have every branch closed. For a node $X$ , the path list of $X$ is the list of formulas on the path from the root down to $X$ , $X$ included.

(a) Prove, by induction on the number of nodes below $X$ , that if every branch through $X$ is closed, then $\Delta \vdash \bot$ , where $\Delta$ is the path list of $X$ . Treat a closed leaf and each rule of the table of search rules, naming the derivable sequents you use.
(b) Deduce $\Gamma \vdash \psi$ .
(c) Explain why (a), (b) and Proposition 4.6.1 give a second proof of Theorem 4.8.4, and where it uses $\mathrm{RAA}$ or $\mathrm{LEM}$ .

Solution (Hint 1). A one-way rule: derive the added formulas from the used one, then chain (Lemma 2.3.3). A two-way rule: join the two derivations of $\bot$ .

Solution (Hint 2). For $\varphi \to \psi$ , split as $\neg\varphi$ or $\psi$ : with $\Delta$ the path list of $X$ , from $\Delta, \neg\varphi \vdash \bot$ get $\Delta \vdash \varphi$ by $\mathrm{RAA}$ .

Solution.

(a) We use Theorem 4.2.2 on the number of nodes below $X$ . Write $\Delta$ for the path list of $X$ .
A closed leaf. $\Delta$ holds $\varphi$ and $\neg\varphi$ (one $\mathrm{\neg E}$ line) or $\bot$ (the premise itself): $\Delta \vdash \bot$ .

An inner node. Its children were added by the rule of some $\chi$ in $\Delta$ . Every branch through each child is closed, and each child has fewer nodes below it, so the hypothesis gives $\Delta, \alpha_1 \vdash \bot$ (or $\Delta, \alpha_1, \alpha_2 \vdash \bot$ ) for the formulas $\alpha$ that each child adds.

One-way rules. It suffices to show $\Delta \vdash \alpha$ for each added $\alpha$ , and then chain (Lemma 2.3.3 (c), after weakening). $\varphi \wedge \psi$ : $\mathrm{\wedge E}$ . $\neg(\varphi \vee \psi) \vdash \neg\varphi$ : a $\mathrm{\neg I}$ box on $\varphi$ , $\mathrm{\vee I}$ , $\mathrm{\neg E}$ ; likewise $\neg\psi$ . $\neg(\varphi \to \psi) \vdash \varphi$ : an $\mathrm{RAA}$ box on $\neg\varphi$ , in which Proposition 2.1.2 gives $\varphi \to \psi$ , then $\mathrm{\neg E}$ . $\neg(\varphi \to \psi) \vdash \neg\psi$ : a $\mathrm{\neg I}$ box on $\psi$ , in which an inner box gives $\varphi \to \psi$ by $\mathrm{R}$ and $\mathrm{{\to}I}$ , then $\mathrm{\neg E}$ . $\neg\neg\varphi \vdash \varphi$ : Proposition 2.5.1.

Two-way rules. $\varphi \vee \psi$ : $\mathrm{\vee E}$ on the line $\varphi \vee \psi$ , with the two derivations of $\bot$ pasted into the boxes as in the proof of Lemma 4.8.3. $\neg(\varphi \wedge \psi)$ : from $\Delta, \neg\varphi \vdash \bot$ , $\Delta \vdash \varphi$ by $\mathrm{RAA}$ ; likewise $\Delta \vdash \psi$ ; then $\mathrm{\wedge I}$ , and $\mathrm{\neg E}$ with $\neg(\varphi \wedge \psi)$ . $\varphi \to \psi$ : $\Delta \vdash \varphi$ by $\mathrm{RAA}$ from the first child; $\mathrm{{\to}E}$ gives $\psi$ ; cut with $\Delta, \psi \vdash \bot$ . $\varphi \leftrightarrow \psi$ : from $\Delta, \varphi, \psi \vdash \bot$ and $\Delta, \varphi \vdash \psi$ (by $\mathrm{{\leftrightarrow}E}$ ), cut gives $\Delta, \varphi \vdash \bot$ ; from $\Delta, \neg\varphi, \neg\psi \vdash \bot$ and $\Delta, \neg\varphi \vdash \neg\psi$ (a $\mathrm{\neg I}$ box on $\psi$ : $\varphi$ by $\mathrm{{\leftrightarrow}E}$ , clash), cut gives $\Delta, \neg\varphi \vdash \bot$ ; join the two by Lemma 4.8.3, which holds for any formula in place of the atom (the remark after its proof). $\neg(\varphi \leftrightarrow \psi)$ : $\Delta, \varphi \vdash \neg\psi$ (a $\mathrm{\neg I}$ box on $\psi$ : $\varphi \leftrightarrow \psi$ by $\mathrm{{\leftrightarrow}I}$ with two two-line boxes, each closed by $\mathrm{R}$ , then the clash with $\neg(\varphi \leftrightarrow \psi)$ ), so $\Delta, \varphi \vdash \bot$ by cut with the first child; $\Delta, \neg\varphi \vdash \psi$ (an $\mathrm{RAA}$ box on $\neg\psi$ : $\varphi \leftrightarrow \psi$ by $\mathrm{{\leftrightarrow}I}$ , each box closing by a clash and $\mathrm{\bot E}$ , then the clash with $\neg(\varphi \leftrightarrow \psi)$ ), so $\Delta, \neg\varphi \vdash \bot$ by cut with the second child; join by Lemma 4.8.3.
(b) At the root, $\Gamma, \neg\psi \vdash \bot$ ; an $\mathrm{RAA}$ box on $\neg\psi$ holding that derivation gives $\Gamma \vdash \psi$ (Proposition 3.2.2 (b)).
(c) If $\Gamma \models \psi$ , a search tree for $\Gamma, \neg\psi$ can be continued until every branch is closed or finished (Proposition 4.6.1 (a)), and it has no open finished branch, since by (c) of that proposition its row would refute $\Gamma \models \psi$ . So every branch is closed, and (a), (b) give $\Gamma \vdash \psi$ . $\mathrm{RAA}$ enters in the cases $\neg(\varphi \to \psi)$ , $\neg\neg\varphi$ , $\neg(\varphi \wedge \psi)$ , $\varphi \to \psi$ , $\neg(\varphi \leftrightarrow \psi)$ and at the root; $\mathrm{LEM}$ in the two biconditional cases. The derivation follows the tree, so it is often far shorter than the $2^n$ rows of the first proof.

Marking scheme. (10 points)

1: the closed leaf.
2: the four one-way cases.
5: the five two-way cases (1 each).
1: (b).
1: (c), with the classical steps located.

Fatal errors (0 for the step): treating a split by assuming one side only.

R. Review

Exercise (R1)

Find a derivation of $p \vee q, \ \neg(p \wedge r), \ r \vdash q$ .

Solution. The method of Section 3.1 (Example (Proof by cases, found by the method) shows it on a proof by cases). The goal $q$ is an atom, so no introduction rule applies; the premise $p \vee q$ is a disjunction, so we use it by $\mathrm{\vee E}$ , with the goal $q$ in both boxes. The case $q$ is the goal. In the case $p$ , nothing gives $q$ directly, so we look for a clash: $p$ and the premise $r$ build $p \wedge r$ by $\mathrm{\wedge I}$ , which clashes with $\neg(p \wedge r)$ , and $\mathrm{\bot E}$ closes the impossible case (Example (Manufacturing the other half of a clash)).

p \vee q

\neg (p \wedge r)

r

p

asm, for

\mathrm{{\vee}E}

p \wedge r

\mathrm{{\wedge}I}

4, 3

\bot

\mathrm{{\neg}E}

5, 2

q

\mathrm{{\bot}E}

q

asm, for

\mathrm{{\vee}E}

q

\mathrm{{\vee}E}

1, 4–7, 8–8

The second box is its assumption alone, which is already the goal. No $\mathrm{RAA}$ is used.

Exercise (R2)

Let $m$ and $n$ be integers, and consider the argument: “ $m + n$ is even only if $m$ and $n$ are both even or both odd. $m$ is even and $n$ is odd. Therefore $m + n$ is not even.” Translate it into a sequent, using atoms $e$ : “ $m + n$ is even”, $a$ : “ $m$ is even”, $b$ : “ $n$ is even”, and decide whether the premises entail the conclusion.

Solution. “ $P$ only if $Q$ ” is $P \to Q$ (Section 1.1, and Exercise (C1: “Only if” and “unless”, used later)). “Both odd” is $\neg a \wedge \neg b$ , since an integer is odd exactly when it is not even. So the sequent is $e \to ((a \wedge b) \vee (\neg a \wedge \neg b)), \ \ a \wedge \neg b \ \models \ \neg e .$ Work backwards from F. A refuting row needs $\neg e$ false, so $e = \mathrm{T}$ , and the second premise true, so $a = \mathrm{T}$ , $b = \mathrm{F}$ . In that row $a \wedge b$ and $\neg a \wedge \neg b$ are both F, so the first premise is $\mathrm{T} \to \mathrm{F}$ , which is F. So no row makes both premises true and the conclusion false: the entailment holds. By Theorem 4.8.4, the sequent is also derivable. (The eight-row table gives the same answer; working backwards found the only candidate row at once.)

Exercise (R3)

Is $(p \wedge (q \vee r)) \to ((p \wedge q) \vee r)$ a tautology? Is it derivable without $\mathrm{RAA}$ ?

Solution. A tautology. Work backwards from F (Section 4.4). The formula is false only if $p \wedge (q \vee r)$ is true and $(p \wedge q) \vee r$ is false. The second needs $r$ false and $p \wedge q$ false; the first needs $p$ true and $q \vee r$ true, so with $r$ false, $q$ true. But then $p \wedge q$ is true. No row makes the formula false, so it is a tautology (Definition 4.5.1).

Derivable without $\mathrm{RAA}$ . Completeness (Theorem 4.8.4) says it is derivable, but not how, and its proof uses $\mathrm{LEM}$ in Lemma 4.8.3, so it does not answer the second question. A search does: the goal is an implication, so a box on $p \wedge (q \vee r)$ ; split it by $\mathrm{\wedge E}$ and use $q \vee r$ by $\mathrm{\vee E}$ .

p \wedge (q \vee r)

asm, for

\mathrm{{{\to}}I}

p

\mathrm{{\wedge}E}

q \vee r

\mathrm{{\wedge}E}

q

asm, for

\mathrm{{\vee}E}

p \wedge q

\mathrm{{\wedge}I}

2, 4

(p \wedge q) \vee r

\mathrm{{\vee}I}

r

asm, for

\mathrm{{\vee}E}

(p \wedge q) \vee r

\mathrm{{\vee}I}

(p \wedge q) \vee r

\mathrm{{\vee}E}

3, 4–6, 7–8

(p \wedge (q \vee r)) \to ((p \wedge q) \vee r)

\mathrm{{{\to}}I}

1–9

No $\mathrm{RAA}$ is used: the boxes close by $\mathrm{\vee E}$ and $\mathrm{{\to}I}$ . The tools: truth values (Definition 4.4.2) for the first question, the search of Chapter 3 for the second. The look-alike tool, completeness, answers only “derivable with all the rules”.