Proof with quantifiers

Searching for a countermodel can establish that an argument fails and can never establish that it succeeds, so predicate logic needs derivations even more than propositional logic did.

The previous lesson closed with the reason: the semantic method is no longer a procedure, since domains are unbounded and no algorithm decides validity. Derivation still works. The system of the sixth and seventh lessons carries over unchanged, and four rules are added, one to introduce and one to eliminate each quantifier. Two of the four are as simple as anything in the subject. The other two carry restrictions, and this lesson spends most of its length on those restrictions, because without them the system proves that everything is everything.

Universal elimination

Universal elimination ( $\forall$ E): from $\forall x φ$ , write $φ$ with any name substituted for $x$ throughout.

If everything is mortal then Socrates is, and so is the alloy, and so is anything else you can name. The rule is sound because the premise says the formula holds of every object in the domain, and a name picks out one of them. There is no restriction: the name may be new or already in use, and it may be one that occurs in the premises, since instantiating a universal claim to something you already know about is exactly what the claim licenses.

Existential introduction

Existential introduction ( $\exists$ I): from a formula containing a name, write the existential formula got by replacing that name with a variable and binding it.

If Socrates is mortal then something is. Soundness is immediate: the named object is a witness. Note that the rule may replace some or all occurrences of the name, so from $L a a$ , " $a$ loves $a$ ", you may infer $\exists x L x x$ , that someone loves themselves, or $\exists x L x a$ , that someone loves $a$ , and the two are different claims.

Those two rules alone settle the argument that broke propositional logic.

#	Formula	Justification
1	$\forall x (M x \to F x)$	premise
2	$M s$	premise
3	$M s \to F s$	1, $\forall$ E
4	$F s$	3, 2, $\to$ E

Four lines for the mortality of Socrates, which propositional logic could not do at all.

Universal introduction, and its restriction

To prove that everything is $F$ , prove it of an arbitrary object.

Universal introduction ( $\forall$ I): from $φ$ containing a name $a$ , write $\forall x φ$ with $x$ replacing $a$ , provided $a$ appears in no premise and in no assumption still open.

The proviso is the whole rule. It makes $a$ genuinely arbitrary: nothing anywhere in the proof said anything special about it, so whatever was shown of it could have been shown of any object, and the generalisation is safe. This is exactly what a mathematician means by "let $n$ be an arbitrary integer", and the restriction is the formal version of the discipline of not smuggling in extra assumptions about $n$ .

Drop the proviso and the system collapses. From the premise $F a$ , meaning that this particular alloy is magnetic, $\forall$ I would give $\forall x F x$ , that everything is magnetic. The name $a$ occurs in a premise, so it is not arbitrary, and the restriction blocks exactly this.

Now the syllogism in full generality: from "all $M$ are $F$ " and "all $S$ are $M$ ", derive "all $S$ are $F$ ".

#	Formula	Justification
1	$\forall x (M x \to F x)$	premise
2	$\forall x (S x \to M x)$	premise
3	│ $S a$	assumption
4	│ $S a \to M a$	2, $\forall$ E
5	│ $M a$	4, 3, $\to$ E
6	│ $M a \to F a$	1, $\forall$ E
7	│ $F a$	6, 5, $\to$ E
8	$S a \to F a$	3-7, $\to$ I
9	$\forall x (S x \to F x)$	8, $\forall$ I

Line 9 is legal because by then the assumption introducing $a$ has been discharged: $a$ occurs in no premise and in no open assumption. Applying $\forall$ I at line 7 instead would have been illegal, since the assumption at line 3 was still in force and it did say something special about $a$ , namely that it was $S$ . That is the single most common error in quantifier proofs, and the timing is the whole of it.

Example. Derive $\forall x (F x \to H x)$ from $\forall x (F x \to G x)$ and $\forall x (G x \to H x)$ .

#	Formula	Justification
1	$\forall x (F x \to G x)$	premise
2	$\forall x (G x \to H x)$	premise
3	│ $F a$	assumption
4	│ $F a \to G a$	1, $\forall$ E
5	│ $G a$	4, 3, $\to$ E
6	│ $G a \to H a$	2, $\forall$ E
7	│ $H a$	6, 5, $\to$ E
8	$F a \to H a$	3-7, $\to$ I
9	$\forall x (F x \to H x)$	8, $\forall$ I

The shape is identical to the syllogism, which is the point: one derivation covers every argument of that form.

Now you. Derive $\forall x G x$ from $\forall x (F x \land G x)$ .

Answer

#	Formula	Justification
1	$\forall x (F x \land G x)$	premise
2	$F a \land G a$	1, $\forall$ E
3	$G a$	2, $\land$ E
4	$\forall x G x$	3, $\forall$ I

Line 4 is legal because $a$ was introduced by $\forall$ E from a premise that does not itself contain $a$ , so nothing special was ever said about it.

Existential elimination, and its restriction

Knowing that something is $F$ does not tell you which thing, so the rule cannot simply hand over a name. It works like argument by cases with a single case.

Existential elimination ( $\exists$ E): given $\exists x φ$ , open a subproof assuming $φ$ with a fresh name substituted for $x$ , derive some conclusion $ψ$ , and close it, writing $ψ$ . The fresh name must not occur in any premise, in any earlier line still available, or in $ψ$ itself.

The name is a temporary label for whatever the witness is, in the way a mathematician writes "let $n$ be such an integer" and then never assumes anything further about it. The requirement that $ψ$ not contain the name is what stops the label from escaping into a conclusion where it would look like a real reference.

Here is what the restriction prevents. Suppose "something is odd", $\exists x O x$ , and "something is even", $\exists x E x$ . Taking a name from each with the same letter $a$ gives $O a$ and $E a$ , then $O a \land E a$ , then $\exists x (O x \land E x)$ : something is both odd and even. Freshness fails at the second step, since $a$ already occurred, and that single requirement is all that stands between the system and arithmetic nonsense.

The other half of the restriction blocks a subtler leak. If the conclusion of the subproof were allowed to contain the fresh name, then from $\exists x F x$ one could assume $F b$ , conclude $F b$ , and export it, ending with a claim about a particular object that was never given.

Example. Derive $\exists x (S x \land P x)$ from $\forall x (M x \to P x)$ and $\exists x (S x \land M x)$ . This is the syllogism Darii.

#	Formula	Justification
1	$\forall x (M x \to P x)$	premise
2	$\exists x (S x \land M x)$	premise
3	│ $S b \land M b$	assumption, $b$ fresh
4	│ $S b$	3, $\land$ E
5	│ $M b$	3, $\land$ E
6	│ $M b \to P b$	1, $\forall$ E
7	│ $P b$	6, 5, $\to$ E
8	│ $S b \land P b$	4, 7, $\land$ I
9	│ $\exists x (S x \land P x)$	8, $\exists$ I
10	$\exists x (S x \land P x)$	2, 3-9, $\exists$ E

Line 9 is the crucial one. The existential is introduced inside the subproof, which removes the name $b$ before the subproof closes, so line 10 satisfies the requirement that the conclusion be free of the fresh name. Almost every $\exists$ E proof ends this way.

Now you. Derive $\exists x G x$ from $\exists x F x$ and $\forall x (F x \to G x)$ .

Answer

#	Formula	Justification
1	$\exists x F x$	premise
2	$\forall x (F x \to G x)$	premise
3	│ $F b$	assumption, $b$ fresh
4	│ $F b \to G b$	2, $\forall$ E
5	│ $G b$	4, 3, $\to$ E
6	│ $\exists x G x$	5, $\exists$ I
7	$\exists x G x$	1, 3-6, $\exists$ E

Both restrictions at once

The instructive proof is the one from the previous lesson's quantifier ordering, since it uses all four rules and both restrictions.

From $\exists y \forall x R x y$ , derive $\forall x \exists y R x y$ .

#	Formula	Justification
1	$\exists y \forall x R x y$	premise
2	│ $\forall x R x b$	assumption, $b$ fresh
3	│ $R a b$	2, $\forall$ E
4	│ $\exists y R a y$	3, $\exists$ I
5	$\exists y R a y$	1, 2-4, $\exists$ E
6	$\forall x \exists y R x y$	5, $\forall$ I

Line 5 is legal because $\exists y R a y$ contains $a$ but not the fresh name $b$ . Line 6 is legal because $a$ occurs in no premise and in no open assumption, having been introduced only by an instantiation.

Now try the converse, which the previous lesson refuted with a two-object countermodel, and watch the rules refuse. From $\forall x \exists y R x y$ you may instantiate to $\exists y R a y$ , then assume $R a b$ with $b$ fresh. To reach $\forall x R x b$ you would need $\forall$ I on $a$ , but you are inside a subproof whose assumption $R a b$ contains $a$ , so $a$ is not arbitrary and the rule is blocked. The proof cannot be completed, which is what soundness guarantees: the rules never prove something a countermodel refutes.

Example. What is wrong with this derivation of $\forall x F x$ from $\exists x F x$ : line 1 the premise, line 2 $F a$ from line 1 by $\exists$ E, line 3 $\forall x F x$ from line 2 by $\forall$ I?

Two things, and either alone is fatal. Line 2 misuses $\exists$ E, which does not simply produce a line with a name in it; it requires a subproof whose conclusion is free of the fresh name. And line 3 misuses $\forall$ I, since $a$ was introduced by an assumption still in force and so is not arbitrary. The result, that something being $F$ makes everything $F$ , is the standard demonstration of why both restrictions exist.

Now you. From $\exists x F x$ and $\exists x G x$ , is $\exists x (F x \land G x)$ derivable? If not, give a countermodel.

Answer

Not derivable, and it is invalid. Take the domain ${1, 2}$ with $F$ true of 1 only and $G$ true of 2 only. Both premises hold and the conclusion fails. Any attempted derivation must take a witness for each premise, and the freshness requirement forces two different names, which then cannot be conjoined into one claim.

Strategy

Quantifier proofs have a standard order of operations, and following it turns most exercises into bookkeeping.

Strip the quantifiers off the premises first. Universals come off by $\forall$ E, and the name to instantiate to should be chosen by looking at the conclusion, since instantiating to the wrong name is the usual reason a proof stalls. Existentials come off by opening an $\exists$ E subproof at once, with a name used nowhere else.

Then look at the conclusion and plan backwards. A universal conclusion means the proof will end with $\forall$ I, so aim at the matrix with an arbitrary name and check at the end that the name really was arbitrary. An existential conclusion means it will end with $\exists$ I, so aim at the matrix with any name you can get. A negated quantifier should be pushed inward with the laws of the ninth lesson before anything else, since $\neg \forall$ is unusable and the $\exists \neg$ it equals is not.

What the system is worth

The four rules, added to the propositional system of the seventh lesson, give a complete proof system for first-order logic. Gödel proved this in his doctoral dissertation of 1929, published in 1930: every valid first-order argument has a derivation. Soundness holds too, and by the same style of argument as before, checking each rule against the definition of truth in a model.

Completeness and undecidability sit side by side without conflict, and the combination is worth stating precisely because it is easy to garble. Every valid formula has a proof, and the proofs can be enumerated by machine, so a search will eventually find one if it exists. What no algorithm can do is tell you in advance, or after any finite time, whether the search is going to succeed. Validity is provable when it holds and not detectable when it fails.

One thing is still missing from the language, and it shows up in counting. Nothing so far can say that there are at least two things of some kind: $\exists x F x \land \exists y F y$ is satisfied by a single object named twice, because two variables may take the same value. Saying that two objects are different needs a predicate the notation does not yet have, and that is the next lesson.