6.3 Finding First-Order Derivations

Chapter 5 added one step to the search method in each rule section, and Section 6.2 added laws. This section puts the steps into one method, puts in order the moves that do most of the work with quantifiers and names a third, admits the propositional step TAUT into derivations with quantifiers, and runs the four kinds of task of Section 3.2 again. The new difficulty is names: which term to instantiate at, when to open a box for a witness, and which names a line may mention when a box closes.

Remark (Looking back). Section 3.1 assembled the search method for the connectives, and Section 3.2 sorted the tasks it serves. Here both return with flags and witnesses. Backward from the goal and forward from the premises is unchanged; what is new is that a box may carry a name, and a closing line must not mention it.

6.3.1. The search method, extended

Section 3.1 put the moves for the connectives in order. Each of Sections 5.3–5.7 added a step. Here is the method with all of them.

Algorithm. Searching for a derivation of $\Gamma \vdash \varphi$ in predicate logic.

Set up. Write the premises $\Gamma$ at the top and $\varphi$ at the bottom, with one gap between. Translate any definition in words into a formula first, as in Example (Five definitions, translated).
Goal-directed step. Take the current goal’s main symbol and set up its introduction rule:
- $\wedge$ , $\to$ , $\neg$ , $\leftrightarrow$ : as in Section 3.1;
- $\forall x\, \psi$ : open a flagged box with a fresh name $x_0$ ; the new goal, the box’s last line, is $\psi[x_0/x]$ (Section 5.4). For $\forall x \in A\; \psi$ , the box opens with the assumption $x_0 \in A$ ;
- $\vee$ : postpone, as in Section 3.1;
- $\exists x\, \psi$ : postpone; work on the premises until an available line shows a term $t$ with $\psi[t/x]$ , then use $\mathrm{\exists I}$ (Section 5.5). For $\exists x \in A\; \psi$ , the line $t \in A$ is needed too.
Repeat while the goal is $\wedge$ , $\to$ , $\neg$ , $\leftrightarrow$ , or $\forall$ .
Premise-directed step. Take the main symbol of a resource and apply its elimination rule:
- $\wedge$ , $\to$ , $\vee$ , $\leftrightarrow$ , and the derived rules: as in Section 3.1;
- $\exists x\, \psi$ : open the $\mathrm{\exists E}$ box early, as soon as the line is available, with a fresh witness $x_0$ , and make its last line the current goal, which must not mention $x_0$ (Section 5.6). An early box lets the witness serve the goals that come later;
- $\forall x\, \psi$ : do not instantiate blindly; instantiate at the term that the goal, or another resource, mentions (Section 5.3). For $\forall x \in A\; \psi$ , the line $t \in A$ is needed too;
- an equation $t_1 = t_2$ : use $\mathrm{{=}E}$ with a $\varphi$ chosen so that one substitution turns an available line into the goal, turning the equation round first if needed (Section 5.7).
Clash. As in Section 3.1: for the goal $\bot$ , find or manufacture a pair $\chi$ , $\neg\chi$ ; an impossible case closes itself by $\mathrm{\bot E}$ .
Stuck. As in Section 3.1: $\mathrm{RAA}$ on the current goal, or $\mathrm{LEM}$ on a well-chosen statement.

When no gap is left, number the lines and check the derivation as Definition 1.4.2, extended in Section 5.4, says: every citation is available, and every side condition holds ( $t$ free for $x$ at $\mathrm{\forall E}$ and $\mathrm{\exists I}$ , bounded or not; $t_1$ and $t_2$ free for $x$ at $\mathrm{{=}E}$ ; a fresh name at each line that closes a flagged box).

Two of the new steps deserve a word on their place in the order. The goal step for $\forall$ is safe in the same way as the goal steps for $\to$ and $\neg$ (Section 3.1): if $\forall x\, \psi$ is derivable at all, then so is $\psi[x_0/x]$ for a fresh $x_0$ , by one more $\mathrm{\forall E}$ ; so opening the box loses nothing. The goal step for $\exists$ is unsafe in the same way as the one for $\vee$ : a witness chosen too early may be the wrong one, as in Example (Derivations with existential introduction), where “take $y = c$ ” stalled. That is why $\exists$ is postponed and the $\mathrm{\exists E}$ boxes of the premises are opened early: the witnesses they supply are often the terms the postponed goal is waiting for, as $N_0$ was in the limit derivation of Section 6.1.

6.3.2. Three moves for quantifiers

Most first-order searches turn on three moves. The first two carry the names Chapter 5 gave them; what is new here is their order, which the method above already follows.

Name the witness early (Section 5.6). When an $\exists$ line is among the resources, open its box at once, with a fresh witness, and make the box’s last line the current goal. The witness costs nothing to name, and it is often the very term that a $\forall$ line or the goal is waiting for.

Instantiate at the term you need (Section 5.3), and so not before that term is known. A $\forall$ line can be instantiated at any term at all, which is exactly why instantiating it before the goal or a witness names the term is a blind choice. Wait for the witnesses, then instantiate at them.

The propositional core. Once the boxes are open and the $\forall$ lines are instantiated, what is left is often a step that holds for propositional reasons alone. The subsection “The propositional core” below names this move and gives it a one-line step.

Two pairs of steps recur: $\mathrm{\forall E}$ followed by $\mathrm{{\to}E}$ , which applies a general law at one point, and $\mathrm{\exists E}$ followed, inside its box, by $\mathrm{\exists I}$ with a term built from the names in hand.

The next move, read off the goal and the lines in hand:

$Diagram. Labels: no, the current goal\and the available lines, goal begins with forall ,\\wedge , to , neg or leftrightarrow ?, an exists line available,\box not yet opened?, a forall line not yet\instantiated at a term\the goal or a witness names?, goal exists x\, psi , and a line\showing psi [t/x]?, stuck: test the subgoal\by a counter-reading;\then RAA or LEM, set up its introduction rule\\(for forall : a fresh flag), open its existsE box now;\fresh witness, same goal, forallE at that term, existsI at t$

The last edge reads “no”, not “impossible”: the chart is a guide to the next move, and it makes no claim that every derivable sequent is found by following it. It leaves out the premise-directed connective steps, the clash and the propositional core (TAUT, below); for those, follow the method above.

Example (A search that waits for its witnesses)

Show that $\forall x\, (P(x) \to \exists y\, R(x, y)), \ \forall x\, \forall y\, (R(x, y) \to Q(y)), \ \exists x\, P(x) \vdash \exists y\, Q(y)$ .

Idea. The goal is an $\exists$ : postpone it. Premise 3 is an $\exists$ : open its box now, with witness $x_0$ (left). Premise 1 is a $\forall$ , and $x_0$ is now the term it needs: $\mathrm{\forall E}$ then $\mathrm{{\to}E}$ gives an $\exists y$ line. Open that box at once, with witness $y_0$ (right). Premise 2 needs two terms, and both are in hand: $x_0$ , then $y_0$ . The postponed goal gets its witness, $y_0$ .

In the left snapshot the gap’s goal is still $\exists y\, Q(y)$ : an $\mathrm{\exists E}$ box keeps the goal it was opened for, and its assumption, line 4, says “ $P(x_0)$ ” and nothing more. In the right snapshot the same goal has moved one box further in, and line 7 is now the only line that asserts $R$ of particular terms.

\forall x\, (P(x) \to \exists y\, R(x, y))

\forall x\, \forall y\, (R(x, y) \to Q(y))

\exists x\, P(x)

x_0

P(x_0)

asm, for

\mathrm{{\exists}E}

\vdots

\exists y\, Q(y)

\exists y\, Q(y)

\forall x\, (P(x) \to \exists y\, R(x, y))

\forall x\, \forall y\, (R(x, y) \to Q(y))

\exists x\, P(x)

x_0

P(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to \exists y\, R(x_0, y)

\mathrm{{\forall}E}

\exists y\, R(x_0, y)

\mathrm{{{\to}}E}

5, 4

y_0

R(x_0, y_0)

asm, for

\mathrm{{\exists}E}

\vdots

\exists y\, Q(y)

\exists y\, Q(y)

\exists y\, Q(y)

Solution.

\forall x\, (P(x) \to \exists y\, R(x, y))

\forall x\, \forall y\, (R(x, y) \to Q(y))

\exists x\, P(x)

x_0

P(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to \exists y\, R(x_0, y)

\mathrm{{\forall}E}

\exists y\, R(x_0, y)

\mathrm{{{\to}}E}

5, 4

y_0

R(x_0, y_0)

asm, for

\mathrm{{\exists}E}

\forall y\, (R(x_0, y) \to Q(y))

\mathrm{{\forall}E}

R(x_0, y_0) \to Q(y_0)

\mathrm{{\forall}E}

Q(y_0)

\mathrm{{{\to}}E}

9, 7

\exists y\, Q(y)

\mathrm{{\exists}I}

\exists y\, Q(y)

\mathrm{{\exists}E}

6, 7–11

\exists y\, Q(y)

\mathrm{{\exists}E}

3, 4–12

At line 12, $y_0$ is not in line 12, in line 6, in the premises, or in the open assumption on line 4. At line 13, $x_0$ is not in line 13, in line 3, or in the premises, and no assumption is open.

Read over $\mathbb{Z}$ , with $P(x)$ as “ $x > 0$ ”, $R(x, y)$ as “ $y = 2x + 1$ ” and $Q(y)$ as “ $y$ is odd”: every positive integer has a $2x + 1$ ; every number of the form $2x + 1$ is odd; some integer is positive; so some integer is odd.

Compare a search that starts with premise 1, before any witness is named. It must instantiate at some term, a variable or a constant that nothing mentions, say $c$ ; the line $P(c) \to \exists y\, R(c, y)$ then waits for $P(c)$ , which no premise gives. The box of premise 3 supplies the term that makes premise 1 usable.

Quick check. Why is line 8 an instance at $x_0$ , and not at some other term?

Solution. Line 7, the only line that asserts $R$ of particular terms, mentions $x_0$ and $y_0$ . Premise 2 is useful only at the terms that line names. This is the move “instantiate at the term you need”: the terms were known only once the witnesses were named.

6.3.3. Steps that are right for propositional reasons

Inside the boxes of a first-order derivation, many steps are propositional: $\mathrm{\wedge E}$ , $\mathrm{{\to}E}$ , a contrapositive, a case split. Section 4.8 let a propositional derivation take such steps in one line, as TAUT. With quantifiers the step must not look inside a quantifier, and the next definition says exactly what it may look at.

Definition 6.3.1 (Propositional Skeleton)

Call a first-order formula prime if it is atomic and not $\bot$ , or begins with a quantifier, bounded or not. Assign to each prime formula a propositional atom, the same atom to two prime formulas exactly when one can be turned into the other by finitely many renamings of bound variables (Section 5.2), in either direction; this is an equivalence relation, so the assignment is well defined. The propositional skeleton $\mathrm{sk}(\varphi)$ of a formula $\varphi$ is defined by recursion: $\mathrm{sk}(\bot) = \bot$ ; $\mathrm{sk}(\pi)$ is the atom of $\pi$ for a prime formula $\pi$ ; $\mathrm{sk}(\neg\varphi) = \neg\,\mathrm{sk}(\varphi)$ ; and $\mathrm{sk}(\varphi \circ \psi) = \mathrm{sk}(\varphi) \circ \mathrm{sk}(\psi)$ for each of $\wedge$ , $\vee$ , $\to$ , $\leftrightarrow$ . The formulas of one list take their skeletons from one assignment.

The skeleton keeps the connectives outside every quantifier and hides everything else; this is not the skeleton of a derivation that Section 3.1 reads off the goal, and wherever the two could be confused, the book says “propositional skeleton” for this one. For example, $\mathrm{sk}\bigl( \forall x\, P(x) \to (\exists y\, R(y, c) \vee \neg\forall z\, P(z)) \bigr) = p \to (q \vee \neg p),$ since $\forall x\, P(x)$ and $\forall z\, P(z)$ differ only by renaming and so share the atom $p$ .

Why only renaming? The formulas $\forall x\, (P(x) \wedge Q(x))$ and $\forall x\, P(x) \wedge \forall x\, Q(x)$ are provably equivalent (Proposition 6.2.6 (a)), yet the first is prime and the second is a conjunction of two prime formulas. If provable equivalence were allowed to merge atoms, the skeleton would depend on what has been derived, and a TAUT line could hide a quantifier step inside a table. Renaming is different: whether two formulas differ only by renaming bound variables can be seen by comparing them symbol by symbol, so anyone can compute the skeleton without a derivation. And $\bot$ is kept as itself, not given an atom, so that $\neg\bot$ is a tautology and a cited line $\bot$ entails every skeleton, as $\mathrm{\bot E}$ says it should; an atom would have neither property.

Proposition 6.3.1 (Tautological Steps on the Skeleton)

Let $\Gamma$ be a list of first-order formulas and $\psi$ a formula, with skeletons taken from one assignment. If the skeletons of $\Gamma$ semantically entail $\mathrm{sk}(\psi)$ (Definition 4.5.3), then $\Gamma \vdash \psi$ . If no two different prime formulas occurring outside all quantifiers in $\Gamma$ and $\psi$ share an atom, the derivation uses only the rules of Chapters 1 and 2.

In words: a step that is right for propositional reasons alone is derivable, with the quantified parts carried along untouched.

The proof takes the propositional derivation that completeness provides and puts the prime formulas back in place of their atoms; it is in the fold below.

Second readingThe proof: completeness on the skeleton, then substitution

Proof. Step 1: no two different prime formulas outside all quantifiers share an atom. By Corollary 4.8.5 (completeness, Section 4.8) there is a derivation $D$ of $\mathrm{sk}(\Gamma) \vdash \mathrm{sk}(\psi)$ with the rules of Chapters 1 and 2; its lines are propositional formulas. Replace, in every line of $D$ , each atom of $\mathrm{sk}(\Gamma)$ , $\mathrm{sk}(\psi)$ by the prime formula of $\Gamma$ , $\psi$ to which it was assigned, and any other atom by $\bot$ . This is the substitution of formulas for atoms that Definition 2.3.1 makes for letters, and that Lemma 4.5.3 makes for meaning. Every rule of Chapters 1 and 2 is a schema in formulas, and the replacement commutes with each connective and leaves $\bot$ alone. So each line keeps its rule and its citations, and each box keeps its extent and its assumption; this holds for $\mathrm{RAA}$ , $\mathrm{LEM}$ and $\mathrm{\bot E}$ as for the others. $D$ has no flagged box, so no side condition about names arises. Each premise $\mathrm{sk}(\gamma)$ becomes $\gamma$ , and the last line becomes $\psi$ . So the result is a first-order derivation of $\Gamma \vdash \psi$ (Definition 1.4.2, as Section 5.4 extended it), and it uses only the rules of Chapters 1 and 2. This is the second sentence of the statement.

Step 2: the general case. Choose one prime formula for each atom, and let $\gamma^*$ be $\gamma$ with every prime formula occurring outside all quantifiers (the occurrences the skeleton sees) replaced by the chosen one of its atom. Prime formulas with one atom differ only by renaming. A renaming is a provable equivalence whose closure is derivable (the renaming sentence after Proposition 6.2.4), so Proposition 6.2.4, applied one occurrence and one renaming step at a time (through a letter new to the formula where needed), with the steps chained by Lemma 2.3.3 (c), gives $\gamma \dashv\vdash \gamma^*$ for each formula $\gamma$ of the list, and $\psi \dashv\vdash \psi^*$ . The formulas $\Gamma^*$ and $\psi^*$ have the same skeletons as $\Gamma$ and $\psi$ , and in them no two different prime formulas outside all quantifiers share an atom, so Step 1 gives $\Gamma^* \vdash \psi^*$ . Now Lemma 2.3.3 (Section 2.3) chains $\Gamma \vdash \gamma^*$ for each $\gamma$ , then $\Gamma^* \vdash \psi^*$ , then $\psi^* \vdash \psi$ . Each pasted block’s flags are first renamed to names new to the whole derivation, as “The laws as one line” (Section 6.2) argues. Then no flag of a pasted block occurs in a premise or an open assumption of the derivation it is pasted into, so every $\mathrm{\forall I}$ and $\mathrm{\exists E}$ side condition of the block still holds, and Lemma 2.3.3 (c) holds for these first-order derivations by the same pasting. So $\Gamma \vdash \psi$ .

TAUT on the skeleton. From now on, a line of a derivation may be justified $\mathrm{TAUT}$ , citing available lines, when their skeletons semantically entail its skeleton (Definition 4.5.3), all from one assignment; with no cited lines, when its skeleton is a tautology. This is Definition 4.8.1 of Section 4.8, applied to skeletons. By Proposition 6.3.1 the line abbreviates a block of primitive steps, pasted in with any flags renamed to names new to the whole derivation, as “The laws as one line” (Section 6.2) allows. As in Section 4.8, use TAUT only for a step a written proof would leave unsaid.

These are TAUT steps:

from $\neg(\exists x\, P(x) \wedge Q(c))$ and $Q(c)$ to $\neg\exists x\, P(x)$ , since $\neg(p \wedge q), q \models \neg p$ ;
from $\forall x\, (P(x) \to Q(x)) \to R$ and $\neg R$ to $\neg\forall x\, (P(x) \to Q(x))$ : modus tollens on the skeleton, $p \to r, \neg r \models \neg p$ .

These are not:

from $\forall x\, \forall y\, R(x, y)$ to $\forall y\, \forall x\, R(x, y)$ : the two prime formulas do not differ by renaming, so the skeletons are $p$ and $q$ , and $p \not\models q$ . The step is derivable, by Example (Flagged boxes at work) (c), and that derivation looks inside the quantifiers;
from $\forall x\, P(x)$ to $P(c)$ : the skeletons are $p$ and $q$ ; this is $\mathrm{\forall E}$ ;
$x = x$ : the skeleton is one atom, not a tautology; this is $\mathrm{{=}I}$ .

Quick check. Which are TAUT steps? (a) From $\exists x\, P(x) \wedge \forall y\, Q(y)$ to $\forall y\, Q(y) \wedge \exists x\, P(x)$ . (b) From $\forall x\, (P(x) \wedge Q(x))$ to $\forall x\, P(x)$ . (c) From $\neg\forall x\, P(x)$ to $\exists x\, \neg P(x)$ .

Solution.

(a) Yes: $p \wedge q \models q \wedge p$ . (b) No: the skeletons are two different atoms; the step is Proposition 6.2.6 (a), which looks inside $\forall x$ . (c) No: the skeletons are $\neg p$ and $q$ ; the step is QN (a) of Section 6.2, which needs the quantifier rules and $\mathrm{RAA}$ .

Warning (Not allowed: TAUT).

From $\forall x\, (P(x) \wedge Q(x))$ to $\forall x\, Q(x)$ . Looks inside a quantifier; needs a flagged box.
From $\forall x\, P(x)$ to $P(f(c))$ . An instance, not an entailment of skeletons; needs $\mathrm{\forall E}$ .
From $P(c)$ to $\exists x\, P(x)$ . Needs $\mathrm{\exists I}$ .
From $s = t$ and $P(s)$ to $P(t)$ . The skeleton is $p, q \models r$ , which fails; needs $\mathrm{{=}E}$ .
Citing a line inside a box that has closed. Not available, whatever the table says (Definition 1.4.2).

6.3.4. The propositional core

Many first-order derivations have the same shape. Open the boxes the goal asks for, instantiate every $\forall$ line at the names in play, then finish with a step that is propositional. The quantifiers frame the derivation, and its core is a truth-table fact.

Example (A propositional core inside a flagged box)

Show that $\forall x\, (P(x) \to (Q(x) \vee R(x))), \ \forall x\, \neg Q(x) \vdash \forall x\, (P(x) \to R(x))$ .

Solution.

\forall x\, (P(x) \to (Q(x) \vee R(x)))

\forall x\, \neg Q(x)

x_0

P(x_0) \to (Q(x_0) \vee R(x_0))

\mathrm{{\forall}E}

\neg Q(x_0)

\mathrm{{\forall}E}

P(x_0) \to R(x_0)

\mathrm{TAUT}

3, 4

\forall x\, (P(x) \to R(x))

\mathrm{{\forall}I}

3–5

The skeleton of line 5’s step is $p \to (q \vee r), \neg q \models p \to r$ . At line 6, $x_0$ is not in a premise or in line 6, and no assumption is open.

Read over $\mathbb{Z}$ , with $P(n)$ as “ $n > 1$ ”, $Q(n)$ as “ $n^2 = 2$ ” and $R(n)$ as “ $n > 0$ ”. The first premise says “if $n > 1$ , then $n^2 = 2$ or $n > 0$ ”, true since $n > 1$ gives $n > 0$ ; the second says that no integer squares to $2$ . Both premises are true under this reading, and so is the conclusion, which says that every integer greater than $1$ is positive. The quantifier part of the derivation is two instantiations and one generalization, and its core is propositional.

The order of the steps is the point. TAUT could not have been applied to the premises themselves: their skeletons are two atoms $p$ and $q$ , and the goal’s is a third, $r$ , and $p, q \not\models r$ . Only after the flagged box is open and both premises are instantiated at its flag do the lines show the connectives that the table needs. So the move reads: boxes first, instances at the flag second, and the table last.

Quick check. Write out what line 5 abbreviates, with the rules of Chapters 1 and 2.

Solution. Lines 5–13 below replace the one TAUT line:

\forall x\, (P(x) \to (Q(x) \vee R(x)))

\forall x\, \neg Q(x)

x_0

P(x_0) \to (Q(x_0) \vee R(x_0))

\mathrm{{\forall}E}

\neg Q(x_0)

\mathrm{{\forall}E}

P(x_0)

asm, for

\mathrm{{{\to}}I}

Q(x_0) \vee R(x_0)

\mathrm{{{\to}}E}

3, 5

Q(x_0)

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

7, 4

R(x_0)

\mathrm{{\bot}E}

R(x_0)

asm, for

\mathrm{{\vee}E}

R(x_0)

\mathrm{R}

R(x_0)

\mathrm{{\vee}E}

6, 7–9, 10–11

P(x_0) \to R(x_0)

\mathrm{{{\to}}I}

5–12

\forall x\, (P(x) \to R(x))

\mathrm{{\forall}I}

3–13

That is nine lines in place of one. A written proof would say “so $R(x_0)$ , since $\neg Q(x_0)$ ”.

6.3.5. Four kinds of task, with quantifiers

Section 3.2 sorted propositional problems into four kinds, and the kind decides how the search begins. The same four come back. A theorem $\vdash \varphi$ has no premises; an equivalence $\varphi \dashv\vdash \psi$ needs two derivations; inconsistency of a list is a derivation of $\bot$ from it (Section 3.2’s definition reads the same for first-order formulas, now with all the rules); and derive or break withholds the verdict. A claim is broken by a counter-reading, which makes every member of its counterexample set true (Section 7.2).

Example (One pair of predicates, four tasks)

(a) Theorem. Show that $\vdash \forall x\, P(x) \to \exists x\, (P(x) \vee Q(x))$ .
(b) Equivalence. Show that $\forall x\, (P(x) \to \neg Q(x)) \dashv\vdash \forall x\, (Q(x) \to \neg P(x))$ .
(c) Inconsistency. Show that the list $\forall x\, (P(x) \to Q(x)), \ \exists x\, (P(x) \wedge \neg Q(x))$ is inconsistent.
(d) Derive or break. Decide $\forall x\, (P(x) \to Q(x)) \vdash \forall x\, P(x) \to \forall x\, Q(x)$ and its converse.

Solution. (a) With no premises the search starts from the goal alone: an $\mathrm{{\to}I}$ box, then the $\exists$ goal waits for a line that shows an instance.

\forall x\, P(x)

asm, for

\mathrm{{{\to}}I}

P(x)

\mathrm{{\forall}E}

P(x) \vee Q(x)

\mathrm{{\vee}I}

\exists x\, (P(x) \vee Q(x))

\mathrm{{\exists}I}

\forall x\, P(x) \to \exists x\, (P(x) \vee Q(x))

\mathrm{{{\to}}I}

1–4

Line 2 instantiates at the variable $x$ itself, and line 4 uses $\mathrm{\exists I}$ at $x$ , as in Proposition 5.5.1. Any term would have done as the witness, since line 1 holds at every term; the variable $x$ is simply the term at hand, and no constant has to be invented.

(b) The E form of Section 6.2 says the same with its two predicates exchanged: “no $P$ is $Q$ ” is “no $Q$ is $P$ ”. An equivalence is two searches, and here the second is the first with the letters exchanged, so one search does the work of both. Each direction opens a flagged box, instantiates at its flag, takes one TAUT step and generalizes:

\forall x\, (P(x) \to \neg Q(x))

x_0

P(x_0) \to \neg Q(x_0)

\mathrm{{\forall}E}

Q(x_0) \to \neg P(x_0)

\mathrm{TAUT}

\forall x\, (Q(x) \to \neg P(x))

\mathrm{{\forall}I}

2–3

\forall x\, (Q(x) \to \neg P(x))

x_0

Q(x_0) \to \neg P(x_0)

\mathrm{{\forall}E}

P(x_0) \to \neg Q(x_0)

\mathrm{TAUT}

\forall x\, (P(x) \to \neg Q(x))

\mathrm{{\forall}I}

2–3

The skeletons are $p \to \neg q \models q \to \neg p$ and the same with $p$ and $q$ exchanged.

(c) An A form and its O form (Section 6.2). The goal is $\bot$ , so the clash step of the method applies, but no pair $\chi$ , $\neg\chi$ is in sight among the premises: the clash lives at a witness. The $\exists$ premise opens its box at once, the $\forall$ premise is instantiated at the witness, and the clash is propositional:

\forall x\, (P(x) \to Q(x))

\exists x\, (P(x) \wedge \neg Q(x))

x_0

P(x_0) \wedge \neg Q(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

\bot

\mathrm{TAUT}

3, 4

\bot

\mathrm{{\exists}E}

2, 3–5

Line 5’s skeleton is $p \wedge \neg q, p \to q \models \bot$ .

(d) With the verdict withheld, spend a minute on each side before committing. For the first claim, a reading that makes the premise true and the conclusion false would need every $P$ to be a $Q$ , every element to be a $P$ , and some element not a $Q$ , which cannot happen; so try to derive it. For the converse, a false hypothesis $\forall x\, P(x)$ makes the premise true cheaply, which suggests a break.

The first claim derives. Lines 3–6 are Example (Flagged boxes at work) (b), run inside the box of line 2:

\forall x\, (P(x) \to Q(x))

\forall x\, P(x)

asm, for

\mathrm{{{\to}}I}

x_0

P(x_0)

\mathrm{{\forall}E}

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

Q(x_0)

\mathrm{{{\to}}E}

4, 3

\forall x\, Q(x)

\mathrm{{\forall}I}

3–5

\forall x\, P(x) \to \forall x\, Q(x)

\mathrm{{{\to}}I}

2–6

At line 6, $x_0$ is not in the premise, in line 6, or in the open assumption on line 2.

The converse breaks. Over $\mathbb{Z}$ , read $P$ as “even” and $Q$ as “positive”. “Every integer is even” is false, so the premise “if every integer is even, then every integer is positive” is true; the conclusion “every even integer is positive” is false at $0$ .

Test the subgoal by a counter-reading. Section 4.7 tested a propositional subgoal by a refuting row before chasing it. The first-order form of the move is the same. When a search produces a subgoal, look for a reading that makes the available lines true and the subgoal false before you chase it. If you find one, the subgoal is the wrong one: Section 7.2 states that such a reading rules out every derivation of it from those lines. Return to the step that produced it, and choose differently there: another term for a $\forall E$ , a box opened earlier, or a different case split. A reading takes a minute to find, and it can save the search a long chase.

Quick check. A search for the limit derivation of Section 6.1 instantiates the premise at $\varepsilon_0$ instead of $\varepsilon_0/2$ , and reaches the subgoal $\left| 2 a_{n_0} - 2L \right| < \varepsilon_0$ with $\left| a_{n_0} - L \right| < \varepsilon_0$ available. Find a sequence and numbers that make every available line true and the subgoal false.

Solution. Take $\varepsilon_0 = 1$ ; $a_n = L$ for every $n$ except $a_{n_0} = L + 0.75$ ; and $N_0 = n_0$ . The premise holds, since the sequence is eventually constant at $L$ . Every term is within $0.75 < 1$ of $L$ , so the instance of the premise at $\varepsilon_0$ and the box line $\forall n \in \mathbb{N}\; (n \ge N_0 \to \left| a_n - L \right| < \varepsilon_0)$ hold; $n_0 \ge N_0$ holds; and $\left| a_{n_0} - L \right| = 0.75 < 1$ . But $\left| 2 a_{n_0} - 2L \right| = 1.5 \ge 1$ . The subgoal is the wrong one; go back to the choice of term.

Quick check. Which task is $\exists x\, (P(x) \wedge \neg P(x)) \vdash \bot$ , and how long is its derivation with TAUT?

Solution. Inconsistency. Three lines below the premise:

\exists x\, (P(x) \wedge \neg P(x))

x_0

P(x_0) \wedge \neg P(x_0)

asm, for

\mathrm{{\exists}E}

\bot

\mathrm{TAUT}

\bot

\mathrm{{\exists}E}

1, 2–3

6.3.6. A library of first-order sequents

Here is what the book has proved about quantifiers, grouped by use; a search that needs one of these can copy its derivation, with formulas in place of letters, rather than rediscover it.

Use	Sequent	Where
exchange two like quantifiers	$\forall x\, \forall y\, \varphi \dashv\vdash \forall y\, \forall x\, \varphi$	Example (Flagged boxes at work) (c)
rename a bound variable	$\forall y\, \varphi \dashv\vdash \forall z\, \varphi[z/y]$ , and the same for $\exists$	Section 5.4 (the fold after Example (Flagged boxes at work)); Section 5.6
every gives some	$\forall x\, \varphi \vdash \exists x\, \varphi$	Proposition 5.5.1
some-all gives all-some	$\exists x\, \forall y\, R(x, y) \vdash \forall y\, \exists x\, R(x, y)$	Proposition 5.6.2
distribute	$\forall$ over $\wedge$ and $\exists$ over $\vee$ both ways; $\forall$ over $\vee$ and $\exists$ over $\wedge$ one way	Proposition 6.2.6 (the instances for $P$ , $Q$ first in Proposition 5.4.1 and Proposition 5.6.1)
negate	“not every” and “some not”; “none” and “every not”; a negated implication; bounded forms	Proposition 6.2.1, Proposition 6.2.2, Proposition 6.2.3
move across a connective	the passage laws	Proposition 6.2.7
replace a part	a provable equivalence, inside any formula	Proposition 6.2.4
equality	symmetric and transitive; equals share every property	Proposition 5.7.1, Proposition 5.7.2
bounds in one step	the bounded rules	Proposition 6.1.1
propositional steps	TAUT on the skeleton	Proposition 6.3.1

The laws of Section 6.2 may already be used as one line, by “The laws as one line”; the other rows are patterns to copy. Either way, a row is used by matching its shape and then checking its conditions: the passage laws need the moved variable not free in the other side, a renaming needs a letter new to the formula, and an instance of a row’s letters must be free for the variables it replaces.

Remark (Looking ahead). Every claim this section broke, it broke by a counter-reading. Chapter 7 gives counter-readings an exact form, the counter-model, and states that a counter-model rules out every derivation.

6.3.7. Exercises

A. Check your understanding

Exercise (A1)

(a) What is the propositional skeleton of $\neg\exists x\, P(x) \vee (Q(c) \wedge \exists y\, P(y))$ ? Is it a tautology?
(b) What is the propositional skeleton of $\exists x\, (P(x) \wedge Q(x)) \wedge \neg\exists x\, (Q(x) \wedge P(x))$ ? Can a TAUT step derive $\bot$ from this formula?
(c) Which are TAUT steps? (i) From $\forall x\, P(x)$ and $\forall x\, P(x) \to \exists y\, Q(y)$ to $\exists y\, Q(y)$ . (ii) From $\forall x\, (P(x) \to Q(x))$ and $P(c)$ to $Q(c)$ . (iii) From $\neg\neg\exists x\, P(x)$ to $\exists x\, P(x)$ .
(d) In Example (A search that waits for its witnesses), why is the box on premise 3 opened before premise 1 is used?
(e) A counter-reading makes the premises of a claim true and its conclusion false. What may you say now, and what will Section 7.2 add?

Solution. (a) $\neg p \vee (q \wedge p)$ : $\exists x\, P(x)$ and $\exists y\, P(y)$ differ only by renaming, so they share $p$ . It is not a tautology: $p$ true and $q$ false make it false.

(b) $p \wedge \neg q$ . The two prime formulas are not renamings of each other ( $P(x) \wedge Q(x)$ against $Q(x) \wedge P(x)$ ), so they get different atoms, and $p \wedge \neg q$ is true in a row: no. $\bot$ is derivable all the same, by an $\mathrm{\exists E}$ box on the first conjunct, a TAUT step inside it to $Q(x_0) \wedge P(x_0)$ , $\mathrm{\exists I}$ , and a clash with the second conjunct.

(c) (i) Yes: $p, p \to q \models q$ . (ii) No: $p, q \not\models r$ ; it is $\mathrm{\forall E}$ at $c$ , then $\mathrm{{\to}E}$ . (iii) Yes: $\neg\neg p \models p$ .

(d) Premise 1 is a $\forall$ whose useful term is not yet known, and the box supplies it, $x_0$ . These are the moves “name the witness early” and “instantiate at the term you need”, in that order.

(e) Now: the claim breaks, and a search for it is abandoned. Section 7.2 states that such a claim has no derivation.

B. Practice

Exercise (B1: Derive or break, twelve claims)

Derive each claim, with TAUT allowed, or break it by a reading over $\mathbb{Z}$ that makes every member of its counterexample set true. The groups say which move to try first; they do not say which claims hold. Claims 1–3: name the witness early. Claims 4 and 5: instantiate at the term you need. Claims 6–8: the propositional core. Claims 9–12: move a quantifier, or derive $\bot$ .

$\exists x\, (P(x) \wedge Q(x)), \ \forall x\, (P(x) \to (Q(x) \to R(f(x)))) \vdash \exists y\, R(y)$ .
$\exists x\, R(x, x) \vdash \forall x\, \exists y\, R(x, y)$ .
$\exists x\, P(x), \ \forall x\, (P(x) \to \forall y\, R(x, y)) \vdash \forall y\, \exists x\, R(x, y)$ .
$\forall x\, \forall y\, (R(x, y) \to R(y, x)), \ \forall x\, R(x, f(x)) \vdash \forall x\, R(f(x), x)$ .
$\forall x\, R(x, f(x)) \vdash \forall x\, R(f(x), x)$ .
$\forall x\, (P(x) \to Q(x)), \ \forall x\, (Q(x) \to R(x)) \vdash \forall x\, (\neg R(x) \to \neg P(x))$ .
$\forall x\, (P(x) \vee Q(x)), \ \forall x\, \neg P(x) \vdash \forall x\, Q(x)$ .
$\forall x\, (P(x) \vee Q(x)), \ \neg\forall x\, P(x) \vdash \forall x\, Q(x)$ .
$\forall x\, (P(x) \to Q(x)) \vdash \exists x\, P(x) \to \exists x\, Q(x)$ .
$\forall x\, (P(x) \to Q(x)) \vdash \exists x\, P(x) \to \forall x\, Q(x)$ .
$\forall x\, (P(x) \leftrightarrow \neg P(f(x))), \ \forall x\, P(x) \vdash \bot$ .
$\forall x\, \exists y\, R(x, y), \ \forall x\, \forall y\, (R(x, y) \to \neg R(y, x)) \vdash \bot$ .

Solution. 1. Derive. The box of the witness opens first; inside it, premise 2 is instantiated at $x_0$ , and the postponed goal takes the compound witness $f(x_0)$ .

\exists x\, (P(x) \wedge Q(x))

\forall x\, (P(x) \to (Q(x) \to R(f(x))))

x_0

P(x_0) \wedge Q(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to (Q(x_0) \to R(f(x_0)))

\mathrm{{\forall}E}

R(f(x_0))

\mathrm{TAUT}

3, 4

\exists y\, R(y)

\mathrm{{\exists}I}

\exists y\, R(y)

\mathrm{{\exists}E}

1, 3–6

Line 5’s skeleton is $p \wedge q, p \to (q \to r) \models r$ . At line 7, $x_0$ is not in line 7, in line 1, or in a premise.

2. Breaks. Read $R(x, y)$ as “ $x \cdot y = 1$ ”. The premise is true, since $1 \cdot 1 = 1$ ; the conclusion fails at $x = 0$ , since $0 \cdot y = 0$ for every $y$ .

3. Derive.

\exists x\, P(x)

\forall x\, (P(x) \to \forall y\, R(x, y))

x_0

P(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to \forall y\, R(x_0, y)

\mathrm{{\forall}E}

\forall y\, R(x_0, y)

\mathrm{{{\to}}E}

4, 3

y_0

R(x_0, y_0)

\mathrm{{\forall}E}

\exists x\, R(x, y_0)

\mathrm{{\exists}I}

\forall y\, \exists x\, R(x, y)

\mathrm{{\forall}I}

6–7

\forall y\, \exists x\, R(x, y)

\mathrm{{\exists}E}

1, 3–8

At line 8, $y_0$ is not in a premise, in the open assumption on line 3, or in line 8. At line 9, $x_0$ is not in line 9, in line 1, or in a premise.

4. Derive. The term premise 1 needs is $f(x_0)$ , and premise 2 names it.

\forall x\, \forall y\, (R(x, y) \to R(y, x))

\forall x\, R(x, f(x))

x_0

R(x_0, f(x_0))

\mathrm{{\forall}E}

\forall y\, (R(x_0, y) \to R(y, x_0))

\mathrm{{\forall}E}

R(x_0, f(x_0)) \to R(f(x_0), x_0)

\mathrm{{\forall}E}

R(f(x_0), x_0)

\mathrm{{{\to}}E}

5, 3

\forall x\, R(f(x), x)

\mathrm{{\forall}I}

3–6

Line 5 instantiates at $f(x_0)$ , which is free for $y$ . At line 7, $x_0$ is not in a premise or in line 7, and no assumption is open.

5. Breaks. Read $f(x)$ as $x + 1$ and $R$ as $<$ . Every $x < x + 1$ , so the premise is true; no $x + 1 < x$ , so the conclusion is false.

6. Derive.

\forall x\, (P(x) \to Q(x))

\forall x\, (Q(x) \to R(x))

x_0

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

Q(x_0) \to R(x_0)

\mathrm{{\forall}E}

\neg R(x_0) \to \neg P(x_0)

\mathrm{TAUT}

3, 4

\forall x\, (\neg R(x) \to \neg P(x))

\mathrm{{\forall}I}

3–5

Line 5’s skeleton is $p \to q, q \to r \models \neg r \to \neg p$ .

7. Derive.

\forall x\, (P(x) \vee Q(x))

\forall x\, \neg P(x)

x_0

P(x_0) \vee Q(x_0)

\mathrm{{\forall}E}

\neg P(x_0)

\mathrm{{\forall}E}

Q(x_0)

\mathrm{TAUT}

3, 4

\forall x\, Q(x)

\mathrm{{\forall}I}

3–5

Line 5’s skeleton is $p \vee q, \neg p \models q$ .

8. Breaks. Read $P$ as “even” and $Q$ as “odd”. Every integer is even or odd; not every integer is even; and $0$ is not odd, so “every integer is odd” is false.

9. Derive.

\forall x\, (P(x) \to Q(x))

\exists x\, P(x)

asm, for

\mathrm{{{\to}}I}

x_0

P(x_0)

asm, for

\mathrm{{\exists}E}

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

Q(x_0)

\mathrm{{{\to}}E}

4, 3

\exists x\, Q(x)

\mathrm{{\exists}I}

\exists x\, Q(x)

\mathrm{{\exists}E}

2, 3–6

\exists x\, P(x) \to \exists x\, Q(x)

\mathrm{{{\to}}I}

2–7

At line 7, $x_0$ is not in line 7, in line 2, in the premise, or in an open assumption (line 2’s box is still open, and line 2 does not mention $x_0$ ).

10. Breaks. Read $P(x)$ as “ $x = 0$ ” and $Q(x)$ as “ $x \cdot x = x$ ”. The premise holds, since the only $x$ with $x = 0$ has $0 \cdot 0 = 0$ . In the conclusion, $\exists x\, (x = 0)$ is true and $\forall x\, (x \cdot x = x)$ is false, since $2 \cdot 2 = 4$ ; so the implication is false.

11. Derive. Premise 2 is instantiated twice, at $y$ and at $f(y)$ , the two terms that premise 1 at $y$ mentions.

\forall x\, (P(x) \leftrightarrow \neg P(f(x)))

\forall x\, P(x)

P(y) \leftrightarrow \neg P(f(y))

\mathrm{{\forall}E}

P(y)

\mathrm{{\forall}E}

P(f(y))

\mathrm{{\forall}E}

\bot

\mathrm{TAUT}

3, 4, 5

Line 6’s skeleton is $p \leftrightarrow \neg q, p, q \models \bot$ : no row makes all three true.

12. Breaks. Read $R$ as $<$ . Every integer has a larger one, and $x < y$ excludes $y < x$ . Both premises are true, and $\neg\bot$ is true, so the whole counterexample set is true: the list is not shown inconsistent.

Seven claims derive and five break. Four breaks sit beside a derivable look-alike: 5 beside 4, 8 beside 7, 10 beside 9, and 12 beside 11. Claim 2 weakens the premise of the derivable $\forall x\, R(x, x) \vdash \forall x\, \exists y\, R(x, y)$ of Example (Derivations with existential introduction) (c). Every break is a counter-reading (Section 7.2).

Marking scheme. (10 points) - 4: the twelve verdicts, $\tfrac13$ point for each correct one, rounded down. - 3: the seven derivations, each with every closing side condition checked and every TAUT line’s skeleton named. - 3: the five readings, each with every premise and the conclusion evaluated. Fatal errors (0 for the claim): a TAUT line that looks inside a quantifier; a “break” with a premise false.

Exercise (B2: Two witnesses in a row)

The premises are 1 $\forall x\, (P(x) \to \exists y\, R(x, y))$ , 2 $\forall x\, \forall y\, (R(x, y) \to P(y))$ and 3 $P(c)$ ; the goal is $\exists y\, \exists z\, (R(c, y) \wedge R(y, z))$ . Here is a partial derivation:

\forall x\, (P(x) \to \exists y\, R(x, y))

\forall x\, \forall y\, (R(x, y) \to P(y))

P(c)

\vdots

y_0

R(c, y_0)

asm, for

\mathrm{{\exists}E}

\vdots

\exists y\, \exists z\, (R(c, y) \wedge R(y, z))

\exists y\, \exists z\, (R(c, y) \wedge R(y, z))

Name the move, then complete it.

Solution. The move is “name the witness early”, twice, with each $\forall$ line instantiated only at the terms in hand: $c$ (premise 3) first, then the witness $y_0$ .

\forall x\, (P(x) \to \exists y\, R(x, y))

\forall x\, \forall y\, (R(x, y) \to P(y))

P(c)

P(c) \to \exists y\, R(c, y)

\mathrm{{\forall}E}

\exists y\, R(c, y)

\mathrm{{{\to}}E}

4, 3

y_0

R(c, y_0)

asm, for

\mathrm{{\exists}E}

\forall y\, (R(c, y) \to P(y))

\mathrm{{\forall}E}

R(c, y_0) \to P(y_0)

\mathrm{{\forall}E}

P(y_0)

\mathrm{{{\to}}E}

8, 6

P(y_0) \to \exists y\, R(y_0, y)

\mathrm{{\forall}E}

\exists y\, R(y_0, y)

\mathrm{{{\to}}E}

10, 9

z_0

R(y_0, z_0)

asm, for

\mathrm{{\exists}E}

R(c, y_0) \wedge R(y_0, z_0)

\mathrm{{\wedge}I}

6, 12

\exists z\, (R(c, y_0) \wedge R(y_0, z))

\mathrm{{\exists}I}

\exists y\, \exists z\, (R(c, y) \wedge R(y, z))

\mathrm{{\exists}I}

\exists y\, \exists z\, (R(c, y) \wedge R(y, z))

\mathrm{{\exists}E}

11, 12–15

\exists y\, \exists z\, (R(c, y) \wedge R(y, z))

\mathrm{{\exists}E}

5, 6–16

Lines 4 and 7 instantiate at $c$ , and lines 8 and 10 at $y_0$ ; line 15 is $\mathrm{\exists I}$ at $y_0$ , which is free for $y$ . At line 16, $z_0$ is not in line 16, in line 11, in the premises, or in the open assumption on line 6. At line 17, $y_0$ is not in line 17, in line 5, or in the premises.

Marking scheme. (10 points) - 2: names the move. - 3: opens the two boxes as soon as their $\exists$ lines exist. - 3: the $\mathrm{\forall E}$ lines at $c$ , $c$ , $y_0$ and $y_0$ , the terms read off the lines in hand. - 2: the two side conditions. Fatal error (0 for the step): $\mathrm{\exists I}$ on line 15 before line 14, so that the witness $z_0$ appears in the box’s last line.

Exercise (B3: How much TAUT saves)

(a) Derive $\forall x\, (P(x) \to Q(x)), \ \forall x\, (Q(x) \to \neg P(x)) \vdash \forall x\, \neg P(x)$ twice: once without TAUT, once with exactly one TAUT line. Count the lines.
(b) Is the step from $\forall x\, (P(x) \to Q(x))$ to $\forall x\, (\neg Q(x) \to \neg P(x))$ a TAUT step?

Solution. (a) With TAUT, six lines (left); without it, ten (right):

\forall x\, (P(x) \to Q(x))

\forall x\, (Q(x) \to \neg P(x))

x_0

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

Q(x_0) \to \neg P(x_0)

\mathrm{{\forall}E}

\neg P(x_0)

\mathrm{TAUT}

3, 4

\forall x\, \neg P(x)

\mathrm{{\forall}I}

3–5

\forall x\, (P(x) \to Q(x))

\forall x\, (Q(x) \to \neg P(x))

x_0

P(x_0) \to Q(x_0)

\mathrm{{\forall}E}

Q(x_0) \to \neg P(x_0)

\mathrm{{\forall}E}

P(x_0)

asm, for

\mathrm{{\neg}I}

Q(x_0)

\mathrm{{{\to}}E}

3, 5

\neg P(x_0)

\mathrm{{{\to}}E}

4, 6

\bot

\mathrm{{\neg}E}

5, 7

\neg P(x_0)

\mathrm{{\neg}I}

5–8

\forall x\, \neg P(x)

\mathrm{{\forall}I}

3–9

Line 5 on the left has the skeleton $p \to q, q \to \neg p \models \neg p$ .

(b) No: the two formulas are prime and not renamings of each other, so their skeletons are two different atoms. The step is derivable by instantiating, one TAUT line ( $p \to q \models \neg q \to \neg p$ ) and generalizing, the pattern of Example (One pair of predicates, four tasks) (b).

Marking scheme. (10 points) - 3: the TAUT derivation, with the skeleton named. - 4: the derivation without TAUT. - 1: the count. - 2: (b), with the reason. Fatal error (0 for the step): a TAUT line citing the $\forall$ lines directly to reach $\neg P(x_0)$ .

C. Going deeper

Exercise (C1: Some index decides, used later)

Let $D(n)$ say “ $a_n > 0$ ” for a sequence $(a_n)$ , over a domain of indices.

(a) Derive $\vdash \exists n\, (D(n) \to \forall m\, D(m))$ , with $\mathrm{LEM}$ on $\forall m\, D(m)$ .
(b) Derive it again in two lines, from one TAUT line and one law of Section 6.2.
(c) Say in two sentences which index the sentence promises, and why the derivations of (a) and (b) name none.

Solution (Hint 1). For (a): in the case $\neg\forall m\, D(m)$ , which law of Section 6.2 turns the negated $\forall$ into an $\exists$ ?

Solution (Hint 2). For (b): the formula $\forall n\, D(n) \to \forall m\, D(m)$ has the skeleton $p \to p$ . Which passage law moves the $\forall n$ out of the hypothesis of an implication, turning it into $\exists n$ ?

Solution. (a)

\forall m\, D(m) \vee \neg\forall m\, D(m)

\mathrm{LEM}

\forall m\, D(m)

asm, for

\mathrm{{\vee}E}

D(n)

asm, for

\mathrm{{{\to}}I}

\forall m\, D(m)

\mathrm{R}

D(n) \to \forall m\, D(m)

\mathrm{{{\to}}I}

3–4

\exists n\, (D(n) \to \forall m\, D(m))

\mathrm{{\exists}I}

\neg\forall m\, D(m)

asm, for

\mathrm{{\vee}E}

\exists m\, \neg D(m)

QN (a) 7

m_0

\neg D(m_0)

asm, for

\mathrm{{\exists}E}

D(m_0) \to \forall m\, D(m)

VI 9

\exists n\, (D(n) \to \forall m\, D(m))

\mathrm{{\exists}I}

\exists n\, (D(n) \to \forall m\, D(m))

\mathrm{{\exists}E}

8, 9–11

\exists n\, (D(n) \to \forall m\, D(m))

\mathrm{{\vee}E}

1, 2–6, 7–12

Line 6 is $\mathrm{\exists I}$ at the variable $n$ itself, as in the proof of passage law (d); as there, the step is sound because every domain is non-empty (Section 7.1). Line 11 is $\mathrm{\exists I}$ at $m_0$ . At line 12, $m_0$ is not in line 12, in line 8, or in the open assumption on line 7.

(b)

\forall n\, D(n) \to \forall m\, D(m)

\mathrm{TAUT}

\exists n\, (D(n) \to \forall m\, D(m))

passage (d) 1

The two prime formulas of line 1 differ only by renaming, so the skeleton is $p \to p$ , a tautology. Line 2 is Proposition 6.2.7 (d), the direction $\dashv$ , used as one line (“The laws as one line”), with $\varphi$ the formula $D(n)$ and $\psi$ the formula $\forall m\, D(m)$ , in which $n$ is not free.

(c) If every term is positive, any index will do; if not, an index with $a_n \le 0$ does, since then the implication is vacuously true. The derivation splits on which case holds without deciding it ( $\mathrm{LEM}$ in (a), the classical direction of (d) in (b)), so it never names the index.

Marking scheme. (10 points) - 4: (a), with the $\mathrm{LEM}$ split, both cases closed, with the side condition of every line that closes a flagged box checked. - 3: (b), with the TAUT line justified by renaming, and law (d) with its condition checked. - 3: (c). Fatal errors (0 for the step): giving $\forall n\, D(n)$ and $\forall m\, D(m)$ different atoms and then claiming the TAUT line anyway; $\mathrm{\exists I}$ at $m_0$ after its box has closed.

Exercise (C2: Every M is P, every M is S, so some S is P?)

(a) Break $\forall x\, (M(x) \to P(x)), \ \forall x\, (M(x) \to S(x)) \vdash \exists x\, (S(x) \wedge P(x))$ by a reading over $\mathbb{N}$ .
(b) Add the premise $\exists x\, M(x)$ and derive the conclusion.
(c) Which line of (b) needs the new premise, and what does Section 5.1’s existential import have to do with it?

Solution. (a) Breaks. Read $M(n)$ as “ $n$ is an even prime greater than $2$ ”, which is true of no $n$ ; $P(n)$ as “ $n$ is odd”; and $S(n)$ as “ $n$ is even”. Both premises are vacuously true, since their hypothesis $M(n)$ is false for every $n$ , and “some even number is odd” is false (Section 7.2).

(b)

\forall x\, (M(x) \to P(x))

\forall x\, (M(x) \to S(x))

\exists x\, M(x)

x_0

M(x_0)

asm, for

\mathrm{{\exists}E}

M(x_0) \to P(x_0)

\mathrm{{\forall}E}

M(x_0) \to S(x_0)

\mathrm{{\forall}E}

S(x_0) \wedge P(x_0)

\mathrm{TAUT}

4, 5, 6

\exists x\, (S(x) \wedge P(x))

\mathrm{{\exists}I}

\exists x\, (S(x) \wedge P(x))

\mathrm{{\exists}E}

3, 4–8

Line 7’s skeleton is $m, m \to p, m \to s \models s \wedge p$ . At line 9, $x_0$ is not in line 9, in line 3, or in a premise.

(c) Line 7: its TAUT needs $M(x_0)$ , line 4, which only the box of premise 3 supplies. Without it, $\mathrm{\exists I}$ could still be applied at some term, but no line would say that term is $S$ and $P$ . A “for every” claims no instance, so the old reading of “every $M$ is $P$ ” as also saying that there are $M$ s is not the book’s reading. With that reading the inference was valid; without it, the premise must be added.

Marking scheme. (10 points) - 3: (a), with all three truth values justified. - 4: (b). - 3: (c). Fatal error (0 for the step): a “break” whose $M$ is true of some number.