5.3  Using “For Every”: Instantiation

Section 5.2 made the language exact and defined the operation $\phi [t/x]$, “put the term $t$ in for the variable $x$”, with its one hazard, capture. We can now give the first quantifier rule. It is the rule for using a universal statement: whatever holds for every object holds for the object named by any term we care to write. The rule is called $\mathrm{\forall }\mathrm{E}$. It is the rule behind every “by the theorem, applied to $x=2$”. With it alone, universal statements can be used but not proved, and the section meets exactly that gap (“A stall” below), which Section 5.4 fills.

5.3.1. Applying a statement about everything

Every application of a general fact to a particular case is one step of logic, and so far that step has been taken on trust. Three earlier places took it.

• Section 1.3 used the theorem “if an integer is divisible by $2$ and by $3$, then it is divisible by $6$” at $n=42$, taking the step from “every integer” to the one integer $42$ on trust.
• In Example (A number below every positive number) (Section 2.5) the hypothesis was “$x\le \epsilon$ for every $\epsilon >0$”, and the proof applied it to the one number $\epsilon =x/2$.
• Section 5.1 opened with the argument “every positive real has a square root; $2$ is positive; so $2$ has a square root”, which a truth table calls invalid because it sees only three unrelated atoms.

The same step happens in each: a statement about every object is applied to one object, named by a term. In the language of Section 5.2, the first premise of the square-root argument is $\mathrm{\forall }x(P(x)\to S(x))$, and applying it to $2$ gives $$(P(x)\to S(x))[2/x]=P(2)\to S(2),$$ which is part (a) of Example (Four substitutions). From there $\to \mathrm{E}$ finishes. All that is missing is a rule that licenses the first step.

5.3.2. The rule

A universal statement may be applied to any term: remove the quantifier and put the term in for the variable.

In words: if a line says that $\phi$ holds for every $x$, then any later line, where that line is still available, may write what $\phi$ says about $t$. The rule cites one line and no box.

• Schema: the block above: one cited line, no box.
• Reading: drop the $\mathrm{\forall }x$, put one term in for every free $x$, and check that no letter of the term gets caught by a quantifier inside.
• Example: from $\mathrm{\forall }x(P(x)\to S(x))$, “$\mathrm{\forall }\mathrm{E}$ 1” at the term $2$ writes $P(2)\to S(2)$.

Read the definition clause by clause; exercises cite the clauses by number.

1. The cited line’s main symbol is $\mathrm{\forall }x$, with all of $\phi$ as its scope: $\mathrm{\forall }xP(x)\to Q(c)$ is an implication; a $\mathrm{\forall }$ buried inside another connective must first be taken out by that connective’s rule, when it can be ($\wedge \mathrm{E}$ takes $\mathrm{\forall }xP(x)$ out of $\mathrm{\forall }xP(x)\wedge Q(c)$), and a $\mathrm{\forall }$ in the hypothesis of an implication cannot be instantiated at all.
2. Any term: a constant, a variable ($x$ itself included) or a compound term. Nothing about it needs to be established first, since every term names an object of the domain.
3. Every free occurrence, by the same term: the new line is $\phi [t/x]$; we do not choose which occurrences change.
4. Free for $x$ (Definition 5.2.6): no letter of $t$ is caught by a quantifier of $\phi$. This is the rule’s only restriction.
5. Line $i$ is available (the scope rule of Definition 1.4.2), as for every rule.

When the universal statement has a bound, $\mathrm{\forall }x\in A\phi$, using it at $t$ also needs the line $t\in A$.

One line, many uses. The cited line stays where it is, available as before. A derivation may instantiate the same universal line as often as it likes, at different terms or the same one. Worked derivation (d) below uses one premise twice.

Why this rule. It says no more than the word “every”. If every object in the domain satisfies $\phi$, then so does the object that $t$ names, whichever object that is. A term always names something, since the domain is never empty (Section 5.1), so the instance always has something to be about.

Why “free for”. The instance must say about $t$ what $\phi$ says about $x$. Section 5.2 showed that when a variable of $t$ is captured, $\phi [t/x]$ can say something quite different. The condition rules capture out, and the subsection on common errors below shows the rule going wrong without it.

A long “and”, taken apart. In world W of Section 5.1, $\mathrm{\forall }x\phi$ says $\phi [a/x]\wedge \phi [b/x]\wedge \phi [c/x]\wedge \phi [d/x]$, and $\mathrm{\forall }\mathrm{E}$ at $b$ does what $\wedge \mathrm{E}$ does: it takes out one conjunct. Over $\mathbb{N}$ the conjunction cannot be written; $\mathrm{\forall }\mathrm{E}$ takes out any conjunct, at any term, without writing the rest.

5.3.3. Four derivations

The worked derivations below use $\mathrm{\forall }\mathrm{E}$ and the rules of Chapter 1. Each has an Idea that says why each rule was chosen, continuing the search method of Section 3.1: a goal-directed step looks at the goal’s main symbol, a premise-directed step at a resource’s. The new question is the one that $\mathrm{\forall }\mathrm{E}$ raises every time: at which term?

In each derivation, the Idea chose the term of every $\mathrm{\forall }\mathrm{E}$ by matching: the goal, or a hypothesis still needed, has a definite shape, and the instance is chosen to have that shape. Instantiating at a term that nothing asks for is legal, and it fills a derivation with lines that lead nowhere.

5.3.4. Checking a line of instantiation

Choosing the term can take thought; checking a line never does. For a line justified “$\mathrm{\forall }\mathrm{E}$ $i$”, ask four questions.

1. Is line $i$ available here (Definition 1.4.2)?
2. Is the main symbol of line $i$ a universal quantifier? If so, read off its variable $x$ and its scope $\phi$.
3. Is this line $\phi [t/x]$ for some term $t$? Find $t$ by comparing the two lines at a free occurrence of $x$ in $\phi$; then check that every free occurrence of $x$ became that same $t$, and that nothing else changed.
4. Is $t$ free for $x$ in $\phi$?

Run on line 5 of (d): line 1 is available, since no box contains it; its main symbol is $\mathrm{\forall }x$, with scope $P(x)\to P(f(x))$; comparing gives $t=f(c)$, and both occurrences of $x$ became $f(c)$; and $f(c)$ has no variables, so it is free for $x$. The line passes.

5.3.5. How this rule looks in a mathematical proof

Let $a$ be a real number. A proof might say:

Since $y^2\ge 0$ for every real $y$, applying this to $a-1$ gives $(a-1{)}^2\ge 0$, that is, $a^2-2a+1\ge 0$.

The first half of the sentence is one $\mathrm{\forall }\mathrm{E}$, at the compound term $a-1$. The second half rewrites $(a-1{)}^2$ by school algebra. In a derivation such a step is written as one line justified “arith”, for arithmetic:

A line justified “arith” records a fact of school arithmetic or algebra, used on the lines it cites; here the fact is that $(u-1{)}^2$ and $u^2-2u+1$ are the same number for every real $u$. It is not a new rule, and the facts of school algebra are used as facts.

Section 5.4 will turn this three-line derivation into a proof of $x^2-2x+1\ge 0$ for every real $x$. That needs a rule this section does not have.

5.3.6. Common errors

Three mistakes are worth seeing written out, each with a reading in which the premise is true and the offending line false.

Capture. The premise $\mathrm{\forall }x\mathrm{\exists }y(y\ne x)$ says, over $\mathbb{N}$, that for every number there is a different one; it is true, since $x+1\ne x$. Instantiating “at $y$” without looking writes this:

Line 2 says that some number differs from itself, which is false. The step breaks the side condition: the free occurrence of $x$ in $\mathrm{\exists }y(y\ne x)$ lies in the scope of $\mathrm{\exists }y$, and $y$ is a variable of the term $y$, so $y$ is not free for $x$. This is the capture example of Section 5.2, now inside a derivation. The repair is to rename first: $\mathrm{\forall }x\mathrm{\exists }z(z\ne x)$ is the same premise up to renaming, and $\mathrm{\forall }\mathrm{E}$ at $y$ gives $\mathrm{\exists }z(z\ne y)$, “some number differs from $y$”, which is what was meant.

A buried quantifier. From the line $\mathrm{\forall }xP(x)\to Q(c)$ one may not write $P(c)\to Q(c)$. The main symbol of the line is $\to$, and the $\mathrm{\forall }x$ governs only the hypothesis $\mathrm{\forall }xP(x)$. The line says “if every $x$ has $P$, then $Q(c)$”; the false step reads it as “if $c$ has $P$, then $Q(c)$”, which is far stronger. Over $\mathbb{N}$, read $P(x)$ as $x\ge 1$, $Q(x)$ as $x=0$, and $c$ as $1$. The line is true, because its hypothesis “every natural number is at least $1$” is false ($0$ is not). The false step’s result, “if $1\ge 1$, then $1=0$”, is false.

Replacing only some occurrences. Over $\mathbb{R}$, $\mathrm{\forall }x(x\le x^2\vee x<1)$ is true: a real $x\ge 1$ has $x^2=x\cdot x\ge x$, and every other real has $x<1$. Writing $2\le x^2\vee x<1$ from it replaces the first $x$ and leaves the others. That is not $\phi [2/x]$, which is $2\le 2^2\vee 2<1$: the substitution replaces every free occurrence. The half-replaced line still has $x$ free, and when $x$ names $1$ it reads $2\le 1\vee 1<1$, which is false.

Each error has a reading, a small one, in which the premise is true and the faulty line false.

Three tiny worlds. In each, the premise is true and the faulty line false. Capture: $\mathrm{\forall }x\mathrm{\exists }y(y\ne x)$ is true, since each dot has the other; line 2, $\mathrm{\exists }y(y\ne y)$, is false, since no dot differs from itself. A buried quantifier: $\mathrm{\forall }xP(x)\to Q(c)$ is true, since $\mathrm{\forall }xP(x)$ fails at $0$; $P(c)\to Q(c)$ is false, since $1$ has $P$ and not $Q$. Some occurrences only: $\mathrm{\forall }x(P(x)\vee \mathrm{\neg }P(x))$ is true, since at each dot one side holds; the half-replaced $P(c)\vee \mathrm{\neg }P(x)$, which put $c$ in for the first $x$ only, is false, since $a$ lacks $P$ and $x$ names $b$, which has it. The instance $P(c)\vee \mathrm{\neg }P(c)$ is true, as every instance must be.

5.3.7. A stall

Try the sequent $$\mathrm{\forall }x(P(x)\wedge Q(x))⊢\mathrm{\forall }xP(x).$$ It is plainly correct: if every $x$ has both properties, then every $x$ has the first. Search for a derivation. The goal begins with $\mathrm{\forall }$, and no rule so far is made for proving a $\mathrm{\forall }$. Apart from $\mathrm{\perp }\mathrm{E}$ (Definition 2.1.1) and $\mathrm{RAA}$ (Definition 2.5.1), which reach a line only by way of a contradiction, a line beginning with $\mathrm{\forall }$ can only be taken out of a line or box that already contains it. So the goal-directed step has nothing to offer, and we turn to the premise. $\mathrm{\forall }\mathrm{E}$ at $c$ gives $P(c)\wedge Q(c)$, and $\wedge \mathrm{E}$ gives $P(c)$. The same works at $d$, at $f(c)$, at any term we name. But each line is an instance. No finite list of instances is the statement $\mathrm{\forall }xP(x)$, which speaks about every object at once, including all the objects that none of our terms happen to name.

So with $\mathrm{\forall }\mathrm{E}$ alone, a universal statement can be used but not proved. Leaving aside a detour through a contradiction, a derivation can write $\mathrm{\forall }x\psi$ only by taking it out of a line or box that already contains it, as line 2 of (b) took $\mathrm{\forall }yR(c,y)$ out of the premise. Section 1.3 was in the same position with implications, and Section 1.4 filled the gap with a box. Section 5.4 does the same for $\mathrm{\forall }$: it proves $P$ of one name about which nothing is known, and that box finishes this derivation in four lines.

Counter-readings. Each error above was shown wrong by a reading, a domain with a meaning for every symbol and a value for each free variable, in which the premises are true and the line is false. Call such a reading a counter-reading: it makes the whole counterexample set of the claim (Section 1.1), its premises and the negation of its line, true at once. A counter-reading shows that a step is unsafe. It is also how this book shows that a sequent has no derivation at all: a search that stalls proves nothing, since a cleverer derivation might exist. Sections 7.1 and 7.2 make readings exact and state that a counter-reading rules out every derivation. Until then, when this chapter says that something does not follow, it gives a counter-reading, and it never treats a stalled search as a proof.

5.3.8. The rule card

Chapters 1 and 2’s thirteen rules are on the card at the end of Section 3.1; here are this chapter’s so far.

Written mathematics has many forms of the phrase: “in particular, for $x=3$, …”; “applying the hypothesis to $x_0-1$, …”; “by the theorem with $\epsilon /2$ in place of $\epsilon$, …”. In the Lean column, h is the universal statement and t the term; applying h to t gives the instance, just as applying an implication to a proof of its hypothesis gave its conclusion in Section 1.3. In Lean a universal statement behaves like a function that takes a term and returns a proof of the instance.

5.3.9. The search method: one more step

The search method of Section 3.1 had a goal-directed step and a premise-directed step for each connective. Instantiation adds a premise-directed step.

• A resource $\mathrm{\forall }x\phi$. Do not instantiate blindly. Instantiate at the term that the goal, or another resource, asks for: match the shape of the goal (or of a hypothesis still needed) against $\phi$, and read off the term. If the term is not free for $x$ in $\phi$, rename the bound variables of $\phi$ first.

In the Givens/Goal table, $\mathrm{\forall }\mathrm{E}$ adds an instance $\phi [t/x]$ to the Givens, with $t$ read off the goal.

Instantiating is always safe, in the sense of Section 3.1: the new line is added and nothing is lost, since the universal line stays available. What can go wrong is only that the derivation fills with instances nobody needs, as a forward search filled with useless lines in Section 1.3.

5.3.10. Exercises

A. Check your understanding

B. Practice