Chapter 36 Basic rules for FOL
The language of FOL makes use of all of the connectives of TFL. So proofs in FOL will use all of the basic and derived rules from part IV. We will also use the prooftheoretic notions (particularly, the symbol ‘$\u22a2$’) introduced there. However, we will also need some new basic rules to govern the quantifiers, and to govern the identity sign.
36.1 Universal elimination
From the claim that everything is $F$, you can infer that any particular thing is $F$. You name it; it’s $F$. So the following should be fine:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xR(x,x,d)$

PR

$2$ 
0

$R(a,a,d)$

$\forall $E $1$

We obtained line $2$ by dropping the universal quantifier and replacing every instance of ‘$x$’ with ‘$a$’. Equally, the following should be allowed:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xR(x,x,d)$

PR

$2$ 
0

$R(d,d,d)$

$\forall $E $1$

We obtained line $2$ here by dropping the universal quantifier and replacing every instance of ‘$x$’ with ‘$d$’. We could have done the same with any other name we wanted.
This motivates the universal elimination rule ($\forall $E):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\forall $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\forall $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

The notation here was introduced in chapter 31. The point is that you can obtain any substitution instance of a universally quantified formula: replace every free occurrence of the quantified variable with any name you like.
We should emphasize that (as with every elimination rule) you can only apply the $\forall $E rule when the universal quantifier is the main logical operator. So the following is banned:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xB(x)\to B(k)$

PR

$2$ 
0

$B(b)\to B(k)$

naughy attempt to invoke $\forall $E $1$

This is illegitimate, since ‘$\forall x$’ is not the main logical operator in line $1$. (If you need a reminder as to why this sort of inference should be banned, reread chapter 24.)
36.2 Existential introduction
From the claim that some particular thing is $F$, you can infer that something is $F$. So we ought to allow:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R(a,a,d)$

PR

$2$ 
0

$\exists xR(a,a,x)$

$\exists $I $1$

Here, we have replaced the name ‘$d$’ with a variable ‘$x$’, and then existentially quantified over it. Equally, we would have allowed:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R(a,a,d)$

PR

$2$ 
0

$\exists xR(x,x,d)$

$\exists $I $1$

Here we have replaced both instances of the name ‘$a$’ with a variable, and then existentially generalized. But we do not need to replace both instances of a name with a variable: if Narcissus loves himself, then there is someone who loves Narcissus. So we also allow:
Line number

Subproof level

Formula

Justification


$1$ 
0

$R(a,a,d)$

PR

$2$ 
0

$\exists xR(x,a,d)$

$\exists $I $1$

Here we have replaced one instance of the name ‘$a$’ with a variable, and then existentially generalized. These observations motivate our introduction rule, although to explain it, we will need to introduce some new notation.
Where $\mathcal{A}$ is a sentence containing the name $\U0001d4b8$, we can emphasize this by writing ‘$\mathcal{A}(\mathrm{\dots}\U0001d4b8\mathrm{\dots}\U0001d4b8\mathrm{\dots})$’. We will write ‘$\mathcal{A}(\mathrm{\dots}\U0001d4cd\mathrm{\dots}\U0001d4b8\mathrm{\dots})$’ to indicate any formula obtained by replacing some or all of the instances of the name $\U0001d4b8$ with the variable $\U0001d4cd$ (provided $\U0001d4b8$, wherever it is replaced, does not occur in the scope of a quantifier binding $\U0001d4cd$). Armed with this, our introduction rule is:
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\exists $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\exists $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

36.3 Empty domains
The following proof combines our two new rules for quantifiers:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xF(x)$

PR

$2$ 
0

$F(a)$

$\forall $E $1$

$3$ 
0

$\exists xF(x)$

$\exists $I $2$

Could this be a bad proof? If anything exists at all, then certainly we can infer that something is $F$, from the fact that everything is $F$. But what if nothing exists at all? Then it is surely vacuously true that everything is $F$; however, it does not following that something is $F$, for there is nothing to be $F$. So if we claim that, as a matter of logic alone, ‘$\exists xF(x)$’ follows from ‘$\forall xF(x)$’, then we are claiming that, as a matter of logic alone, there is something rather than nothing. This might strike us as a bit odd.
Actually, we are already committed to this oddity. In chapter 23, we stipulated that domains in FOL must have at least one member. We then defined a validity (of FOL) as a sentence which is true in every interpretation. Since ‘$\exists xx=x$’ will be true in every interpretation, this also had the effect of stipulating that it is a matter of logic that there is something rather than nothing.
Since it is far from clear that logic should tell us that there must be something rather than nothing, we might well be cheating a bit here.
If we refuse to cheat, though, then we pay a high cost. Here are three things that we want to hold on to:

1.
$\forall xF(x)\u22a2F(a)$: after all, that was $\forall $E.

2.
$F(a)\u22a2\exists xF(x)$: after all, that was $\exists $I.

3.
the ability to copyandpaste proofs together: after all, reasoning works by putting lots of little steps together into rather big chains.
If we get what we want on all three counts, then we have to countenance that $\forall xF(x)\u22a2\exists xF(x)$. So, if we get what we want on all three counts, the proof system alone tells us that there is something rather than nothing. And if we refuse to accept that, then we have to surrender one of the three things that we want to hold on to!
Before we start thinking about which to surrender, we might want to ask how much of a cheat this is. Granted, it may make it harder to engage in theological debates about why there is something rather than nothing. But the rest of the time, we will get along just fine. So maybe we should just regard our proof system (and FOL, more generally) as having a very slightly limited purview. If we ever want to allow for the possibility of nothing, then we will have to cast around for a more complicated proof system. But for as long as we are content to ignore that possibility, our proof system is perfectly in order. (As, similarly, is the stipulation that every domain must contain at least one object.)
36.4 Universal introduction
Suppose you had shown of each particular thing that it is F (and that there are no other things to consider). Then you would be justified in claiming that everything is F. This would motivate the following proof rule. If you had established each and every single substitution instance of ‘$\forall xF(x)$’, then you can infer ‘$\forall xF(x)$’.
Unfortunately, that rule would be utterly unusable. To establish each and every single substitution instance would require proving ‘$F(a)$’, ‘$F(b)$’, …, ‘$F({j}_{2})$’, …, ‘$F({r}_{79002})$’, …, and so on. Indeed, since there are infinitely many names in FOL, this process would never come to an end. So we could never apply that rule. We need to be a bit more cunning in coming up with our rule for introducing universal quantification.
A solution will be inspired by considering:
This argument should obviously be valid. After all, alphabetical variation ought to be a matter of taste, and of no logical consequence. But how might our proof system reflect this? Suppose we begin a proof thus:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xF(x)$

PR

$2$ 
0

$F(a)$

$\forall $E $1$

We have proved ‘$F(a)$’. And, of course, nothing stops us from using the same justification to prove ‘$F(b)$’, ‘$F(c)$’, …, ‘$F({j}_{2})$’, …, ‘$F({r}_{79002})$, …, and so on until we run out of space, time, or patience. But reflecting on this, we see that there is a way to prove $F(\U0001d4b8)$, for any name $\U0001d4b8$. And if we can do it for any thing, we should surely be able to say that ‘$F$’ is true of everything. This therefore justifies us in inferring ‘$\forall yF(y)$’, thus:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xF(x)$

PR

$2$ 
0

$F(a)$

$\forall $E $1$

$3$ 
0

$\forall yF(y)$

$\forall $I $2$

The crucial thought here is that ‘$a$’ was just some arbitrary name. There was nothing special about it—we might have chosen any other name—and still the proof would be fine. And this crucial thought motivates the universal introduction rule ($\forall $I):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$


0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\forall $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\forall $}$I $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$

where the name $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}$ must not occur in a premise or an undischarged assumption.
In section 31.3, we introduced a convention for indicating substitution instances: We said that if $\mathcal{A}(\mathrm{\dots}\U0001d4cd\mathrm{\dots}\U0001d4cd\mathrm{\dots})$ is a formula, then $\mathcal{A}(\mathrm{\dots}\U0001d4b8\mathrm{\dots}\U0001d4b8\mathrm{\dots})$ is the result of replacing every free occurrence of $\U0001d4cd$ in $\mathcal{A}$ by $\U0001d4b8$. To state our $\forall $I rule, we are using the same convention, except in the other direction: If $\mathcal{A}(\mathrm{\dots}\U0001d4b8\mathrm{\dots}\U0001d4b8\mathrm{\dots})$ is a formula, then $\mathcal{A}(\mathrm{\dots}\U0001d4cd\mathrm{\dots}\U0001d4cd\mathrm{\dots})$ is the result of replacing every occurrence of $\U0001d4b8$ in it by $\U0001d4cd$. (This is only allowed as long as $\U0001d4b8$ does not occur in the scope of a quantifier binding $\U0001d4cd$ in $\mathcal{A}$.)
There are a two important things to watch out for in applying the $\forall $I rule. If we are not careful with the choice of name $\U0001d4b8$ and its replacement by $\U0001d4cd$ we are at risk of making some incorrect inferences.
The constraint on the $\forall $I rule requires that $\U0001d4b8$ must not occur in a premise or an undischarged assumption. This constraint ensures that we are always reasoning at a sufficiently general level. To see the constraint in action, consider this terrible argument:

Everyone loves Kylie Minogue.

∴
Everyone loves themselves.
We might symbolize this obviously invalid inference pattern as:
Now, suppose we tried to offer a proof that vindicates this argument:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xL(x,k)$

PR

$2$ 
0

$L(k,k)$

$\forall $E $1$

$3$ 
0

$\forall xL(x,x)$

naughty attempt to invoke $\forall $I $2$

This is not allowed, because ‘$k$’ occurred already in a premise, namely, on line $1$. The crucial point is that, if we have made any assumptions about the object we are working with, then we are not reasoning generally enough to license $\forall $I.
Although the name may not occur in any undischarged assumption, it may occur in a discharged assumption. That is, it may occur in a subproof that we have already closed. For example, this is just fine:
Line number

Subproof level

Formula

Justification


$1$ 
open subproof,
1

$G(d)$

AS

$2$ 
1

$G(d)$

R $1$

$3$ 
close subproof,
0

$G(d)\to G(d)$

$\to $I $1$–$2$

$4$ 
0

$\forall z(G(z)\to G(z))$

$\forall $I $3$

This tells us that ‘$\forall z(G(z)\to G(z))$’ is a theorem. And that is as it should be.
If we only replace some names and not others, we end up ‘proving’ silly things. For example, consider the argument:

Everyone is as old as themselves.

∴
Everyone is as old as Judi Dench.
We might symbolize this as follows:
But now suppose we tried to vindicate this terrible argument with the following:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xO(x,x)$

PR

$2$ 
0

$O(d,d)$

$\forall $E $1$

$3$ 
0

$\forall xO(x,d)$

naughty attempt to invoke $\forall $I $2$

Fortunately, our rules do not allow us to do this: the attempted proof is banned, since it doesn’t replace every occurrence of ‘$d$’ in line $2$ with an ‘$x$’.
36.5 Existential elimination
Suppose we know that something is $F$. The problem is that simply knowing this does not tell us which thing is $F$. So it would seem that from ‘$\exists xF(x)$’ we cannot immediately conclude ‘$F(a)$’, ‘$F({e}_{23})$’, or any other substitution instance of the sentence. What can we do?
Suppose we know that something is $F$, and that everything which is $F$ is also $G$. In (almost) natural English, we might reason thus:
Since something is $F$, there is some particular thing which is an $F$. We do not know anything about it, other than that it’s an $F$, but for convenience, let’s call it ‘Becky’. So: Becky is $F$. Since everything which is $F$ is $G$, it follows that Becky is $G$. But since Becky is $G$, it follows that something is $G$. And nothing depended on which object, exactly, Becky was. So, something is $G$.
We might try to capture this reasoning pattern in a proof as follows:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\exists xF(x)$

PR

$2$ 
0

$\forall x(F(x)\to G(x))$

PR

$3$ 
open subproof,
1

$F(b)$

AS

$4$ 
1

$F(b)\to G(b)$

$\forall $E $2$

$5$ 
1

$G(b)$

$\to $E $4$, $3$

$6$ 
1

$\exists xG(x)$

$\exists $I $5$

$7$ 
close subproof,
0

$\exists xG(x)$

$\exists $E $1$, $3$–$6$

Breaking this down: we started by writing down our assumptions. At line $3$, we made an additional assumption: ‘$F(b)$’. This was just a substitution instance of ‘$\exists xF(x)$’. On this assumption, we established ‘$\exists xG(x)$’. Note that we had made no special assumptions about the object named by ‘$b$’; we had only assumed that it satisfies ‘$F(x)$’. So nothing depends upon which object it is. And line $1$ told us that something satisfies ‘$F(x)$’, so our reasoning pattern was perfectly general. We can discharge the specific assumption ‘$F(b)$’, and simply infer ‘$\exists xG(x)$’ on its own.
Putting this together, we obtain the existential elimination rule ($\exists $E):
Line number

Subproof level

Formula

Justification


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$ 
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\exists $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$


$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$ 
open subproof,
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$

AS

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$ 
1

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$


close subproof,
0

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\exists $}$E $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$m$}$, $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$–$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$j$}$

$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}$ must not occur in any assumption undischarged before line $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$i$}$
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}$ must not occur in $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\exists $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4cd$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\dots}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$
$\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\U0001d4b8$}$ must not occur in $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$
As with universal introduction, the constraints are extremely important. To see why, consider the following terrible argument:

Tim Button is a lecturer.

Someone is not a lecturer.

∴
Tim Button is both a lecturer and not a lecturer.
We might symbolize this obviously invalid inference pattern as follows:
Now, suppose we tried to offer a proof that vindicates this argument:
Line number

Subproof level

Formula

Justification


$1$ 
0

$L(b)$

PR

$2$ 
0

$\exists x\mathrm{\neg}L(x)$

PR

$3$ 
open subproof,
1

$\mathrm{\neg}L(b)$

AS

$4$ 
1

$L(b)\wedge \mathrm{\neg}L(b)$

$\wedge $I $1$, $3$

$5$ 
close subproof,
0

$L(b)\wedge \mathrm{\neg}L(b)$

naughty attempt
to invoke $\exists $E $2$, $3$–$4$

The last line of the proof is not allowed. The name that we used in our substitution instance for ‘$\exists x\mathrm{\neg}L(x)$’ on line $3$, namely ‘$b$’, occurs in line $4$. This would be no better:
Line number

Subproof level

Formula

Justification


$1$ 
0

$L(b)$

PR

$2$ 
0

$\exists x\mathrm{\neg}L(x)$

PR

$3$ 
open subproof,
1

$\mathrm{\neg}L(b)$

AS

$4$ 
1

$L(b)\wedge \mathrm{\neg}L(b)$

$\wedge $I $1$, $3$

$5$ 
1

$\exists x(L(x)\wedge \mathrm{\neg}L(x))$

$\exists $I $4$

$6$ 
close subproof,
0

$\exists x(L(x)\wedge \mathrm{\neg}L(x))$

naughty attempt to invoke $\exists $E $2$, $3$–$5$

The last line is still not allowed. For the name that we used in our substitution instance for ‘$\exists x\mathrm{\neg}L(x)$’, namely ‘$b$’, occurs in an undischarged assumption, namely line $1$.
Finally, consider this ‘proof’:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\exists xL(a,x)$

PR

$2$ 
open subproof,
1

$L(a,a)$

AS

$3$ 
1

$\exists xL(x,x)$

$\exists $I $2$

$4$ 
close subproof,
0

$\exists xL(x,x)$

naughty attempt to invoke $\exists $E $1$, $2$–$3$

Here the name ‘$a$’ violates the second condition of the $\exists $E rule: it occurs in ‘$\exists xL(a,x)$’ on line $1$. And we have to prevent this from being a proof, since it is invalid: ‘Someone likes themselves’ does not follow from ‘Alex likes someone’.
The moral of the story is this. If you want to squeeze information out of an existential quantifier, choose a new name for your substitution instance. That way, you can guarantee that you meet all the constraints on the rule for $\exists $E.
36.6 Quantifier rules and vacuous quantification
There is a subtle issue in our quantifier rules that has to do with an aspect of the way we have specified the rules of our syntax, namely the possibility of vacuous quantification (see the end of section 27.3). In sections 36.1 and 36.5 we made use of the substitution notation of chapter 31: $\mathcal{A}(\mathrm{\dots}\U0001d4b8\mathrm{\dots}\U0001d4b8\mathrm{\dots})$ is the formula obtained by replacing every free occurrence of $\U0001d4cd$ in $\mathcal{A}$ with $\U0001d4b8$. Here, we emphasize the ‘free’ for a reason. It means you cannot always replace every occurrence of $\U0001d4cd$. For instance, this would be incorrect:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall x(F(x)\wedge \exists xG(x))$

PR

$2$ 
0

$F(a)\wedge \exists xG(a)$

naughty attempt to invoke $\forall $E $1$

On line $2$, we have formed the substitution instance incorrectly: we replaced the ‘$x$’ in both ‘$F(x)$’ and in ‘$G(x)$’ by ‘$a$’, but only the first one is a free occurrence—the other one is bound by ‘$\exists x$’. Not only would this violate a restriction on substitution, it would allow us to ‘prove’ an invalid argument. Since ‘$\exists xG(a)$’ is a case of vacuous quantification, it is equivalent to just ‘$G(a)$’. Furthermore, line $1$ is equivalent to ‘$\forall x(F(x)\wedge \exists yG(y))$’. It should be easy to see that this does not entail ‘$F(a)\wedge G(a)$’. You’re unlikely to encounter such a case (unless you have a devious instructor): your exercises will likely only involve sentences like ‘$\forall x(F(x)\wedge \exists yG(y))$’, with variables nicely kept separate.
In section 36.2, we said that we use ‘$\mathcal{A}(\mathrm{\dots}\U0001d4cd\mathrm{\dots}\U0001d4b8\mathrm{\dots})$’ to indicate any formula obtained by replacing some or all of the instances of the name $\U0001d4b8$ with the variable $\U0001d4cd$ provided $\U0001d4b8$, wherever it is replaced, does not occur in the scope of a quantifier binding $\U0001d4cd$. The emphasized restriction prohibiting the replacement of $\U0001d4b8$ in some cases is somewhat subtle. You probably will never find yourself in a situation where you run the risk of violating it. But it is needed to make the rule correct. Since we allow vacuous quantification, for instance, ‘$\exists x\forall xL(x,x)$’ is a legal sentence of FOL. It’s just that in it, the first ‘$\exists x$’ doesn’t do any work, and the sentence is equivalent to just ‘$\forall xL(x,x)$’. Now, ‘$\forall xL(x,x)$’ could be obtained from ‘$\forall xL(a,x)$’ by replacing the name ‘$a$’ by the variable ‘$x$’ if we weren’t careful and overlooked that here ‘$a$’ does occur in the scope of ‘$\forall x$’. Without the restriction, the following would then be allowed:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xL(a,x)$

PR

$2$ 
0

$\exists x\forall xL(x,x)$

naughty attempt to invoke $\exists $I $1$

But since ‘$\exists x\forall xL(x,x)$’ is equivalent to just ‘$\forall xL(x,x)$’, this would be an invalid inference. To see why, read ‘$L$’ as ‘likes’: From ‘Alex likes everyone’ it does not follow that everyone likes everyone.
Similarly, in section 36.4, we said that $\mathcal{A}(\mathrm{\dots}\U0001d4cd\mathrm{\dots}\U0001d4cd\mathrm{\dots})$ is the result of replacing every occurrence of $\U0001d4b8$ in $\mathcal{A}(\mathrm{\dots}\U0001d4b8\mathrm{\dots}\U0001d4b8\mathrm{\dots})$ by $\U0001d4cd$, but that this is only allowed as long as $\U0001d4b8$ does not occur in the scope of a quantifier binding $\U0001d4cd$ in $\mathcal{A}$. Like the constraint involved in the statement of the $\exists $I rule, it does not often happen that you’d risk violating it in practice. But here’s why it’s important. Again, since we allow vacuous quantification, ‘$\forall x\exists xL(x,x)$’ is a legal sentence of FOL. However, ‘$\forall x\exists xL(x,x)$’ can be obtained from ‘$\forall xL(a,x)$’ by replacing the name ‘$a$’ by the variable ‘$x$’ everywhere. This violates the restriction we included, though: ‘$a$’ does occur in the scope of ‘$\forall x$’ in this case. Without the restriction, the following would be allowed:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall y\exists xL(y,x)$

PR

$2$ 
0

$\exists xL(a,x)$

$\forall $E $1$

$3$ 
0

$\forall x\exists xL(x,x)$

naughty attempt to invoke $\forall $I $2$

But since ‘$\forall x\exists xL(x,x)$’ is equivalent to just ‘$\exists xL(x,x)$’, this would be an invalid inference: ‘Someone likes themselves’ does not follow from ‘Everyone likes someone’.
Practice exercises
A. Explain why these two ‘proofs’ are incorrect. Also, provide interpretations which would invalidate the fallacious argument forms the ‘proofs’ enshrine:
Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall xR(x,x)$

PR

$2$ 
0

$R(a,a)$

$\forall $E $1$

$3$ 
0

$\forall yR(a,y)$

$\forall $I $2$

$4$ 
0

$\forall x\forall yR(x,y)$

$\forall $I $3$

Line number

Subproof level

Formula

Justification


$1$ 
0

$\forall x\exists yR(x,y)$

PR

$2$ 
0

$\exists yR(a,y)$

$\forall $E $1$

$3$ 
open subproof,
1

$R(a,a)$

AS

$4$ 
1

$\exists xR(x,x)$

$\exists $I $3$

$5$ 
close subproof,
0

$\exists xR(x,x)$

$\exists $E $2$, $3$–$4$

B. The following three proofs are missing their citations (rule and line numbers). Add them, to turn them into bona fide proofs.

1.Line numberSubproof levelFormulaJustification
$1$ 0$\forall x\exists y(R(x,y)\vee R(y,x))$$2$ 0$\forall x\mathrm{\neg}R(m,x)$$3$ 0$\exists y(R(m,y)\vee R(y,m))$$4$ open subproof, 1$R(m,a)\vee R(a,m)$$5$ 1$\mathrm{\neg}R(m,a)$$6$ 1$R(a,m)$$7$ 1$\exists xR(x,m)$$8$ close subproof, 0$\exists xR(x,m)$ 
2.Line numberSubproof levelFormulaJustification
$1$ 0$\forall x(\exists yL(x,y)\to \forall zL(z,x))$$2$ 0$L(a,b)$$3$ 0$\exists yL(a,y)\to \forall zL(z,a)$$4$ 0$\exists yL(a,y)$$5$ 0$\forall zL(z,a)$$6$ 0$L(c,a)$$7$ 0$\exists yL(c,y)\to \forall zL(z,c)$$8$ 0$\exists yL(c,y)$$9$ 0$\forall zL(z,c)$$10$ 0$L(c,c)$$11$ 0$\forall xL(x,x)$ 
3.Line numberSubproof levelFormulaJustification
$1$ 0$\forall x(J(x)\to K(x))$$2$ 0$\exists x\forall yL(x,y)$$3$ 0$\forall xJ(x)$$4$ open subproof, 1$\forall yL(a,y)$$5$ 1$L(a,a)$$6$ 1$J(a)$$7$ 1$J(a)\to K(a)$$8$ 1$K(a)$$9$ 1$K(a)\wedge L(a,a)$$10$ 1$\exists x(K(x)\wedge L(x,x))$$11$ close subproof, 0$\exists x(K(x)\wedge L(x,x))$
C. In exercise 24A, we considered fifteen syllogistic figures of Aristotelian logic. Provide proofs for each of the argument forms. NB: You will find it much easier if you symbolize (for example) ‘No F is G’ as ‘$\forall x(F(x)\to \mathrm{\neg}G(x))$’.
D. Aristotle and his successors identified other syllogistic forms which depended upon ‘existential import’. Symbolize each of these argument forms in FOL and offer proofs.

1.
Barbari. Something is H. All G are F. All H are G. So: Some H is F.

2.
Celaront. Something is H. No G are F. All H are G. So: Some H is not F.

3.
Cesaro. Something is H. No F are G. All H are G. So: Some H is not F.

4.
Camestros. Something is H. All F are G. No H are G. So: Some H is not F.

5.
Felapton. Something is G. No G are F. All G are H. So: Some H is not F.

6.
Darapti. Something is G. All G are F. All G are H. So: Some H is F.

7.
Calemos. Something is H. All F are G. No G are H. So: Some H is not F.

8.
Fesapo. Something is G. No F is G. All G are H. So: Some H is not F.

9.
Bamalip. Something is F. All F are G. All G are H. So: Some H are F.
E. For each of the following claims, provide an FOL proof that shows it is true.

1.
$\u22a2\forall xF(x)\to \forall y(F(y)\wedge F(y))$

2.
$\forall x(A(x)\to B(x)),\exists xA(x)\u22a2\exists xB(x)$

3.
$\forall x(M(x)\leftrightarrow N(x)),M(a)\wedge \exists xR(x,a)\u22a2\exists xN(x)$

4.
$\forall x\forall yG(x,y)\u22a2\exists xG(x,x)$

5.
$\u22a2\forall xR(x,x)\to \exists x\exists yR(x,y)$

6.
$\u22a2\forall y\exists x(Q(y)\to Q(x))$

7.
$N(a)\to \forall x(M(x)\leftrightarrow M(a)),M(a),\mathrm{\neg}M(b)\u22a2\mathrm{\neg}N(a)$

8.
$\forall x\forall y(G(x,y)\to G(y,x))\u22a2\forall x\forall y(G(x,y)\leftrightarrow G(y,x))$

9.
$\forall x(\mathrm{\neg}M(x)\vee L(j,x)),\forall x(B(x)\to L(j,x)),\forall x(M(x)\vee B(x))\u22a2\forall xL(j,x)$
F. Write a symbolization key for the following argument, symbolize it, and prove it:

There is someone who likes everyone who likes everyone that she likes.

∴
There is someone who likes herself.
G. Show that each pair of sentences is provably equivalent.

1.
$\forall x(A(x)\to \mathrm{\neg}B(x))$, $\mathrm{\neg}\exists x(A(x)\wedge B(x))$

2.
$\forall x(\mathrm{\neg}A(x)\to B(d))$, $\forall xA(x)\vee B(d)$

3.
$\exists xP(x)\to Q(c)$, $\forall x(P(x)\to Q(c))$
H. For each of the following pairs of sentences: If they are provably equivalent, give proofs to show this. If they are not, construct an interpretation to show that they are not logically equivalent.

1.
$\forall xP(x)\to Q(c),\forall x(P(x)\to Q(c))$

2.
$\forall x\forall y\forall zB(x,y,z),\forall xB(x,x,x)$

3.
$\forall x\forall yD(x,y),\forall y\forall xD(x,y)$

4.
$\exists x\forall yD(x,y),\forall y\exists xD(x,y)$

5.
$\forall x(R(c,a)\leftrightarrow R(x,a)),R(c,a)\leftrightarrow \forall xR(x,a)$
I. For each of the following arguments: If it is valid in FOL, give a proof. If it is invalid, construct an interpretation to show that it is invalid.

1.
$\exists y\forall xR(x,y)\therefore \forall x\exists yR(x,y)$

2.
$\forall x\exists yR(x,y)\therefore \exists y\forall xR(x,y)$

3.
$\exists x(P(x)\wedge \mathrm{\neg}Q(x))\therefore \forall x(P(x)\to \mathrm{\neg}Q(x))$

4.
$\forall x(S(x)\to T(a)),S(d)\therefore T(a)$

5.
$\forall x(A(x)\to B(x)),\forall x(B(x)\to C(x))\therefore \forall x(A(x)\to C(x))$

6.
$\exists x(D(x)\vee E(x)),\forall x(D(x)\to F(x))\therefore \exists x(D(x)\wedge F(x))$

7.
$\forall x\forall y(R(x,y)\vee R(y,x))\therefore R(j,j)$

8.
$\exists x\exists y(R(x,y)\vee R(y,x))\therefore R(j,j)$

9.
$\forall xP(x)\to \forall xQ(x),\exists x\mathrm{\neg}P(x)\therefore \exists x\mathrm{\neg}Q(x)$

10.
$\exists xM(x)\to \exists xN(x)$, $\mathrm{\neg}\exists xN(x)\therefore \forall x\mathrm{\neg}M(x)$