forallx-yyc-prooffol.tex

%!TEX root = forallxyyc.tex
\part{Natural deduction for FOL}
\label{ch.NDFOL}
\addtocontents{toc}{\protect\mbox{}\protect\hrulefill\par}

\chapter{Basic rules for FOL}\label{s:BasicFOL}

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 \cref{ch.NDTFL}. We will also use the proof-theoretic notions (particularly, the symbol `$\proves$') introduced there. However, we will also need some new basic rules to govern the quantifiers, and to govern the identity sign.


\section{Universal elimination}\label{s:forallElim}

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:
\begin{fitchproof}
	\hypo{a}{\forall x\,\atom{R}{x,x,d}}\PR
	\have{c}{\atom{R}{a,a,d}} \Ae{a}
\end{fitchproof}
We obtained line~$2$ by dropping the universal quantifier and replacing every instance of `$x$' with `$a$'. Equally, the following should be allowed:
\begin{fitchproof}
	\hypo{a}{\forall x\,\atom{R}{x,x,d}}\PR
	\have{c}{\atom{R}{d,d,d}} \Ae{a}
\end{fitchproof}
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):

\factoidbox{
\begin{fitchproof}
	\have[m]{a}{\forall \metav{x}\,\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)}
	\have[\ ]{c}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)} \Ae{a}
\end{fitchproof}}

The notation here was introduced in \cref{s:TruthFOL}. The point is
that you can obtain any \emph{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 \emph{banned}:
\begin{fitchproof}
	\hypo{a}{\forall x\,\atom{B}{x} \eif \atom{B}{k}}\PR
	\have{c}{\atom{B}{b} \eif \atom{B}{k}}\by{naughy attempt to invoke $\forall$E}{a}
\end{fitchproof}
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 \cref{s:MoreMonadic}.)

\section{Existential introduction}\label{s:existsIntro}

From the claim that some particular thing is~$F$, you can infer that something is~$F$. So we ought to allow:
\begin{fitchproof}
	\hypo{a}{\atom{R}{a,a,d}}\PR
	\have{b}{\exists x\, \atom{R}{a,a,x}} \Ei{a}
\end{fitchproof}
Here, we have replaced the name `$d$' with a variable `$x$', and then existentially quantified over it. Equally, we would have allowed:
\begin{fitchproof}
	\hypo{a}{\atom{R}{a,a,d}}\PR
	\have{c}{\exists x\, \atom{R}{x,x,d}} \Ei{a}
\end{fitchproof}
Here we have replaced both instances of the name `$a$' with a variable, and then existentially generalized. But we do not need to replace \emph{both} instances of a name with a variable: if Narcissus loves himself, then there is someone who loves Narcissus. So we also allow:
\begin{fitchproof}
	\hypo{a}{\atom{R}{a,a,d}}\PR
	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
\end{fitchproof}
Here we have replaced \emph{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 $\metav{A}$ is a sentence containing the name $\metav{c}$, we
can emphasize this by writing `$\metav{A}(\ldots \metav{c} \ldots
\metav{c}\ldots)$'. We will write `$\metav{A}(\ldots \metav{x} \ldots
\metav{c}\ldots)$' to indicate any formula obtained by replacing
\emph{some or all} of the instances of the name \metav{c} with the
variable~\metav{x} (provided~$\metav{c}$, wherever it is
replaced, does not occur in the scope of a quantifier
binding~$\metav{x}$). Armed with this, our introduction rule is:
\factoidbox{
\begin{fitchproof}
	\have[m]{a}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}
	\have[\ ]{c}{\exists \metav{x}\,\metav{A}(\ldots \metav{x} \ldots \metav{c}\ldots)} \Ei{a}
\end{fitchproof}
%\metav{x} must not occur in $\metav{A}(\ldots \metav{c} \ldots
%\metav{c}\ldots)$
}
% The constraint is included to guarantee that any application of the rule yields a  sentence of FOL. Thus the following is allowed:
% \begin{fitchproof}
% 	\hypo{a}{\atom{R}{a,a,d}}
% 	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
% 	\have{e}{\exists y \exists x\, \atom{R}{x,y,d}} \Ei{d}
% \end{fitchproof}
% But this is banned:
% \begin{fitchproof}
% 	\hypo{a}{\atom{R}{a,a,d}}
% 	\have{d}{\exists x\, \atom{R}{x,a,d}} \Ei{a}
% 	\have{e}{\exists x\, \exists x\, \atom{R}{x,x,d}}\by{naughty attempt to invoke $\exists$I}{d}
% \end{fitchproof}
% since the expression on line~3 contains clashing variables, and so is not a sentence of FOL.

\section{Empty domains}
The following proof combines our two new rules for quantifiers:
	\begin{fitchproof}
		\hypo{a}{\forall x\, \atom{F}{x}}\PR
		\have{in}{\atom{F}{a}}\Ae{a}
		\have{e}{\exists x\, \atom{F}{x}}\Ei{in}
	\end{fitchproof}
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 \emph{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 \emph{be}~$F$. So if we claim that, as a matter of logic alone, `$\exists x\,\atom{F}{x}$' follows from `$\forall x\,\atom{F}{x}$', then we are claiming that, as a matter of \emph{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 \cref{s:FOLBuildingBlocks}, 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 x\, x=x$' will be true in every interpretation, this \emph{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:
	\begin{compactlist}
		\item $\forall x\,\atom{F}{x} \proves \atom{F}{a}$: after all, that was $\forall$E.
		\item $\atom{F}{a} \proves \exists x\,\atom{F}{x}$: after all, that was $\exists$I.
		\item the ability to copy-and-paste proofs together: after all, reasoning works by putting lots of little steps together into rather big chains.
	\end{compactlist}
If we get what we want on all three counts, then we have to countenance that $\forall x\,\atom{F}{x} \proves \exists x\,\atom{F}{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 \emph{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 \emph{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.)

\section{Universal introduction}\label{s:forallIntro}

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 x\,\atom{F}{x}$', then you can infer `$\forall x\,\atom{F}{x}$'.

Unfortunately, that rule would be utterly unusable. To establish each and every single substitution instance would require proving `$\atom{F}{a}$', `$\atom{F}{b}$', \dots, `$\atom{F}{j_2}$', \dots, `$\atom{F}{r_{79002}}$', \ldots, 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:
$$\forall x\,\atom{F}{x} \therefore \forall y\,\atom{F}{y}$$
This argument should \emph{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:
\begin{fitchproof}
	\hypo{x}{\forall x\, \atom{F}{x}} \PR
	\have{a}{\atom{F}{a}} \Ae{x}
\end{fitchproof}
We have proved `$\atom{F}{a}$'. And, of course, nothing stops us from using the same justification to prove `$\atom{F}{b}$', `$\atom{F}{c}$', \ldots, `$\atom{F}{j_2}$', \ldots, `$\atom{F}{r_{79002}}$, \dots, 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 $\atom{F}{\metav{c}}$, for any name~\metav{c}. And if we can do it for \emph{any} thing, we should surely be able to say that `$F$' is true of \emph{everything}. This therefore justifies us in inferring `$\forall y\,\atom{F}{y}$', thus:
\begin{fitchproof}
	\hypo{x}{\forall x\, \atom{F}{x}}\PR
	\have{a}{\atom{F}{a}} \Ae{x}
	\have{y}{\forall y\, \atom{F}{y}} \Ai{a}
\end{fitchproof}
The crucial thought here is that `$a$' was just some \emph{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):
\factoidbox{
\begin{fitchproof}
	\have[m]{a}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}
	\have[\ ]{c}{\forall \metav{x}\,\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)} \Ai{a}
\end{fitchproof}
where the name \metav{c} must not occur in a premise or an undischarged
assumption.%\\ 
%\metav{x} must not occur in $\metav{A}(\ldots \metav{c} \ldots
%\metav{c}\ldots)$
}

In \cref{s:MainLogicalOperatorQuantifier}, we introduced a convention
for indicating \emph{substitution instances}: We said that if
$\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)$ is a formula,
then $\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)$ is the
result of replacing \emph{every} free occurrence of $\metav{x}$ in
$\metav{A}$ by~$\metav{c}$. To state our $\forall$I rule, we are using
the same convention, except in the other direction: If
$\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)$ is a formula,
then $\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)$ is the
result of replacing \emph{every} occurrence of~$\metav{c}$ in it
by~$\metav{x}$. (This is only allowed as long as $\metav{c}$ does not
occur in the scope of a quantifier binding~$\metav{x}$ in~$\metav{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~$\metav{c}$ and its replacement by~$\metav{x}$ we are at risk of
making some incorrect inferences.

The constraint on the $\forall$I rule requires that \metav{c} must not
occur in a premise or an undischarged assumption. This constraint
ensures that we are always reasoning at a sufficiently general level.
%\footnote{Recall from \cref{s:BasicTFL} that we are treating `$\ered$' as a canonical contradiction. But if it were the canonical contradiction as involving some \emph{constant}, it might interfere with the constraint mentioned here. To avoid such problems, we will treat `$\ered$' as a canonical contradiction \emph{that involves no particular names}.} 
To see the constraint in action, consider this terrible argument:
	\begin{earg}
		\item Everyone loves Kylie Minogue.
		\item[\texttherefore] Everyone loves themselves.
	\end{earg}
We might symbolize this obviously invalid inference pattern as:
$$\forall x\,\atom{L}{x,k} \therefore \forall x\,\atom{L}{x,x}$$
Now, suppose we tried to offer a proof that vindicates this argument:
\begin{fitchproof}
	\hypo{x}{\forall x\, \atom{L}{x,k}}\PR
	\have{a}{\atom{L}{k,k}} \Ae{x}
	\have{y}{\forall x\, \atom{L}{x,x}} \by{naughty attempt to invoke $\forall$I}{a}
\end{fitchproof}
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 \emph{undischarged} assumption, it may occur in a \emph{discharged} assumption. That is, it may occur in a subproof that we have already closed. For example, this is just fine:
\begin{fitchproof}
	\open
		\hypo{f1}{\atom{G}{d}}\AS
		\have{f2}{\atom{G}{d}}\by{R}{f1}
	\close
	\have{ff}{\atom{G}{d} \eif \atom{G}{d}}\ci{f1-f2}
	\have{zz}{\forall z(\atom{G}{z} \eif \atom{G}{z})}\Ai{ff}
\end{fitchproof}
This tells us that `$\forall z (\atom{G}{z} \eif \atom{G}{z})$' is a \emph{theorem}. And that is as it should be.

If we only replace \emph{some} names and not others, we end up
`proving' silly things. For example, consider the argument:
	\begin{earg}
	\item Everyone is as old as themselves.
	\item[\texttherefore] Everyone is as old as Judi Dench.
	\end{earg}
We might symbolize this as follows:
$$\forall x\,\atom{O}{x,x} \therefore \forall x\,\atom{O}{x,d}$$
But now suppose we tried to vindicate this terrible argument with the following:
\begin{fitchproof}
	\hypo{x}{\forall x\, \atom{O}{x,x}}\PR
	\have{a}{\atom{O}{d,d}}\Ae{x}
	\have{y}{\forall x\, \atom{O}{x,d}}\by{naughty attempt to invoke $\forall$I}{a}
\end{fitchproof}
Fortunately, our rules do not allow us to do this: the attempted proof
is banned, since it doesn't replace \emph{every} occurrence of `$d$'
in line $2$ with an~`$x$'.

\section{Existential elimination}\label{s:existsElim}

Suppose we know that \emph{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 x\,\atom{F}{x}$' we cannot immediately conclude `$\atom{F}{a}$', `$\atom{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:
	\begin{quote}
		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$.
	\end{quote}
We might try to capture this reasoning pattern in a proof as follows:
\begin{fitchproof}
	\hypo{es}{\exists x\, \atom{F}{x}}\PR
	\hypo{ast}{\forall x(\atom{F}{x} \eif \atom{G}{x})}\PR
	\open
		\hypo{s}{\atom{F}{b}}\AS
		\have{st}{\atom{F}{b} \eif \atom{G}{b}}\Ae{ast}
		\have{t}{\atom{G}{b}} \ce{st, s}
		\have{et1}{\exists x\, \atom{G}{x}}\Ei{t}
	\close
	\have{et2}{\exists x\, \atom{G}{x}}\Ee{es,s-et1}
\end{fitchproof}\noindent
Breaking this down: we started by writing down our assumptions. At line~$3$, we made an additional assumption: `$\atom{F}{b}$'. This was just a substitution instance of `$\exists x\,\atom{F}{x}$'. On this assumption, we established `$\exists x\,\atom{G}{x}$'. Note that we had made no \emph{special} assumptions about the object named by `$b$'; we had \emph{only} assumed that it satisfies `$\atom{F}{x}$'. So nothing depends upon which object it is. And line~$1$ told us that \emph{something} satisfies `$\atom{F}{x}$', so our reasoning pattern was perfectly general. We can discharge the specific assumption `$\atom{F}{b}$', and simply infer `$\exists x\,\atom{G}{x}$' on its own.

Putting this together, we obtain the existential elimination rule ($\exists$E):
\factoidbox{
\begin{fitchproof}
	\have[m]{a}{\exists \metav{x}\,\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)}
	\open	
		\hypo[i]{b}{\metav{A}(\ldots \metav{c} \ldots \metav{c}\ldots)}\AS
		\have[j]{c}{\metav{B}}
	\close
	\have[\ ]{d}{\metav{B}} \Ee{a,b-c}
\end{fitchproof}
\metav{c} must not occur in any assumption undischarged before line $i$\\
\metav{c} must not occur in $\exists \metav{x}\,\metav{A}(\ldots \metav{x} \ldots \metav{x}\ldots)$\\
\metav{c} must not occur in \metav{B}}
As with universal introduction, the constraints are extremely important. To see why, consider the following terrible argument:
	\begin{earg}
		\item Tim Button is a lecturer. 
		\item Someone is not a lecturer. 
		\item[\texttherefore] Tim Button is both a lecturer and not a lecturer.
	\end{earg}
We might symbolize this obviously invalid inference pattern as follows:
$$\atom{L}{b}, \exists x\, \enot\atom{L}{x} \therefore \atom{L}{b} \eand \enot \atom{L}{b}$$
Now, suppose we tried to offer a proof that vindicates this argument:
\begin{fitchproof}
	\hypo{f}{\atom{L}{b}}\PR
	\hypo{nf}{\exists x\, \enot \atom{L}{x}}\PR
	\open
		\hypo{na}{\enot \atom{L}{b}}\AS
		\have{con}{\atom{L}{b} \eand \enot \atom{L}{b}}\ai{f, na}
	\close
\ifHTMLtarget
	\have{econ1}{\atom{L}{b} \eand \enot \atom{L}{b}}\by{naughty attempt
	to invoke $\exists$E }{nf, na-con}
\else
	\have{econ1}{\atom{L}{b} \eand \enot \atom{L}{b}}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\exists$E }{nf, na-con}
\fi
\end{fitchproof}
The last line of the proof is not allowed. The name that we used in our substitution instance for `$\exists x\, \enot \atom{L}{x}$' on line~$3$, namely `$b$', occurs in line~$4$. This would be no better:
\begin{fitchproof}
	\hypo{f}{\atom{L}{b}}\PR
	\hypo{nf}{\exists x\, \enot \atom{L}{x}}\PR
	\open
		\hypo{na}{\enot \atom{L}{b}}\AS
		\have{con}{\atom{L}{b} \eand \enot \atom{L}{b}}\ai{f, na}
		\have{con1}{\exists x (\atom{L}{x} \eand \enot \atom{L}{x})}\Ei{con}		
	\close
\ifHTMLtarget
	\have{econ1}{\exists x (\atom{L}{x} \eand \enot
	\atom{L}{x})}\by{naughty attempt to invoke $\exists$E }{nf, na-con1}
\else
	\have{econ1}{\exists x (\atom{L}{x} \eand \enot \atom{L}{x})}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\exists$E }{nf, na-con1}
\fi
\end{fitchproof}
The last line is still not allowed. For the name that we used in our substitution instance for `$\exists x\, \enot \atom{L}{x}$', namely `$b$', occurs in an undischarged assumption, namely line~$1$.

Finally, consider this `proof':
\begin{fitchproof}
	\hypo{nf}{\exists x\, \atom{L}{a, x}}\PR
	\open
		\hypo{na}{\atom{L}{a, a}}\AS
		\have{con1}{\exists x\,\atom{L}{x,x}}\Ei{na}		
	\close
\ifHTMLtarget
	\have{econ1}{\exists x\,\atom{L}{x,x}}\by{naughty attempt to invoke $\exists$E }{nf, na-con1}
\else
	\have{econ1}{\exists x\,\atom{L}{x,x}}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\exists$E }{nf, na-con1}
\fi
\end{fitchproof}
Here the name `$a$' violates the second condition of the $\exists$E
rule: it occurs in `$\exists x\, \atom{L}{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. \emph{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.

\section{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 \emph{vacuous quantification} (see the end of
\cref{s:FreeVars}). In \cref{s:forallElim,s:existsElim} we made use of
the substitution notation of \cref{s:TruthFOL}: $\metav{A}(\ldots
\metav{c} \ldots \metav{c} \ldots)$ is the formula obtained by
replacing every \emph{free} occurrence of $\metav{x}$ in $\metav{A}$
with~$\metav{c}$. Here, we emphasize the `free' for a reason. It means
you cannot always replace \emph{every} occurrence of~$\metav{x}$. For
instance, this would be incorrect:
\begin{fitchproof}
	\hypo{a}{\forall x(\atom{F}{x} \land \exists x\,\atom{G}{x})}\PR
	\ifHTMLtarget
	\have{e}{\atom{F}{a} \land \exists x\,\atom{G}{a}}\by{naughty attempt to invoke $\forall$E}{a}
\else
	\have{e}{\atom{F}{a} \land \exists x\,\atom{G}{a}}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\forall$E}{a}
\fi
\end{fitchproof}
On line $2$, we have formed the substitution instance incorrectly: we
replaced the `$x$' in both `$\atom{F}{x}$' and in `$\atom{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 x\,\atom{G}{a}$' is a case of vacuous quantification,
it is equivalent to just `$\atom{G}{a}$'. Furthermore, line~$1$ is
equivalent to `$\forall x(\atom{F}{x} \land \exists y\,\atom{G}{y})$'.
It should be easy to see that this does not entail `$\atom{F}{a} \land
\atom{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(\atom{F}{x} \land \exists
y\,\atom{G}{y})$', with variables nicely kept separate.


In \cref{s:existsIntro}, we said that we use `$\metav{A}(\ldots
\metav{x} \ldots \metav{c}\ldots)$' to indicate any formula obtained
by replacing \emph{some or all} of the instances of the name \metav{c}
with the variable~\metav{x} \emph{provided~$\metav{c}$,
wherever it is replaced, does not occur in the scope of a quantifier
binding~$\metav{x}$}. The emphasized restriction prohibiting the
replacement of $\metav{c}$ 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 x\,\atom{L}{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 x\,\atom{L}{x,x}$'. Now, `$\forall
x\,\atom{L}{x,x}$' \emph{could} be obtained from `$\forall
x\,\atom{L}{a,x}$' by replacing the name~`$a$' by the variable~`$x$'
if we weren't careful and overlooked that here `$a$' \emph{does} occur
in the scope of~`$\forall x$'. Without the restriction, the following
would then be allowed:
\begin{fitchproof}
		\hypo{a}{\forall x\, \atom{L}{a,x}}\PR
		\ifHTMLtarget
		\have{e}{\exists x\, \forall x\, \atom{L}{x,x}}\by{naughty attempt to invoke $\exists$I}{a}
	\else
		\have{e}{\exists x\, \forall x\, \atom{L}{x,x}}\by{naughty attempt}{}
		\have[\ ]{x}{}\by{to invoke $\exists$I}{a}
	\fi\end{fitchproof}
But since `$\exists x\, \forall x\, \atom{L}{x,x}$' is equivalent to
just `$\forall x\, \atom{L}{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 \cref{s:forallIntro}, we said that $\metav{A}(\ldots
\metav{x} \ldots \metav{x}\ldots)$ is the result of replacing
\emph{every} occurrence of~$\metav{c}$ in $\metav{A}(\ldots \metav{c}
\ldots \metav{c}\ldots)$ by~$\metav{x}$, but that \emph{this is only
allowed as long as $\metav{c}$ does not occur in the scope of a
quantifier binding~$\metav{x}$ in~$\metav{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 x\,\atom{L}{x,x}$' is a legal sentence of FOL. However,
`$\forall x\exists x\,\atom{L}{x,x}$' can be obtained from `$\forall
x\,\atom{L}{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:
\begin{fitchproof}
	\hypo{p}{\forall y\exists x\,\atom{L}{y,x}}\PR
	\have{a}{\exists x\, \atom{L}{a,x}}\Ae{p}
\ifHTMLtarget
	\have{e}{\forall x\, \exists x\, \atom{L}{x,x}}\by{naughty attempt to invoke $\forall$I}{a}
\else
\have{e}{\forall x\, \exists x\, \atom{L}{x,x}}\by{naughty attempt}{}
	\have[\ ]{x}{}\by{to invoke $\forall$I}{a}
\fi
\end{fitchproof}
But since `$\forall x\, \exists x\, \atom{L}{x,x}$' is equivalent to
just `$\exists x\, \atom{L}{x,x}$', this would be an invalid
inference: `Someone likes themselves' does not follow from `Everyone
likes someone'.

\practiceproblems
\problempart
Explain why these two `proofs' are \emph{incorrect}. Also, provide interpretations which would invalidate the fallacious argument forms the `proofs' enshrine:
\begin{multicols}{2}
	\begin{fitchproof}
		\hypo{Rxx}{\forall x\, \atom{R}{x,x}}\PR
		\have{Raa}{\atom{R}{a,a}}\Ae{Rxx}
		\have{Ray}{\forall y\, \atom{R}{a,y}}\Ai{Raa}
		\have{Rxy}{\forall x\, \forall y\, \atom{R}{x,y}}\Ai{Ray}
	\end{fitchproof}
	\begin{fitchproof}
		\hypo{AE}{\forall x\, \exists y\, \atom{R}{x,y}}\PR
		\have{E}{\exists y\, \atom{R}{a,y}}\Ae{AE}
		\open
			\hypo{ass}{\atom{R}{a,a}}\AS
			\have{Ex}{\exists x\, \atom{R}{x,x}}\Ei{ass}
		\close
		\have{con}{\exists x\, \atom{R}{x,x}}\Ee{E, ass-Ex}
	\end{fitchproof}
\end{multicols}

\problempart 
\label{pr.justifyFOLproof}
The following three proofs are missing their citations (rule and line numbers). Add them, to turn them into bona fide proofs.
\begin{compactlist}
\item \begin{fitchproof}
\hypo{p1}{\forall x\exists y(\atom{R}{x,y} \eor \atom{R}{y,x})}
\hypo{p2}{\forall x\,\enot \atom{R}{m,x}}
\have{3}{\exists y(\atom{R}{m,y} \eor \atom{R}{y,m})}{}
	\open
		\hypo{a1}{\atom{R}{m,a} \eor \atom{R}{a,m}}
		\have{a2}{\enot \atom{R}{m,a}}{}
		\have{a3}{\atom{R}{a,m}}{}
		\have{a4}{\exists x\, \atom{R}{x,m}}{}
	\close
\have{n}{\exists x\, \atom{R}{x,m}} {}
\end{fitchproof}

\item \begin{fitchproof}
\hypo{1}{\forall x(\exists y\,\atom{L}{x,y} \eif \forall z\,\atom{L}{z,x})}
\hypo{2}{\atom{L}{a,b}}
\have{3}{\exists y\,\atom{L}{a,y} \eif \forall z\atom{L}{z,a}}{}
\have{4}{\exists y\, \atom{L}{a,y}} {}
\have{5}{\forall z\, \atom{L}{z,a}} {}
\have{6}{\atom{L}{c,a}}{}
\have{7}{\exists y\,\atom{L}{c,y} \eif \forall z\,\atom{L}{z,c}}{}
\have{8}{\exists y\, \atom{L}{c,y}}{}
\have{9}{\forall z\, \atom{L}{z,c}}{}
\have{10}{\atom{L}{c,c}}{}
\have{11}{\forall x\, \atom{L}{x,x}}{}
\end{fitchproof}

\item \begin{fitchproof}
\hypo{a}{\forall x(\atom{J}{x} \eif \atom{K}{x})}
\hypo{b}{\exists x\,\forall y\, \atom{L}{x,y}}
\hypo{c}{\forall x\, \atom{J}{x}}
\open
	\hypo{2}{\forall y\, \atom{L}{a,y}}
	\have{3}{\atom{L}{a,a}}{}
	\have{d}{\atom{J}{a}}{}
	\have{e}{\atom{J}{a} \eif \atom{K}{a}}{}
	\have{f}{\atom{K}{a}}{}
	\have{4}{\atom{K}{a} \eand \atom{L}{a,a}}{}
	\have{5}{\exists x(\atom{K}{x} \eand \atom{L}{x,x})}{}
\close
\have{j}{\exists x(\atom{K}{x} \eand \atom{L}{x,x})}{}
\end{fitchproof}
\end{compactlist}

\problempart
\label{pr.BarbaraEtc.proof1}
In \hyperref[pr.BarbaraEtc]{exercise \ref*{s:MoreMonadic}A}, we
considered fifteen syllogistic figures of Aristotelian logic. Provide
proofs for each of the argument forms. NB: You will find it
\emph{much} easier if you symbolize (for example) `No F is G' as
`$\forall x (\atom{F}{x} \eif \enot \atom{G}{x})$'.

\

\problempart
\label{pr.BarbaraEtc.proof2}
Aristotle and his successors identified other syllogistic forms which depended upon `existential import'. Symbolize each of these argument forms in FOL and offer proofs.
\begin{compactlist}
	\item \textbf{Barbari.} Something is H. All G are F. All H are G. So: Some H is F.
	\item \textbf{Celaront.} Something is H. No G are F. All H are G. So: Some H is not F.
	\item \textbf{Cesaro.} Something is H. No F are G. All H are G. So: Some H is not F.
	\item \textbf{Camestros.} Something is H. All F are G. No H are G. So: Some H is not F.
	\item \textbf{Felapton.} Something is G. No G are F. All G are H. So: Some H is not F.
	\item \textbf{Darapti.} Something is G. All G are F. All G are H. So: Some H is F.
	\item \textbf{Calemos.} Something is H. All F are G. No G are H. So: Some H is not F.
	\item \textbf{Fesapo.} Something is G. No F is G. All G are H. So: Some H is not F.
	\item \textbf{Bamalip.} Something is F. All F are G. All G are H. So: Some H are F.
\end{compactlist}

\problempart
\label{pr.someFOLproofs}
For each of the following claims, provide an FOL proof that shows it
is true.
\begin{compactlist}
\item $\proves \forall x\,\atom{F}{x} \eif \forall y(\atom{F}{y} \eand \atom{F}{y})$
\item $\forall x(\atom{A}{x}\eif \atom{B}{x}), \exists x\,\atom{A}{x} \proves \exists x\,\atom{B}{x}$
\item $\forall x(\atom{M}{x} \eiff \atom{N}{x}), \atom{M}{a} \eand \exists x\,\atom{R}{x,a} \proves \exists x\,\atom{N}{x}$
\item $\forall x\, \forall y\,\atom{G}{x,y}\proves\exists x\,\atom{G}{x,x}$
\item $\proves\forall x\,\atom{R}{x,x} \eif \exists x\, \exists y\,\atom{R}{x,y}$
\item $\proves\forall y\, \exists x (\atom{Q}{y} \eif \atom{Q}{x})$
\item $\atom{N}{a} \eif \forall x(\atom{M}{x} \eiff \atom{M}{a}), \atom{M}{a}, \enot\atom{M}{b}\proves \enot \atom{N}{a}$
\item $\forall x\, \forall y (\atom{G}{x,y} \eif \atom{G}{y,x}) \proves \forall x\forall y (\atom{G}{x,y} \eiff \atom{G}{y,x})$
\item $\forall x(\enot\atom{M}{x} \eor \atom{L}{j,x}), \forall x(\atom{B}{x}\eif \atom{L}{j,x}), \forall x(\atom{M}{x}\eor \atom{B}{x})\proves \forall x\,\atom{L}{j,x}$
\end{compactlist}

\solutions
\problempart
\label{pr.likes}
Write a symbolization key for the following argument, symbolize it, and prove it:
\begin{earg}
\item There is someone who likes everyone who likes everyone that she
likes. 
\item[\texttherefore] There is someone who likes herself.
\end{earg}


\problempart
Show that each pair of sentences is provably equivalent.
\begin{compactlist}
\item $\forall x (\atom{A}{x}\eif \enot \atom{B}{x})$, $\enot\exists x(\atom{A}{x} \eand \atom{B}{x})$
\item $\forall x (\enot\atom{A}{x}\eif \atom{B}{d})$, $\forall x\,\atom{A}{x} \eor \atom{B}{d}$
\item $\exists x\,\atom{P}{x} \eif \atom{Q}{c}$, $\forall x (\atom{P}{x} \eif \atom{Q}{c})$
\end{compactlist}

\solutions
\problempart
\label{pr.FOLequivornot}
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.
\begin{compactlist}
\item $\forall x\,\atom{P}{x} \eif \atom{Q}{c}, \forall x (\atom{P}{x} \eif \atom{Q}{c})$
\item $\forall x\,\forall y\, \forall z\,\atom{B}{x,y,z}, \forall x\,\atom{B}{x,x,x}$
\item $\forall x\,\forall y\,\atom{D}{x,y}, \forall y\,\forall x\,\atom{D}{x,y}$
\item $\exists x\,\forall y\,\atom{D}{x,y}, \forall y\,\exists x\,\atom{D}{x,y}$
\item $\forall x (\atom{R}{c,a} \eiff \atom{R}{x,a}), \atom{R}{c,a} \eiff \forall x\,\atom{R}{x,a}$
\end{compactlist}

\solutions
\problempart
\label{pr.FOLvalidornot}
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.
\begin{compactlist}
\item $\exists y\,\forall x\,\atom{R}{x,y} \therefore \forall x\,\exists y\,\atom{R}{x,y}$
\item $\forall x\,\exists y\,\atom{R}{x,y} \therefore  \exists y\,\forall x\,\atom{R}{x,y}$
\item $\exists x(\atom{P}{x} \eand \enot \atom{Q}{x}) \therefore \forall x(\atom{P}{x} \eif \enot \atom{Q}{x})$
\item $\forall x(\atom{S}{x} \eif \atom{T}{a}), \atom{S}{d} \therefore \atom{T}{a}$
\item $\forall x(\atom{A}{x}\eif \atom{B}{x}), \forall x(\atom{B}{x} \eif \atom{C}{x}) \therefore \forall x(\atom{A}{x} \eif \atom{C}{x})$
\item $\exists x(\atom{D}{x} \eor \atom{E}{x}), \forall x(\atom{D}{x} \eif \atom{F}{x}) \therefore \exists x(\atom{D}{x} \eand \atom{F}{x})$
\item $\forall x\,\forall y(\atom{R}{x,y} \eor \atom{R}{y,x}) \therefore \atom{R}{j,j}$
\item $\exists x\,\exists y(\atom{R}{x,y} \eor \atom{R}{y,x}) \therefore \atom{R}{j,j}$
\item $\forall x\,\atom{P}{x} \eif \forall x\,\atom{Q}{x}, \exists x\, \enot\atom{P}{x} \therefore \exists x\, \enot \atom{Q}{x}$
\item $\exists x\,\atom{M}{x} \eif \exists x\,\atom{N}{x}$, $\enot \exists x\,\atom{N}{x}\therefore  \forall x\, \enot \atom{M}{x}$
\end{compactlist}

\chapter{Proofs with quantifiers}

In \cref{s:stratTFL} we discussed strategies for constructing proofs
using the basic rules of natural deduction for TFL. The same
principles apply to the rules for the quantifiers. If we want to prove
a quantifier sentence $\forall \metav{x}\,
\atom{\metav{A}}{\metav{x}}$ or $\exists \metav{x}\,
\atom{\metav{A}}{\metav{x}}$, we can work backward by justifying the
sentence we want by $\forall$I or $\exists$I and trying to find a
proof of the corresponding premise of that rule. And to work forward
from a quantified sentence, we apply $\forall$E or $\exists$E, as the
case may be.

Specifically, suppose you want to prove $\forall \metav{x}\, \atom{\metav{A}}{\metav{x}}$. To do so using $\forall$I, we would need a proof of $\atom{\metav{A}}{\metav{c}}$ for some name~$\metav{c}$ which does not occur in any undischarged assumption. To apply the corresponding strategy, i.e., to construct a proof of $\forall \metav{x}\, \atom{\metav{A}}{\metav{x}}$ by working backward, is thus to write $\atom{\metav{A}}{\metav{c}}$ above it and then to continue to try to find a proof of that sentence.
\begin{fitchproof}
	\ellipsesline
	\have[n]{n}{\atom{\metav{A}}{\metav{c}}}
	\have{m}{\forall \metav{x}\, \atom{\metav{A}}{\metav{x}}}\Ai{n}
\end{fitchproof}
$\atom{\metav{A}}{\metav{c}}$ is obtained from $\atom{\metav{A}}{\metav{x}}$ by replacing every free occurrence of $\metav{x}$ in $\atom{\metav{A}}{\metav{x}}$ by~$\metav{c}$. For this to work, $\metav{c}$ must satisfy the special condition. We can ensure that it does by always picking a name that does not already occur in the proof constructed so far. (Of course, it will occur in the proof we end up constructing---just not in an assumption that is undischarged at line~$n+1$.)

To work backward from a sentence $\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}$ we similarly write a sentence above it that can serve as a justification for an application of the $\exists$I rule, i.e., a sentence of the form $\atom{\metav{A}}{\metav{c}}$.
\begin{fitchproof}
	\ellipsesline
	\have[n]{n}{\atom{\metav{A}}{\metav{c}}}
	\have{m}{\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}}\Ei{n}
\end{fitchproof}
This looks just like what we would do if we were working backward from a universally quantified sentence. The difference is that whereas for $\forall$I we have to pick a name~$\metav{c}$ which does not occur in the proof (so far), for $\exists$I we may and in general must pick a name~$\metav{c}$ which already occurs in the proof.  Just like in the case of $\eor$I, it is often not clear which $\metav{c}$ will work out, and so to avoid having to backtrack you should work backward from existentially quantified sentences only when all other strategies have been applied.

By contrast, working \emph{forward} from sentences $\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}$ generally always works and you won't have to backtrack. Working forward from an existentially quantified sentence takes into account not just $\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}$ but also whatever sentence $\metav{B}$ you would like to prove. It requires that you set up a subproof above $\metav{B}$, wherein $\metav{B}$ is the last line, and a substitution instance $\atom{\metav{A}}{\metav{c}}$ of $\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}$ as the assumption.  In order to ensure that the condition on $\metav{c}$ that governs $\exists$E is satisfied, chose a name $\metav{c}$ which does not already occur in the proof.
\begin{fitchproof}
	\ellipsesline
	\have[m]{m}{\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}}
	\ellipsesline
	\open
	\hypo[n]{n}{\atom{\metav{A}}{\metav{c}}}\AS
	\ellipsesline
	\have[k]{k}{\metav{B}}
	\close
	\have{e}{\metav{B}}\Ee{m,n-k}
\end{fitchproof}
You'll then continue with the goal of proving $\metav{B}$, but now inside a subproof in which you have an additional sentence to work with, namely~$\atom{\metav{A}}{\metav{c}}$.

Lastly, working forward from $\forall \metav{x}\, \atom{\metav{A}}{\metav{x}}$ means that you can always write down $\atom{\metav{A}}{\metav{c}}$ and justify it using $\forall$E, for any name~$\metav{c}$. Of course, you wouldn't want to do that willy-nilly. Only certain names $\metav{c}$ will help in your task of proving whatever goal sentence you are working on. So, like working backward from $\exists \metav{x}\, \atom{\metav{A}}{\metav{x}}$, you should work forward from $\forall \metav{x}\, \atom{\metav{A}}{\metav{x}}$ only after all other strategies have been applied.

Let's consider as an example the argument $\forall x(\atom{A}{x} \eif B) \therefore \exists x\,\atom{A}{x} \eif B$. To start constructing a proof, we write the premise at the top and the conclusion at the bottom.
\begin{fitchproof}
\hypo{1}{\forall x(\atom{A}{x} \eif B)}\PR
\ellipsesline
\have[n]{7}{\exists x\,\atom{A}{x} \eif B}
\end{fitchproof}
The strategies for connectives of TFL still apply, and you should apply them in the same order: first work backward from conditionals, negated sentences, conjunctions, and now also universal quantifiers, then forward from disjunctions and now existential quantifiers, and only then try to apply $\eif$E, $\enot$E, $\lor$I, $\forall$E, or $\exists$I. In our case, that means, working backward from the conclusion:
\begin{fitchproof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}\PR
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}\AS
	\ellipsesline
	\have[n][-1]{6}{B}
	\close
	\have[n]{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-(6)}
\end{fitchproof}
Our next step should be to work forward from $\exists x\,\atom{A}{x}$ on line~$2$. For that, we have to pick a name not already in our proof. Since no names appear, we can pick any name, say~`$d$'
\begin{fitchproof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}\PR
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}\AS
	\open
	\hypo{3}{\atom{A}{d}}\AS
	\ellipsesline
	\have[n][-2]{5}{B}
	\close
	\have[n][-1]{6}{B}\Ee{2,3-(5)}
	\close
	\have[n]{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-(6)}
\end{fitchproof}
Now we've exhausted our primary strategies, and it is time to work forward from the premise $\forall x(\atom{A}{x} \eif B)$. Applying $\forall$E means we can justify any instance of $A(\metav{c}) \eif B$, regardless of what $\metav{c}$ we choose. Of course, we'll do well to choose $d$, since that will give us $\atom{A}{d} \eif B$. Then we can apply $\eif$E to justify~$B$, finishing the proof.
\begin{fitchproof}
	\hypo{1}{\forall x(\atom{A}{x} \eif B)}\PR
	\open
	\hypo{2}{\exists x\,\atom{A}{x}}\AS
	\open
	\hypo{3}{\atom{A}{d}}\AS
\have{4}{\atom{A}{d} \eif B}\Ae{1}
	\have{5}{B}\ce{4,3}
	\close
	\have{6}{B}\Ee{2,3-5}
	\close
	\have{7}{\exists x\,\atom{A}{x} \eif B}\ci{2-6}
\end{fitchproof}

Now let's construct a proof of the converse. We begin with
\begin{fitchproof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}\PR
	\ellipsesline
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}
\end{fitchproof}
Note that the premise is a conditional, not an existentially quantified sentence, so we should not (yet) work forward from it. Working backward from the conclusion, $\forall x(\atom{A}{x} \eif B)$, leads us to look for a proof of $\atom{A}{d} \eif B$:
\begin{fitchproof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}\PR
	\ellipsesline
	\have[n][-1]{6}{\atom{A}{d} \eif B}
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{fitchproof}
And working backward from $\atom{A}{d} \eif B$ means we should set up a subproof with $\atom{A}{d}$ as an assumption and $B$ as the last line:
\begin{fitchproof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}\PR
	\open
	\hypo{2}{\atom{A}{d}}\AS
	\ellipsesline
	\have[n][-2]{5}{B}
	\close
	\have[n][-1]{6}{\atom{A}{d} \eif B}\ci{2-(5)}
	\have[n]{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{fitchproof}
Now we can work forward from the premise on line~$1$. That's a conditional, and its consequent happens to be the sentence~$B$ we are trying to justify. So we should look for a proof of its antecedent, $\exists x\,\atom{A}{x}$. Of course, that is now readily available, by $\exists$I from line~$2$, and we're done:
\begin{fitchproof}
	\hypo{1}{\exists x\,\atom{A}{x} \eif B}\PR
	\open
	\hypo{2}{\atom{A}{d}}\AS
	\have{3}{\exists x\,\atom{A}{x}}\Ei{2}
	\have{5}{B}\ce{1,3}
	\close
	\have{6}{\atom{A}{d} \eif B}\ci{2-5}
	\have{7}{\forall x(\atom{A}{x} \eif B)}\Ai{6}
\end{fitchproof}

\practiceproblems

\problempart
Use the strategies to find proofs for each of the following arguments and theorems:
\begin{compactlist}
\item $A \eif \forall x\,\atom{B}{x} \therefore \forall x(A \eif \atom{B}{x})$
\item $\exists x(A \eif \atom{B}{x}) \therefore A \eif \exists x\, \atom{B}{x}$
\item $\forall x(\atom{A}{x} \eand \atom{B}{x}) \eiff (\forall x\,\atom{A}{x} \eand \forall x\,\atom{B}{x})$
\item $\exists x(\atom{A}{x} \eor \atom{B}{x}) \eiff (\exists x\,\atom{A}{x} \eor \exists x\,\atom{B}{x})$
\item $A \eor \forall x\,\atom{B}{x}) \therefore \forall x(A \eor \atom{B}{x})$
\item $\forall x(\atom{A}{x} \eif B) \therefore \exists x\,\atom{A}{x} \eif B$
\item $\exists x(\atom{A}{x} \eif B) \therefore \forall x\,\atom{A}{x} \eif B$
\item $\forall x(\atom{A}{x} \eif \exists y\,\atom{A}{y})$
\end{compactlist}
Use only the basic rules of TFL in addition to the basic quantifier rules.

\problempart
Use the strategies to find proofs for each of the following arguments and theorems:
\begin{compactlist}
\item $\forall x\,\atom{R}{x,x} \therefore \forall x\,\exists y\,\atom{R}{x,y}$
\item $\forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{y,z}) \eif \atom{R}{x,z}]$ \\
$\therefore \forall x\,\forall y[\atom{R}{x,y} \eif \forall z(\atom{R}{y,z} \eif \atom{R}{x,z})]$
\item $\forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{y,z}) \eif \atom{R}{x,z}],$\\ $\forall x\,\forall y(\atom{R}{x,y} \eif \atom{R}{y, x})$ \\ $\therefore \forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{x,z}) \eif \atom{R}{y,z}]$
\item $\forall x\,\forall y(\atom{R}{x,y} \eif \atom{R}{y, x})$ \\$\therefore \forall x\,\forall y\,\forall z[(\atom{R}{x,y} \eand \atom{R}{x,z}) \eif \exists u(\atom{R}{y,u} \eand \atom{R}{z,u})]$
\item $\enot \exists x\,\forall y (\atom{A}{x, y} \eiff \lnot\atom{A}{y, y})$
\end{compactlist}

\problempart
Use the strategies to find proofs for each of the following arguments and theorems:
\begin{compactlist}
\item $\forall x\,\atom{A}{x} \eif B \therefore \exists x(\atom{A}{x} \eif B)$
\item $A \eif \exists x\, \atom{B}{x} \therefore \exists x(A \eif \atom{B}{x})$
\item $\forall x(A \eor \atom{B}{x}) \therefore A \eor \forall x\,\atom{B}{x})$
\item $\exists x(\atom{A}{x} \eif \forall y\,\atom{A}{y})$
\item $\exists x(\exists y\,\atom{A}{y} \eif \atom{A}{x})$
\end{compactlist}
These require the use of IP. Use only the basic rules of TFL in addition to the basic quantifier rules.

\chapter{Conversion of quantifiers}\label{s:CQ}

In this section, we will add some additional rules to the basic rules of the previous section. These govern the interaction of quantifiers and negation.
 
In \cref{s:FOLBuildingBlocks}, we noted that $\enot\exists x\metav{A}$ is logically equivalent to $\forall x\, \enot\metav{A}$. We will add some rules to our proof system that govern this. In particular, we add:
	\factoidbox{
	\begin{fitchproof}
		\have[m]{a}{\forall \metav{x}\, \enot\metav{A}}
		\have[\ ]{con}{\enot \exists \metav{x}\, \metav{A}}\cq{a}
	\end{fitchproof}}
and
\factoidbox{
	\begin{fitchproof}
		\have[m]{a}{ \enot \exists \metav{x}\, \metav{A}}
		\have[\ ]{con}{\forall \metav{x}\, \enot \metav{A}}\cq{a}
	\end{fitchproof}}
Equally, we add:
\factoidbox{
	\begin{fitchproof}
		\have[m]{a}{\exists \metav{x}\, \enot \metav{A}}
		\have[\ ]{con}{\enot \forall \metav{x}\, \metav{A}}\cq{a}
	\end{fitchproof}}
and
\factoidbox{
	\begin{fitchproof}
		\have[m]{a}{\enot \forall \metav{x}\, \metav{A}}
		\have[\ ]{con}{\exists \metav{x}\, \enot \metav{A}}\cq{a}
	\end{fitchproof}}

\practiceproblems
\problempart
Show in each case that the sentences are inconsistent:
\begin{compactlist}
\item $\atom{S}{a}\eif \atom{T}{m}, \atom{T}{m} \eif \atom{S}{a}, \atom{T}{m} \eand \enot \atom{S}{a}$
\item $\enot\exists x\,\atom{R}{x,a}, \forall x\, \forall y\,\atom{R}{y,x}$
\item $\enot\exists x\, \exists y\,\atom{L}{x,y}, \atom{L}{a,a}$
\item $\forall x(\atom{P}{x} \eif \atom{Q}{x}), \forall z(\atom{P}{z} \eif \atom{R}{z}), \forall y\,\atom{P}{y}, \enot \atom{Q}{a} \eand \enot \atom{R}{b}$
\end{compactlist}

\problempart
Show that each pair of sentences is provably equivalent:
\begin{compactlist}
\item $\forall x (\atom{A}{x}\eif \enot \atom{B}{x}), \enot\exists x(\atom{A}{x} \eand \atom{B}{x})$
\item $\forall x (\enot\atom{A}{x}\eif \atom{B}{d}), \forall x\,\atom{A}{x} \eor \atom{B}{d}$
\end{compactlist}

\problempart
In \cref{s:MoreMonadic}, we considered what happens when we move quantifiers `across' various logical operators. Show that each pair of sentences is provably equivalent:
\begin{compactlist}
\item $\forall x(\atom{F}{x} \eand \atom{G}{a}), \forall x\,\atom{F}{x} \eand \atom{G}{a}$
\item $\exists x(\atom{F}{x} \eor \atom{G}{a}), \exists x\,\atom{F}{x} \eor \atom{G}{a}$
\item $\forall x(\atom{G}{a} \eif \atom{F}{x}), \atom{G}{a} \eif \forall x\,\atom{F}{x}$
\item $\forall x(\atom{F}{x} \eif \atom{G}{a}), \exists x\,\atom{F}{x} \eif \atom{G}{a}$
\item $\exists x(\atom{G}{a} \eif \atom{F}{x}), \atom{G}{a} \eif \exists x\,\atom{F}{x}$
\item $\exists x(\atom{F}{x} \eif \atom{G}{a}), \forall x\,\atom{F}{x} \eif \atom{G}{a}$
\end{compactlist}
NB: the variable `$x$' does not occur in `$\atom{G}{a}$'. When all the quantifiers occur at the beginning of a sentence, that sentence is said to be in \emph{prenex normal form}. These equivalences are sometimes called \emph{prenexing rules}, since they give us a means for putting any sentence into prenex normal form.


\chapter{Rules for identity}
In \cref{s:Interpretations}, we mentioned the philosophically contentious thesis of the \emph{identity of indiscernibles}. This is the claim that objects which are indiscernible in every way are, in fact, identical to each other. It was also mentioned that we will not subscribe to this thesis. It follows that, no matter how much you learn about two objects, we cannot prove that they are identical. That is unless, of course, you learn that the two objects are, in fact, identical, but then the proof will hardly be very illuminating.

The general point, though, is that \emph{no sentences} which do not already contain the identity predicate could justify an inference to `$a=b$'. So our identity introduction rule cannot allow us to infer to an identity claim containing two \emph{different} names.

However, every object is identical to itself. No premises, then, are required in order to conclude that something is identical to itself. So this will be the identity introduction rule:
\factoidbox{
\begin{fitchproof}
	\have[\ \,\,\,]{x}{\metav{c}=\metav{c}} \by{=I}{}
\end{fitchproof}}
Notice that this rule does not require referring to any prior lines of the proof. For any name \metav{c}, you can write $\metav{c}=\metav{c}$ on any line, with only the {=}I rule as justification.

Our elimination rule is more fun. If you have established `$a=b$', then anything that is true of the object named by `$a$' must also be true of the object named by `$b$'. For any sentence with `$a$' in it, you can replace some or all of the occurrences of `$a$' with `$b$' and produce an equivalent sentence. For example, from `$\atom{R}{a,a}$' and `$a = b$', you are justified in inferring `$\atom{R}{a,b}$', `$\atom{R}{b,a}$' or `$\atom{R}{b,b}$'. More generally:
\factoidbox{\begin{fitchproof}
	\have[m]{e}{\metav{a}=\metav{b}}
	\have[n]{a}{\metav{A}(\ldots \metav{a} \ldots \metav{a}\ldots)}
	\have[\ ]{ea1}{\metav{A}(\ldots \metav{b} \ldots \metav{a}\ldots)} \by{=E}{e,a}
\end{fitchproof}}
The notation here is as for $\exists$I. So $\metav{A}(\ldots \metav{a} \ldots \metav{a}\ldots)$ is a formula containing the name $\metav{a}$, and $\metav{A}(\ldots \metav{b} \ldots \metav{a}\ldots)$ is a formula obtained by replacing one or more instances of the name $\metav{a}$ with the name $\metav{b}$. Lines $m$ and $n$ can occur in either order, and do not need to be adjacent, but we always cite the statement of identity first. Symmetrically, we allow:
\factoidbox{\begin{fitchproof}
	\have[m]{e}{\metav{a}=\metav{b}}
	\have[n]{a}{\metav{A}(\ldots \metav{b} \ldots \metav{b}\ldots)}
	\have[\ ]{ea2}{\metav{A}(\ldots \metav{a} \ldots \metav{b}\ldots)} \by{=E}{e,a}
\end{fitchproof}}
This rule is sometimes called \emph{Leibniz's Law}, after Gottfried Leibniz.

To see the rules in action, we will prove some quick results. First, we will prove that identity is \emph{symmetric}:
\begin{fitchproof}
	\open
		\hypo{ab}{a = b}\AS
		\have{aa}{a = a}\by{=I}{}
		\have{ba}{b = a}\by{=E}{ab, aa}
	\close
	\have{abba}{a = b \eif b =a}\ci{ab-ba}
	\have{ayya}{\forall y (a = y \eif y = a)}\Ai{abba}
	\have{xyyx}{\forall x\, \forall y (x = y \eif y = x)}\Ai{ayya}
\end{fitchproof}
We obtain line~$3$ by replacing one instance of `$a$' in line~$2$ with an instance of~`$b$'; this is justified given `$a= b$'.

Second, we will prove that identity is \emph{transitive}:
\begin{fitchproof}
	\open
		\hypo{abc}{a = b \eand b = c}\AS
		\have{ab}{a = b}\ae{abc}
		\have{bc}{b = c}\ae{abc}
		\have{ac}{a = c}\by{=E}{ab, bc}
	\close
	\have{con}{(a = b \eand b =c) \eif a = c}\ci{abc-ac}
	\have{conz}{\forall z((a = b \eand b = z) \eif a = z)}\Ai{con}
	\have{cony}{\forall y\,\forall z((a = y \eand y = z) \eif a = z)}\Ai{conz}
	\have{conx}{\forall x\,\forall y \forall z((x = y \eand y = z) \eif x = z)}\Ai{cony}
\end{fitchproof}
We obtain line~$4$ by replacing `$b$' in line~$3$ with `$a$'; this is justified given `$a= b$'.

\practiceproblems
\problempart
\label{pr.identity}
For each of the following claims, provide an FOL proof that shows it
is true.
\begin{compactlist}
\item $\atom{P}{a} \eor \atom{Q}{b}, \atom{Q}{b} \eif b=c, \enot\atom{P}{a} \proves \atom{Q}{c}$
\item $m=n \eor n=o, \atom{A}{n} \proves \atom{A}{m} \eor \atom{A}{o}$
\item $\forall x\ x=m, \atom{R}{m,a} \proves \exists x\,\atom{R}{x,x}$
\item $\forall x\,\forall y(\atom{R}{x,y} \eif x=y)\proves \atom{R}{a,b} \eif \atom{R}{b,a}$
\item $\enot \exists x\enot x = m \proves \forall x\,\forall y (\atom{P}{x} \eif \atom{P}{y})$
\item $\exists x\,\atom{J}{x}, \exists x\, \enot\atom{J}{x}\proves \exists x\, \exists y\, \enot x = y$
\item $\forall x(x=n \eiff \atom{M}{x}), \forall x(\atom{O}{x} \eor \enot \atom{M}{x})\proves \atom{O}{n}$
\item $\exists x\,\atom{D}{x}, \forall x(x=p \eiff \atom{D}{x})\proves \atom{D}{p}$
\item $\exists x\bigl[(\atom{K}{x} \eand \forall y(\atom{K}{y} \eif x=y)) \eand \atom{B}{x}\bigr], Kd\proves \atom{B}{d}$
\item $\proves \atom{P}{a} \eif \forall x(\atom{P}{x} \eor \enot x = a)$
\end{compactlist}

\problempart
Show that the following are provably equivalent:
\begin{itemize}
\item $\exists x \bigl([\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)] \eand x = n\bigr)$
\item $\atom{F}{n} \eand \forall y (\atom{F}{y} \eif n= y)$
\end{itemize}
And hence that both have a decent claim to symbolize the English sentence `Nick is the~$F$'.\\

\problempart
In \cref{sec.identity}, we claimed that the following are logically equivalent symbolizations of the English sentence `there is exactly one $F$':
\begin{itemize}
\item $\exists x\,\atom{F}{x} \eand \forall x\, \forall y \bigl[(\atom{F}{x} \eand \atom{F}{y}) \eif x = y\bigr]$
\item $\exists x \bigl[\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)\bigr]$
\item $\exists x\, \forall y (\atom{F}{y} \eiff x = y)$
\end{itemize}
Show that they are all provably equivalent. (\emph{Hint}: to show that three claims are provably equivalent, it suffices to show that the first proves the second, the second proves the third and the third proves the first; think about why.)


\
\problempart
Symbolize the following argument
	\begin{earg}
		\item There is exactly one $F$. 
		\item There is exactly one $G$. 
		\item Nothing is both $F$ and~$G$. 
		\item[\texttherefore] There are exactly two things that are either~$F$ or~$G$.
	\end{earg}
And offer a proof of it.
%\begin{itemize}
%\item  $\exists x \bigl[\atom{F}{x} \eand \forall y (\atom{F}{y} \eif x = y)\bigr], \exists x \bigl[\atom{G}{x} \eand \forall y (\atom{G}{y} \eif x = y)\bigr], \forall x (\enot\atom{F}{x} \eor \enot \atom{G}{x}) \proves \exists x\, \exists y \bigl[\enot x = y \eand \forall z ((\atom{F}{z} \eor \atom{G}{z}) \eif (x = y \eor x = z))\bigr]$
%\end{itemize}




\chapter{Derived rules}\label{s:DerivedFOL}
As in the case of TFL, we first introduced some rules for FOL as basic (in \cref{s:BasicFOL}), and then added some further rules for conversion of quantifiers (in \cref{s:CQ}). In fact, the CQ rules should be regarded as \emph{derived} rules, for they can be derived from the  \emph{basic} rules of \cref{s:BasicFOL}. (The point here is as in \cref{s:Derived}.) Here is a justification for the first CQ rule:
\begin{fitchproof}
	\have[m]{An}{\forall x\, \enot \atom{A}{x}}
	\open
		\hypo[m+1]{E}{\exists x\, \atom{A}{x}}\AS
		\open
			\hypo[m+2]{c}{\atom{A}{c}}\AS
			\have[m+3]{nc}{\enot \atom{A}{c}}\Ae{An}
			\have[m+4]{red}{\ered}\ne{nc,c}
		\close
		\have[m+5]{red2}{\ered}\Ee{E,(c)-(red)}
	\close
	\have[m+6]{dada}{\enot \exists x\, \atom{A}{x}}\ni{(E)-(red2)}
\end{fitchproof}
%You will note that on line 3 I have written `for $\exists$E'. This is not technically a part of the proof. It is just a reminder---to me and to you---of why I have bothered to introduce `$\enot \atom{A}{c}$' out of the blue. You might find it helpful to add similar annotations to assumptions when performing proofs. But do not add annotations on lines other than assumptions: the proof requires its own citation, and your annotations will clutter it.
Here is a justification of the third CQ rule:
\begin{fitchproof}
	\have[m]{nEna}{\exists x\, \enot \atom{A}{x}}
	\open
		\hypo[m+1]{Aa}{\forall x\, \atom{A}{x}}\AS
		\open
			\hypo[m+2]{nac}{\enot \atom{A}{c}}\AS
			\have[m+3]{a}{\atom{A}{c}}\Ae{Aa}
			\have[m+4]{con}{\ered}\ne{nac,a}
		\close
		\have[m+5]{con1}{\ered}\Ee{nEna, (nac)-(con)}
	\close
	\have[m+6]{dada}{\enot \forall x\, \atom{A}{x}}\ni{(Aa)-(con1)}
\end{fitchproof}
This explains why the CQ rules can be treated as derived. Similar justifications can be offered for the other two CQ rules.

\practiceproblems

\problempart
Offer proofs which justify the addition of the second and fourth CQ rules as derived rules.



\chapter{Proofs and semantics}
We have used two different turnstiles in this book.  This:
$$\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n \proves \metav{C}$$
means that there is some proof which ends with $\metav{C}$ and whose only undischarged assumptions are among $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$. This is a \emph{proof-theoretic notion}. By contrast, this: 
$$\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n \entails \metav{C}$$
means that no valuation (or interpretation) makes all of $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$ true and~$\metav{C}$ false. This concerns assignments of truth and falsity to sentences. It is a \emph{semantic notion}.

It cannot be emphasized enough that these are different notions. But we can emphasize it a bit more: \emph{They are different notions.}

Once you have internalised this point, continue reading.

Although our semantic and proof-theoretic notions are different, there is a deep connection between them. To explain this connection,we will start by considering the relationship between validities and theorems.

To show that a sentence is a theorem, you need only produce a proof. Granted, it may be hard to produce a twenty line proof, but it is not so hard to check each line of the proof and confirm that it is legitimate; and if each line of the proof individually is legitimate, then the whole proof is legitimate. Showing that a sentence is a validity, though, requires reasoning about all possible interpretations. Given a choice between showing that a sentence is a theorem and showing that it is a validity, it would be easier to show that it is a theorem.

Contrawise, to show that a sentence is \emph{not} a theorem is hard. We would need to reason about all (possible) proofs. That is very difficult. However, to show that a sentence is not a validity, you need only construct an interpretation in which the sentence is false. Granted, it may be hard to come up with the interpretation; but once you have done so, it is relatively straightforward to check what truth value it assigns to a sentence. Given a choice between showing that a sentence is not a theorem and showing that it is not a validity, it would be easier to show that it is not a validity.

Fortunately, \emph{a sentence is a theorem if and only if it is a validity}. As a result, if we provide a proof of $\metav{A}$ on no assumptions, and thus show that $\metav{A}$ is a theorem, i.e., ${}\proves \metav{A}$, we can legitimately infer that $\metav{A}$ is a validity, i.e., $\entails\metav{A}$. Similarly, if we construct an interpretation in which \metav{A} is false and thus show that it is not a validity, i.e., $\nentails \metav{A}$, it follows that \metav{A} is not a theorem, i.e.,  $\nproves \metav{A}$.

More generally, we have the following powerful result:
\factoidbox{$\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n
\proves\metav{B}$ \textbf{\ifeff} $\metav{A}_1, \metav{A}_2, \ldots,
\metav{A}_n \entails\metav{B}$}
This shows that, whilst provability and entailment are \emph{different} notions, they are extensionally equivalent. As such:
	\factoidbox{\begin{factoiditems}
		\item An argument is \emph{valid} \ifeff{} \emph{the conclusion can be proved from the premises}.
		\item A sentence is a \emph{validity} \ifeff{} it is a \emph{theorem}.
		\item Two sentences are \emph{equivalent} \ifeff{} they are
		\emph{provably equivalent}.
		\item Sentences are \emph{jointly satisfiable} \ifeff{} they are
		\emph{jointly consistent}.
	\end{factoiditems}}
For this reason, you can pick and choose when to think in terms of proofs and when to think in terms of valuations/interpretations, doing whichever is easier for a given task. The table on the next page summarizes which is (usually) easier.

It is intuitive that provability and semantic entailment should agree. But---let us repeat this---do not be fooled by the similarity of the symbols `$\entails$' and `$\proves$'. These two symbols have very different meanings. The fact that provability and semantic entailment agree is not an easy result to come by.

In fact, demonstrating that provability and semantic entailment agree is, very decisively, the point at which introductory logic becomes intermediate logic.

\ifHTMLtarget
\begin{table}
\else
\begin{sidewaystable}\small
\fi
	\begin{center}
\begin{tabular*}{\textwidth}{p{.25\textheight}p{.325\textheight}p{.325\textheight}}
 & \textbf{Yes}  & \textbf{No}\\
\\
Is \metav{A} a \textbf{validity}? 
& give a proof which shows $\proves\metav{A}$ 
& give an interpretation in which \metav{A} is false\\
\\
Is \metav{A} a \textbf{contradiction}? &
give a proof which shows $\proves\enot\metav{A}$ & 
give an interpretation in which \metav{A} is true\\
\\
%Is \metav{A} contingent? & 
%give two interpretations, one in which \metav{A} is true and another in which \metav{A} is false & give a proof which either shows $\proves\metav{A}$ or $\proves\enot\metav{A}$\\
%\\
Are \metav{A} and \metav{B} \textbf{equivalent}? &
give two proofs, one for $\metav{A}\proves\metav{B}$ and one for $\metav{B}\proves\metav{A}$  
& give an interpretation in which \metav{A} and \metav{B} have different truth values\\
\\
Are $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$ \textbf{jointly satisfiable}? 
& give an interpretation in which all of $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$ are true 
& prove a contradiction from assumptions $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$\\
\\
Is $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n \therefore \metav{C}$ \textbf{valid}? 
& give a proof with assumptions $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$ and concluding with \metav{C}
& give an interpretation in which each of $\metav{A}_1, \metav{A}_2, \ldots, \metav{A}_n$ is true and \metav{C} is false\\
\end{tabular*}
\end{center}
\ifHTMLtarget
\end{table}
\else
\end{sidewaystable}
\fi