%!TEX root = proofs+concepts.tex

\chapter{First-Order Logic}
\label{ch.firstorder}

\begin{quote}
\it Three Logicians walk into a bar, and
\\ the barkeeper asks ``Would you all like something to drink?''
\\ The 1st Logician says ``I don't know\rlap,''
\\ and the 2nd Logician says ``I don't know\rlap.''
\\ Then the 3rd Logician says ``yes\rlap.''
\\ \hbox{\hskip 2in}  \small\rm\sf
author unknown
\end{quote}


\section{Quantifiers}
\label{sec.quantifiers}

Earlier, we observed that {\SL} cannot fully express ideas involving quantity, such as ``some'' or ``all\rlap.''  In this chapter, we will fill this gap by introducing quantifier symbols. Together with predicates and sets, which have already been discussed, this completes the language of {\QL}. We will then use this language to translate assertions from English into mathematical notation.

In our first example we will use this symbolization key:
\begin{multicols}{2}
\begin{ekey}
\item[\univ] The set of all people.
\item[L] The set of all people in \hbox to 0pt{Lethbridge.\hss} % !!!
\item[A] The set of all angry people.
\item[H] The set of all happy people.
\item [x \mathrel{R} y] $x$ is richer than $y$
\item [d] Donald
\item [g] Gregor
\item [m] Marybeth
\end{ekey}
\end{multicols}
\noindent Now consider  these assertions:
\begin{assertlist}
\item[\ex{q.a}] Everyone is happy.
\item[\ex{q.Lhap}] Everyone in Lethbridge is happy.
\item[\ex{q.ac}] Everyone in Lethbridge is richer than Donald.
\item[\ex{q.e}] Someone in Lethbridge is angry.
\end{assertlist}

It might be tempting to translate \assert{q.a} as $(d \in H) \eand (g \in H) \eand (m \in H)$. Yet this would only say that Donald, Gregor, and Marybeth are happy. We want to say that \emph{everyone} is happy, even if we have not listed them in our symbolization key. In order to do this, we introduce the ``$\forall$'' symbol. This is called the \define[quantifier!universal]{universal quantifier}.
\factoidbox{$\forall x$ means ``for all $x$''%
\nindex{$\forall$}%
}\index{all ($\forall$)}

A quantifier must always be followed by a variable, and then a formula that the quantifier applies to. We can translate \assert{q.a} as $\forall x, (x \in H)$. Paraphrased in English, this means ``For all~$x$, $x$~is happy\rlap.'' %(or ``for all~$x$, $x$~is a happy person''). 
%\nix{This may be too soon:}
%We call $\forall x$ an \emph{x-quantifier}. The formula that follows the quantifier is called the \emph{scope} of the quantifier. We will give a formal definition of scope later, but intuitively it is the part of the assertion that the quantifier quantifies over. In $\forall x Hx$, the scope of the universal quantifier is $Hx$.

In quantified assertions such as this one, the variable $x$ is serving as a kind of placeholder. The expression $\forall x$ means that you can pick anyone and put them in as~$x$. There is no special reason to use $x$ rather than some other variable. The assertion ``$\forall x, (x \in H)$'' means exactly the same thing as ``$\forall y , (y \in H)$\rlap,'' ``$\forall z, (z \in H)$\rlap,'' or ``$\forall x_5, (x_5 \in H)$\rlap.''

To translate \assert{q.Lhap}, we use a different version of the universal quantifier:
\factoidbox{If $X$ is any set, then $\forall x \in X$ means ``for all $x$ in~$X$''}
Now we can translate \assert{q.Lhap} as $\forall \ell \in L, (\ell \in H)$. (It would also be logically correct to write $\forall x \in L, (x \in H)$, but $\ell$ is a better name an element of the set~$L$.) Paraphrased in English, our symbolic assertion means ``For all $\ell$ in Lethbridge, $\ell$~is happy\rlap.''

\assert{q.ac} can be paraphrased as, ``For all $\ell$ in~Lethbridge, $\ell$~is richer than Donald\rlap.'' This translates as $\forall \ell \in L, (\ell \mathrel{R} d)$.

To translate \assert{q.e}, we introduce another new symbol: the \define[quantifier!existential]{existential quantifier}, $\exists$. 
\factoidbox{$\exists x$ means ``there exists some $x$, such that''%
\nindex{$\exists$}}\index{exists ($\exists$)}
\factoidbox{If $X$ is any set, then $\exists x \in X$ means 
\\``there exists some $x$ in~$X$, such that''}%
%Like the universal quantifier, the existential quantifier requires a variable. \assert{q.e} can be translated as $\exists x, A(x)$. 
We write $\exists \ell \in L, (\ell \in A)$.
This means that there exists some~$\ell$ in Lethbridge who is angry. More precisely, it means that there is \emph{at least one} angry person in Lethbridge. Once again, the variable is a kind of placeholder; it would have been logically correct (but poor form) to translate \assert{q.e} as $\exists z \in L, (z \in A)$.


\begin{eg}
Consider this symbolization key.
\begin{ekey}
\item[S]  The set of all students.
\item[B] The set of all books.
\item[N] The set of all novels.
\item[x \mathrel{L} y] $x$ likes to read~$y$.
\end{ekey}
Then:
\begin{enumerate}
\item $\forall n \in N, (n \in B)$ means ``every novel is a book\rlap,''
and
\item $\forall s \in S, \bigl( \exists b \in B, (s  \mathrel{L} b) \bigr)$ means ``for every student, there is some book that the student likes to read\rlap.''
\end{enumerate}
\end{eg}

Notice that all of the quantifiers in this example are of the form $\forall x \in X$ or $\exists x \in X$, not $\forall x$ or $\exists x$. That is, all of the variables range over specific sets, rather than being free to range over the entire universe of discourse. Because of this, it is acceptable to omit specifying a universe of discourse.  Of course, the universe of discourse (whatever it is) must include at least all students, all books, and all novels.

\begin{exer}  \label{SubsetDefnsEx}
Suppose $A$ and $B$ are sets.
\\{\it Give your answers in the notation of {First-Order Logic} {\rm(}not English\/{\rm)}.}
\begin{enumerate}
\item  \label{SubsetDefnsEx-Subset}
 What does it mean to say that $A$ is a subset of~$B$? 
\item  \label{SubsetDefnsEx-NotSubset}
 What does it mean to say that $A$ is \emph{not} a subset of~$B$? 
\end{enumerate}
\end{exer}



%\section{Universe of Discourse}
%Given the symbolization key we have been using, $\forall x,H(x)$ means ``Everyone is happy\rlap.'' Who is included in this \emph{everyone}? When we use assertions like this in English, we usually do not mean everyone now alive on the Earth. We certainly do not mean everyone who was ever alive or who will ever live. We mean something more modest: everyone in the building, everyone in the class, or everyone in the room.

%In order to eliminate this ambiguity, we will need to specify a \define{universe of discourse}---abbreviated \univ. The \univ{} is the set of things that we are talking about. So if we want to talk about people in Alberta, we define \univ{} to be people in the Alberta. We write this at the beginning of the symbolization key, like this:
%\begin{ekey}
%\item[\univ ] people in Alberta
%\end{ekey}
%The quantifiers \emph{range over} the universe of discourse. Given this \univ, $\forall x$ means ``Everyone in Alberta'' and $\exists x$ means ``Someone in Alberta\rlap.'' Each constant names some member of \univ, so we can only use this \univ{} with the symbolization key above if Donald, Gregor, and Marybeth are all in Alberta. If we want to talk about people in places besides Alberta, then we need to include those people in~\univ.

%In {\QL}, \univ{} must be \emph{non-empty}; that is, it must contain at least one member. It is possible to construct formal languages that allow for empty \univ s, but this introduces complications.

%Even allowing for a \univ{} with just one member can produce some strange results. Suppose we have this as a symbolization key:
%\begin{ekey}
%\item[\univ ] the Eiffel Tower
%\item[Px] $x$ is in Paris.
%\end{ekey}
%The assertion $\forall x Px$ might be paraphrased in English as ``Everything is in Paris\rlap.'' Yet that would be misleading. It means that everything \emph{in \univ } is in Paris. This \univ{} contains only the Eiffel Tower, so with this symbolization key $\forall x Px$ just means that the Eiffel Tower is in Paris.



%\subsection{Non-referring terms}
%In {\QL}, each constant must pick out exactly one member of \univ. A constant cannot refer to more than one thing---it is a \emph{singular} term. Each constant must still pick out \emph{something}. This is connected to a classic philosophical problem: the so-called problem of non-referring terms.

%Medieval philosophers typically used assertions about the \emph{chimera} to exemplify this problem. Chimera is a mythological creature; it does not really exist. Consider these two assertions:
%\begin{assertlist}
%\item[\ex{chimera1}] Chimera is angry.
%\item[\ex{chimera2}] Chimera is not angry.
%\end{assertlist}
%It is tempting just to define a constant to mean ``chimera\rlap.'' The symbolization key would look like this:
%\begin{ekey}
%\item[\univ ] creatures on Earth
%\item[Ax] $x$ is angry.
%\item[c] chimera
%\end{ekey}
%We could then translate \assert{chimera1} as $Ac$ and \assert{chimera2} as $\enot Ac$.

%Problems will arise when we ask whether these assertions are true or false.

%One option is to say that \assert{chimera1} is not true, because there is no chimera. If \assert{chimera1} is false because it talks about a non-existent thing, then \assert{chimera2} is false for the same reason. Yet this would mean that $Ac$ and $\enot Ac$ would both be false. Given the truth conditions for negation, this cannot be the case.

%Since we cannot say that they are both false, what should we do? Another option is to say that \assert{chimera1} is \emph{meaningless} because it talks about a non-existent thing. So $Ac$ would be a meaningful expression in {\QL} for some interpretations but not for others. Yet this would make our formal language hostage to particular interpretations. Since we are interested in logical form, we want to consider the logical force of an assertion like $Ac$ apart from any particular interpretation. If $Ac$ were sometimes meaningful and sometimes meaningless, we could not do that.

%This is the \emph{problem of non-referring terms}, and we will return to it later (see p.~\pageref{subsec.defdesc}.) The important point for now is that each constant of {\QL} \emph{must} refer to something in \univ, although \univ{} can be any set of things that we like. If we want to symbolize deductions about mythological creatures, then we must define a \univ{} that includes them. This option is important if we want to consider the logic of stories. We can translate an assertion like ``Sherlock Holmes lived at 221B Baker Street'' by including fictional characters like Sherlock Holmes in our \univ.



\section{Translating to {\QL}}
We now have all of the pieces of {\QL}. Translating assertions (no matter how complicated) from English to mathematical notation will only be a matter of knowing the right way to combine predicates, constants, quantifiers, connectives, and sets. Consider these assertions:
\begin{assertlist}
\item[\ex{quan1}] Every coin in my pocket is a dime.
\item[\ex{quan2}] Some coin on the table is a dime.
\item[\ex{quan3}] Not all the coins in my pocket are dimes.
\item[\ex{quan4}] None of the coins on the table are dimes.
\end{assertlist}
In providing a symbolization key, we need to specify~\univ. Since we are not talking about anything besides coins, we may let \univ{} be the set of all coins. (It is not necessary to include all coins in~\univ, but, since we are talking about the coins in my pocket and the coins on the table, \univ~must at least contain all of those coins.) Since we are not talking about any specific coins, we do not need to define any constants.
Since we will be explicitly talking about the coins in my pocket and the coins on the table, it will be helpful to have these defined as sets. The symbolization key also needs to say something about dimes; let's do this with a predicate. So we define this key:
\begin{ekey}
\item[\univ ] The set of all coins.
\item[P] The set of all coins in my pocket.
\item[T] The set of all coins on the table.
%\item[Q(x)] $x$ is a quarter.
\item[D(x)] $x$ is a dime.
\end{ekey}
\assert{quan1} is most naturally translated with a universal quantifier. It talks about all of the coins in my pocket (that is, the elements of the set~$P$). It means that, for any coin in my pocket, that coin is a dime. So we can translate it as $\forall p\in P, D(p)$.

\assert{quan2} says there is some coin on the table, such that the coin is a dime. So we translate it as $\exists t \in T, D(t)$.

\assert{quan3} can be paraphrased as, ``It is not the case that every coin in my pocket is a dime\rlap.'' So we can translate it as $\enot \bigl(\forall p\in P, D(p)\bigr)$. This is simply the negation of \assert{quan1}. 
%Thus, by the rules for negation in \cref{sect.predicate.negation}, the assertion could be rephrased as ``Some coin in my pocket is not a dime\rlap,'' which would translate as $\exists x, \bigl(P(x) \eand \enot D(x) \bigr)$. This is not the same as \assert{quan3}, but it is logically equivalent to it.
%Although it is probably not obvious, these two translations are logically equivalent. (This is due to the logical equivalence between $\enot\forall x, \script{A}$ and $\exists x,\enot\script{A}$, along with the equivalence between $\enot(\script{A}\eif\script{B})$ and $\script{A}\eand\enot\script{B}$.)

\assert{quan4} can be paraphrased as, ``It is not the case that some coin on the table is a dime\rlap.'' This can be translated as $\enot\bigl(\exists t\in T, D(t) \bigr)$. 
It is the negation of \assert{quan2}.
%Applying the rules for negation, we can express the same meaning as ``Every coin either is not on the table or is not a dime. This translates to $\forall x, \bigl(\enot T(x) \eor \enot D(x) \bigr)$.
%Again, the two translations are logically equivalent. 
%In English, there are also other ways to express the same meaning. For example, one could say ``Every coin on the table is a non-dime\rlap,'' which translates as $\forall x, \bigl(T(x) \eif \enot D(x) \bigr)$. This is logically equivalent to the other two translations.
%It might also be paraphrased as, ``Everything in my pocket is a non-dime\rlap,'' and then could be translated as $\forall x, \bigl(P(x) \eif \enot D(x) \bigr)$. Again the two translations are logically equivalent. Both are correct translations of \assert{quan4}.

\begin{rem} \label{DimeSetBetter}
Alternatively, we could have defined a set $D$, the set of all dimes, instead of the predicate $D(x)$.  In this case: 
	\begin{itemize}
	\item \assert{quan1} would be translated as $\forall p \in P, \ p \in D$.  
	\item \assert{quan2} would be translated as $\exists t \in T, \ t \in D$.
	\item \assert{quan3} would be translated as $\enot (\forall p \in P, \ p \in D)$.
	\item \assert{quan4} would be translated as $\enot (\exists t \in T, \ t \in D)$.
	\end{itemize}
Either approach is perfectly legitimate. 

However, if we need to quantify over dimes, then it is much better to use a set than a predicate.
For example, let's symbolize the assertion ``Every dime is in my pocket\rlap.''
	\begin{itemize}
	\item If $D$ is the set of all dimes, we can write: $\forall d \in D, \ d \in P$.
	\item It is less straightforward if we use the predicate $D(x)$, because we cannot directly say ``for all dimes'' 
	(since the set of all dimes is not available). The translation must consider all coins, and then say that
	the ones that are dimes are in my pocket: $\forall x, \bigl( D(x) \eif x \in P \bigr)$.
	\end{itemize}
For this reason (and others), mathematicians tend to use sets, rather than predicates, and we will do the same.
%We will use assertions like this later on.  However, in this chapter, while we are just learning {\QL}, we will generally use sets only immediately after quantifiers, and use predicates in what follows.
\end{rem}

\begin{rem}
If we had defined the predicate $P(x)$ (for ``$x$ is in my pocket'') instead of the corresponding set $P$, we would have needed to translate \assert{quan1} as $\forall x, \bigl( P(x) \implies D(x) \bigr)$: that is, ``for any coin, if it is in my pocket, then it is a dime\rlap.''
Since the assertion is about coins that are both in my pocket \emph{and} that are dimes, it might be tempting to translate it using~$\eand$. However, the assertion $\forall x, \bigl(P(x) \eand D(x) \bigr)$ would mean that everything in~\univ{} is both in my pocket and a dime: All the coins that exist are dimes in my pocket. This is would be a crazy thing to say, and it means something very different than \assert{quan1}.  However, this issue is completely avoided when we use sets. Thus, defining $P$ to be a set, rather than a predicate, is the best approach in this problem (and similarly for~$T$).
%Notice that we needed to use a conditional with the universal quantifier, but we used a conjunction with the existential quantifier. What would it mean to write $\exists x, \bigl(T(x) \eif D(x) \bigr)$? Probably not what you think. It means that there is some member of~\univ{} that would satisfy the subformula; roughly speaking, there is some $a$ such that $\bigl( T(a) \eif D(a) \bigr)$ is true. In {\SL}, $\script{A} \eif \script{B}$ is logically equivalent to $\enot\script{A} \eor \script{B}$, and this will also hold in {\QL}. So $\exists x, \bigl(T(x) \eif D(x) \bigr)$ is true if there is some $a$ such that $\bigl(\enot T(a) \eor D(a) \bigr)$; i.e., it is true if some coin is \emph{either} not on the table \emph{or} is a dime. Of course there is a coin that is not the table---there are coins lots of other places. So $\exists x, \bigl(T(x) \eif D(x) \bigr)$ is obviously true. A conditional will usually be the natural connective to use with a universal quantifier, but a conditional within the scope of an existential quantifier can do very strange things. As a general rule, do not put conditionals in the scope of existential quantifiers unless you are sure that you need one.
\end{rem}

\begin{eg} \label{MerlinFunnyHatSoln}
We can now translate the deduction from page~\pageref{willard1}, the one that motivated the need for quantifiers:
\begin{quote}
Merlin is a wizard. All wizards wear funny hats.\\
\therefore\ Merlin wears a funny hat.
\end{quote}
\begin{ekey}
\item[\univ ] The set of all people.
\item[W] The set of all wizards.
\item[H] The set of all people who wear a funny hat.
\item[m] Merlin
\end{ekey}
Translating, we get:
\begin{earg}
\item[] $m \in W$
\item[] $\forall w\in W, (w \in H) $
\conclusion $m \in H$
\end{earg}
\end{eg}

This captures the structure that was left out when we translated the deduction into {\SL}, and this is a valid deduction in {\QL}.
We will be able to prove it rigorously after we have discussed the introduction and elimination rules for~$\forall$ (and~$\exists$) in \cref{IntroElimQuantSect}.

%\nix{What does $\forall x, x \mathrel{O} i$ mean? [Wait.] ``Ryan and I owe me money\rlap.'' It might be true (although slightly odd), but it would be very different than the same formal assertion with \univ{} being all people.}

\begin{exers}
\label{pr.{\QL}alligators}
Using the given symbolization key, translate each English-language assertion into {\QL}.
\begin{multicols}{2}
\begin{ekey}
\item[\univ ] The set of all animals.
 \item[A] The set of all alligators.
 \item[R] The set of all reptiles.
 \item[Z] The set of all \hbox to 0pt{animals who live at the zoo.\hss} % !!!
 \item[M] The set of all monkeys.
\item[x \mathrel{\heartsuit} y] $x$ loves $y$.
\item[a] Amos
\item[b] Bouncer
\item[c] Cleo
\end{ekey}
\end{multicols}
\begin{problist}
\item \label{pr.{\QL}alligators-ABCzoo}
Amos, Bouncer, and Cleo all live at the zoo. 
\item \label{pr.{\QL}alligators-Brept}
 Bouncer is a reptile, but not an alligator. 
\item \label{pr.{\QL}alligators-CloveB}
 If Cleo loves Bouncer, then Bouncer is a monkey. 
\item \label{pr.{\QL}alligators-BCall}
 If both Bouncer and Cleo are alligators, then Amos loves them both.
\item \label{pr.{\QL}alligators-SomeReptZoo}
 Some reptile lives at the zoo. 
\item \label{pr.{\QL}alligators-EveryAllZoo}
 Every alligator is a reptile. 
\item \label{pr.{\QL}alligators-Zoo->MA}
 Every animal that lives at the zoo is either a monkey or an alligator. 
\item \label{pr.{\QL}alligators-ReptNotAll}
 There are reptiles which are not alligators.
\item \label{pr.{\QL}alligators-CloveRept}
 Cleo loves a reptile.
\item \label{pr.{\QL}alligators-BLoveAllM}
 Bouncer loves all the monkeys that live at the zoo.
\item \label{pr.{\QL}alligators-LoveHimBack}
 All the monkeys that Amos loves love him back.
%\item \label{pr.{\QL}alligators-AnyReptAmos}
% If any animal is an reptile, then Amos is.
\item \label{pr.{\QL}alligators-All->Rept}
 If any animal is an alligator, then it is a reptile.
\item \label{pr.{\QL}alligators-MLovedCleo}
 Every monkey that Cleo loves is also loved by Amos.
\item \label{pr.{\QL}alligators-MLovesBSad}
 There is a monkey that loves Bouncer, but Bouncer does not reciprocate this love.
\end{problist}
\end{exers}

\vbox{% !!!
\begin{exers}
\label{pr.SwimTranslate}
 Using the given symbolization key, translate each English-language assertion into {\QL}.
 \smallskip % !!!
 \begin{multicols}{2}
\begin{ekey}
\item[\univ ] The set of all animals.
\item[D] The set of all dogs.
\item[S] The set of all animals \hbox to 0pt{who like to swim.\hss} % !!!
\item[x \mathrel{L} y] $x$ is larger than $y$.
\item[b] Bertie
\item[e] Emerson
\item[f] Fergis
\end{ekey}
\end{multicols}
\smallskip % !!!
\begin{problist}
\item \label{pr.SwimTranslate-BDS}
Bertie is a dog who likes to swim.
\item \label{pr.SwimTranslate-BEFD}
Bertie, Emerson, and Fergis are all dogs.
\item \label{pr.SwimTranslate-ELBFLE}
Emerson is larger than Bertie, and Fergis is larger than Emerson.
\item \label{pr.SwimTranslate-DS}
All dogs like to swim.
\item \label{pr.SwimTranslate-ASD}
Every animal that likes to swim is a dog.
\item \label{pr.SwimTranslate-DLE}
There is a dog that is larger than Emerson.
%mult\item If there is a dog larger than Fergis, then there is a dog larger than Emerson.
\item \label{pr.SwimTranslate-nASLE}
No animal that likes to swim is larger than Emerson.
%\item Fergis is the largest dog.
\item \label{pr.SwimTranslate-AnSLB}
Any animal that does not like to swim is larger than Bertie.
\item \label{pr.SwimTranslate-EALBSE}
There is an animal that is larger than Bertie, but smaller than Emerson.
\item \label{pr.SwimTranslate-nDLBSE}
There is no dog  that is larger than Bertie, but smaller than Emerson.
\item \label{pr.SwimTranslate-nDLD}
No dog is larger than itself.
%mult\item Every dog is larger than some dog.
%mult\item There is an animal that is smaller than every dog.
%mult\item If there is an animal that is larger than any dog, then that animal does not like to swim.
\end{problist}
\end{exers}
}

\begin{exers}
\label{pr.{\QL}deductions}
For each deduction, write a symbolization key and translate the deduction into {\QL}.
\begin{problist}
\item \label{pr.{\QL}deductions-desk}
Nothing on my desk escapes my attention. There is a computer on my desk. Therefore, there is a computer that does not escape my attention.
\item \label{pr.{\QL}deductions-dreams}
 All my dreams are black and white. Old TV shows are in black and white. Therefore, some of my dreams are old TV shows.
\item \label{pr.{\QL}deductions-Holmes}
 Neither Holmes nor Watson has been to Australia. A person could see a kangaroo only if they had been to Australia or to a zoo. Although Watson has not seen a kangaroo, Holmes has. Therefore, Holmes has been to a zoo.
\item \label{pr.{\QL}deductions-SpInq}
 No one expects the Spanish Inquisition. No one knows the troubles I've seen. Therefore, anyone who expects the Spanish Inquisition knows the troubles I've seen.
\item \label{pr.{\QL}deductions-thinking}
 Every antelope is bigger than a bread box. The thing I am thinking of is no bigger than a bread box, and it is either an antelope or a cantaloupe. Therefore, I am thinking of a cantaloupe.
\end{problist}
\end{exers}



\subsection{\index{multiple!quantifiers}Multiple quantifiers} \label{sec.multiplequant}

\begin{eg}
Consider the following symbolization key and the assertions that follow it:
%\begin{ekey}
%\item[\univ ] People and dogs
%\item[D(x)] $x$ is a dog.
%\item[F(x,y)] $x$ is a friend of $y$.
%\item[O(x,y)] $x$ owns $y$.
%\item[f] Fifi
%\item[g] Gerald
%\end{ekey}

%\begin{assertlist}
%\item[\ex{dog1}] Fifi is a dog.
%\item[\ex{dog2}] Gerald is a dog owner.
%\item[\ex{dog3}] Someone is a dog owner.
%\item[\ex{dog4}] All of Gerald's friends are dog owners.
%\item[\ex{dog5}] Every dog owner is the friend of a dog owner.
%\end{assertlist}

%\assert{dog1} is easy: $D(f)$.

%\assert{dog2} can be paraphrased as, ``There is a dog that Gerald owns\rlap.'' This can be translated as $\exists x, \bigl(D(x) \eand O(g,x) \bigr)$.

%\assert{dog3} can be paraphrased as, ``There is some $y$, such that $y$ is a dog owner\rlap.'' The subassertion ``$y$ is a dog owner'' is just like \assert{dog2}, except that it is about $y$ rather than being about Gerald. So we can translate \assert{dog3} as $\exists y, \exists x, \bigl( D(x) \eand O(y,x) \bigr)$. 
%%(Although we could swap the $x$s and $y$s, it is important that we use two different variables here.)

%\assert{dog4} can be paraphrased as, ``Every friend of Gerald is a dog owner\rlap.'' Translating part of this assertion, we get 
%$$\forall x, \bigl( F(x,g) \eif\mbox{``$x$ is a dog owner''} \bigr) .$$
% Again, it is important to recognize that ``$x$ is a dog owner'' is structurally just like \assert{dog2}. However, since we are already using~$x$ to represent the dog owner, we will need a different variable for the existential quantifier. Any other variable will do. Using $z$, \assert{dog4} can be translated as $\forall x, \bigl[F(x,g) \eif\exists z, \bigl(D(z) \eand O(x,z) \bigr)\bigr]$.

%\assert{dog5} can be paraphrased as ``For any $x$ that is a dog owner, there is a dog owner who is $x$'s friend\rlap.'' Partially translated, this becomes 
%$$\forall x,\bigl[\mbox{$x$ is a dog owner}\eif\exists y, \bigl(\mbox{$y$ is a dog owner}\eand F(x,y) \bigr)\bigr].$$ 
%Completing the translation, \assert{dog5} becomes 
%$$\forall x,\bigl[\exists z, \bigl(D(z) \eand O(x,z) \bigr)\eif\exists y, \bigl(\exists z, (D(z) \eand O(y,z) \bigr)\eand F(x,y)\bigr].$$

%Consider this symbolization key and these assertions:
\begin{multicols}{2}
\begin{ekey}
\item[\univ ] The set of all people.
%\item[F(x,y)] $x$ is a friend of $y$.
\item[F]The set of all of \hbox to 0pt{Karl's friends.\hss} % !!!
\item[N]The set of all of \hbox to 0pt{Imre's neighbours.\hss} % !!!
\item[x \mathrel{L} y] $x$ likes $y$.
\item[i] Imre.
\item[k] Karl.
\end{ekey}
\end{multicols}
\begin{assertlist}
\item[\ex{likes1}]All of Imre's neighbours like all of Karl's friends.
\item[\ex{likes2}]At least one of Karl's friends likes at least one of Imre's neighbours.
\item[\ex{likes3}]All of Karl's friends like at least one of Imre's neighbours.
\item[\ex{likes4}]There is one of Imre's neighbours, who is a friend of Karl and who likes all of Imre's neighbours.
\end{assertlist}

Beginning to translate \assert{likes1}, we start with all of Imre's neighbours: $\forall n \in N.$  Now we would like to say $n \mathrel{L}f$, where $f$ represents every one of Karl's friends.  Before we can do this, we need to introduce the variable $f$, and give it the desired meaning and the appropriate quantifier: $\forall f \in F$.  Thus, \assert{likes1}  can be translated as 
$\forall n \in N, \bigl(\forall f \in F, (n \mathrel{L}f)\bigr)$.

For \assert{likes2}, we start with at least one of Karl's friends.  Another way to say this is that there is some friend of Karl's: $\exists f \in F$.  Similarly, we now need to introduce at least one of Imre's neighbours: $\exists n \in N$.  The completed translation is $\exists f \in F, \bigl(\exists n \in N, (f \mathrel{L}n)\bigr)\bigr)$.

For \assert{likes3}, we start with all of Karl's friends: $\forall f \in F$.  Now we need at least one of Imre's neighbours: $\exists n \in N$.  The completed translation is $\forall f\in F, \bigl(\exists n\in N, (f \mathrel{L} n)\bigr)$.

Finally, for \assert{likes4}, we start with one of Imre's neighbours: $\exists n \in N$.  Now we need this person to be a friend of Karl: $n \in F$.  For the next part of the sentence, we need all of Imre's neighbours.  It is tempting to write $\forall n \in N$, but we have already used the variable $n$ for a particular one of Imre's neighbours, so we cannot use it again here to mean something else.  Let's use $n'$ instead: $\forall n' \in N$.  We are now ready to translate \assert{likes4}: 
	$$\exists n \in N, \bigl( n\in F \eand \bigl[\forall n' \in N, (n \mathrel{L} n')\bigr]\bigr).$$
(Alternatively, we could have used $n_1$ and~$n_2$ instead of $n$ and~$n'$.)
\end{eg}

When symbolizing assertions with multiple quantifiers, it is best to proceed by small steps. Figure out who is being discussed in the sentence, and what quantifiers are required to introduce these variables. Paraphrase the English assertion so that the logical structure is readily symbolized in {\QL}. Then translate bit by bit, replacing the daunting task of translating a long assertion with the simpler task of translating shorter formulas.

\begin{rem} \label{EqualsSign}
The equals sign ``$=$''%
\nindex{$=$}
is a part of every symbolization key (even though we do not bother to include it explicitly). It is a binary predicate, and, as you would expect, ``$x = y$'' means ``$x$~is equal to~$y$\rlap.'' 
%(One often writes $x \mathbin{R} y$, instead of $R(x,y)$, when $R$ is a binary predicate.) 
This does not mean merely that $x$ and~$y$ look very much alike, or that they are indistinguishable, or that they have all of the same properties. Rather, it means that $x$ and~$y$ are (different) names for the same object.  
\end{rem}

%Consider this symbolization key and these assertions:
%
%\begin{ekey}
%\item[\univ] The set of all people.
%\item[H]The set of people who owe money to Hikaru.
%\item[p] Pavel
%\item[h] Hikaru
%\end{ekey}
%
%\begin{assertlist}
%%\item[\ex{else1}] Pavel owes money to everyone else.
%\item[\ex{else3}] No one other than Pavel owes money to Hikaru.
%\item[\ex{else4}] Only Pavel owes Hikaru money.
%\end{assertlist}
%
%
%%\assert{else1} can be paraphrased as, ``Everyone who is not Pavel is owed money by Pavel\rlap.'' This is an assertion structure we already know how to symbolize: ``For all $x$, if $x$ is not Pavel, then $x$ is owed money by Pavel\rlap.'' This translates to $\forall x,  \bigl((x\neq p) \eif O(p,x) \bigr)$.
%%(We use $x \neq y$ as an abbreviation for $\enot(x = y)$.)
%
%\assert{else3} can be paraphrased as, ``There is no one who owes money to Hikaru and is not Pavel\rlap.'' This can be translated as $\enot\exists h \in H, h \neq p$. (We use $x \neq y$ as an abbreviation for $\enot(x = y)$.) Simplifying, this is logically equivalent to $\forall h\in H, h = p$, which can be paraphrased as, ``Any person that owes Hikaru must be Pavel\rlap.'' 
%
%\assert{else4} can be paraphrased as, ``Pavel owes Hikaru \emph{and} any person that owes Hikaru must be Pavel\rlap.'' We have already translated the second conjunct, and the first is straightforward. \assert{else4} becomes $p \in H \eand ( \forall h\in H, h = p )$.
%
%\begin{exers}
%\label{pr.{\QL}cards}
%Using the given symbolization key, translate each English-language assertion into {\QL}. % with identity. The last two assertions are ambiguous and can be translated two ways; you should provide both translations for each.
%%\hint{Some of these assertions require ``=\rlap.''}
%\begin{ekey}
%\item[\univ ] The set of all cards in a standard deck.
%\item[C] The set of all clubs.
%\item[B] The set of all black cards.
%%\item[B(x)] $x$ is black.
%%\item[C(x)] $x$ is a club.
%\item[D] The set of all deuces.
%\item[J] The set of all jacks.
%%\item[M(x)] $x$ is a man with an axe.
%%\item[O(x)] $x$ is one-eyed.
%\item[W] The set of all wild cards.
%\end{ekey}
%\begin{problist}
%%\item All clubs are black cards.
%%\item There are no wild cards.
%\item \label{pr.{\QL}cards-2clubs}
% There are at least two clubs.
%\item \label{pr.{\QL}cards-moreblackjack}
% There is more than one black jack.
%%\item There are at most two one-eyed jacks.
%\item \label{pr.{\QL}cards-2blackjacks}
% There are exactly two black jacks.
%%\item There are four deuces.
%%\item There is a unique deuce of clubs. %, and it is a black card.
%%\item One-eyed jacks and any man with an axe are wild.
%\item \label{pr.{\QL}cards-deucewild}
% If there is a deuce of clubs, then it is the only wild card.
%\item \label{pr.{\QL}cards-3clubs}
%There are at least three clubs.
%%\item The man with the axe is not a jack.
%%\item The deuce of clubs is not the man with the axe.
%\end{problist}
%\end{exers}



\begin{warn}
 It is important to put quantifiers in the correct order. For example, consider the following assertions (with $\univ$ being the set of all objects):
% \begin{ekey}
% \item[\univ] everything
% \end{ekey}
\begin{assertlist}
\item[\ex{quantifierorderok}]  $\forall x,\bigl( \exists y, (x=y)\bigr)$
\item[\ex{quantifierorderbad}] $\exists y, \bigl(\forall x, (x=y)\bigr)$
\end{assertlist}
They are exactly the same, except for which of $\forall x$ and~$\exists y$ is first, and which is second. \assert{quantifierorderok} is obviously true: ``For every thing, there is something that it is equal to\rlap.'' (Namely, every thing is equal to itself.) But \assert{quantifierorderbad} says: ``There is some thing (let us call it~$y$), such that everything is equal to~$y$\rlap.'' There is no such~$y$, so this is obviously false.
\end{warn}

\begin{exers} \label{pr.SwimTranslateAgain}
 Using the symbolization key from \cref{pr.SwimTranslate}, translate each English-language assertion into {\QL}.
\begin{problist}
\item \label{pr.SwimTranslateAgain-DFDE}
If there is a dog larger than Fergis, then there is a dog larger than Emerson.
\item \label{pr.SwimTranslateAgain-DLD}
Every dog is larger than some dog.
\item \label{pr.SwimTranslateAgain-ASD}
There is an animal that is smaller than every dog.
%\item If there is an animal that is larger than any dog, then that animal does not like to swim.
\item \label{pr.SwimTranslateAgain-ALDES}
If there is an animal that is larger than every dog, then Emerson does not like to swim.
\item \label{pr.SwimTranslateAgain-DSSD}
For every dog that likes to swim, there is a smaller dog that does not like to swim.
\item \label{pr.SwimTranslateAgain-DSLDL}
Every dog that likes to swim is larger than every dog that does not like to swim.
\item \label{pr.SwimTranslateAgain-ALDS}
Some animal is larger than all of the dogs that like to swim.
%\item If there is an animal that likes to swim, than all of the dogs are larger than it.
\item \label{pr.SwimTranslateAgain-DSDLAS}
If there is a dog that does not like to swim, than there is a dog that is larger than every animal that likes to swim.
\end{problist}
\end{exers}

\begin{exers}[(harder)] \label{pr.{\QL}ballet}
Use the symbolization key to translate each English-language assertion into {\QL}.
\begin{multicols}{2}
\begin{ekey}
\item[\univ ] The set of all people.
\vskip1.6\baselineskip % !!!
\item[D] The set of \hbox to 0pt{all ballet dancers.\hss} % !!!
\item[F] The set of all females.
\item[M] The set of all males.
\columnbreak
\item[x \mathrel{C} y] $x$ is a child of $y$.
\item[x \mathrel{S} y] $x$ is a sibling of $y$.
\item[e] Elmer
\item[j] Jane
\item[p] Patrick
\end{ekey}
\end{multicols}
\begin{problist}
%\item All of Patrick's children are ballet dancers.
%\item Jane is Patrick's daughter.
%\item Patrick has a daughter.
%\item Jane is an only child.
%\item All of Patrick's daughters dance ballet.
%\item Patrick has no sons.
%\item Jane is Elmer's niece.
%\item Patrick is Elmer's brother.
\item \label{pr.{\QL}ballet-BCB}
Everyone who dances ballet is the child of someone who dances ballet.
\item \label{pr.{\QL}ballet-MBCB}
Every male who dances ballet is the child of someone who dances ballet.
\item \label{pr.{\QL}ballet-BSB}
Everyone who dances ballet has a sister who also dances ballet.
\item \label{pr.{\QL}ballet-JA}
Jane is an aunt.
\item \label{pr.{\QL}ballet-PBC}
Patrick's brothers have no children.
\end{problist}
\end{exers}



\subsection{Uniqueness}

Saying ``there is a \define{unique} so-and-so'' means not only that there is a so-and-so, but also that there is only one of them---there are not two different so-and-so's. For example, to say that
``there is a \emph{unique} person who owes Hikaru money'' means 
\begin{quote}
 some person owes Hikaru 
 \emph{and} no other person owes Hikaru.
 \end{quote}
 This translates to
 $$ \exists h\in H, \bigl( \forall y, (y \neq h \eif y \notin H) \bigr);$$
 or, equivalently,
 $$ \exists h\in H, \bigl( \forall y, ( y \in H \eif y =h ) \bigr).$$ 
Unfortunately, both of these are quite complicated expressions (and are examples of ``multiple quantifiers\rlap,'' because they use both $\exists$ and~$\forall$). To simplify the situation, mathematicians introduce a special notation:
 \factoidbox{``$\exists!\, x$'' means ``there is a unique $x$, such that\dots''%
 \nindex{$\exists!$}%
 }
 \factoidbox{If $X$ is any set, then ``$\exists!\, x \in X$'' means 
 \\``there is a unique $x$ in~$X$, such that\dots''}
For example, $\exists!\, h, h \in H$ means exactly the same thing as the complicated expression above.

If we add 
\begin{ekey}
\item[R]The set of people who are rich.
\end{ekey}
to our symbolization key, we can translate ``There is a unique rich person who owes Hikaru money\rlap.''  
%First notice that this is the same as saying ``There is a unique person who owes Hikaru money, and is rich\rlap.''  Now this translates as
Namely, it translates as:
$$\exists!\, r \in R, (r \in H).$$

%\begin{rem}
%Consider the assertion, 
%\begin{assertlist}
%\item [\ex{unique1}] There is a unique person who owes Hikaru money, and that person is rich.
%\end{assertlist}
%It would be tempting to translate this as $\exists!\, h \in H, R(h)$, but this actually means that there exists a unique person who \emph{both} owes Hikaru money \emph{and} is rich.  In such a case, there could be additional people who owe Hikaru money, as long as they are not rich.  As this was not the intent of \assert{unique1}, we need to rephrase the English to make it clearer how to proceed with translation.  

%\assert{unique1} can be rephrased as, ``There is a unique person who owes Hikaru money, and all of the people who owe Hikaru money are rich\rlap.''  This is true because as long as there is only one person who owes Hikaru money, then any property of that person is held by all of the people who owe Hikaru money.  Thus, an appropriate translation into {\QL} is
%$$(\exists!\, h, h \in H) \eand \bigl(\forall k \in H, R(k)\bigr).$$
%\end{rem}

\begin{exers} \label{pr.pegasus}
Using the given symbolization key, translate each English-language assertion into {\QL}. %with identity. The last two assertions are ambiguous and can be translated two ways; you should provide both translations for each.
\begin{ekey}
\item[\univ ] The set of all creatures.
\item[H] The set of all horses.
\item[W] The set of all creatures with wings.
\item[B] The set of all creatures in Farmer Brown's field.
\end{ekey}
\begin{problist}
%\item There are at least three horses in the world.
%\item There are at least three animals in the world.
%\item There is more than one horse in Farmer Brown's field.
%\item There are no more than three horses in Farmer Brown's field.
\item \label{pr.pegasus-ExistsUniqueWinged}
 There is a unique winged creature that is in Farmer Brown's field.
%\item Every Pegasus is a winged horse.
%\item There is a creature in Farmer Brown's field that is not a horse.
%\item The horse in Farmer Brown's field does not have wings.
%\item \label{pr.pegasus-NotPegasus}
% There is a unique winged horse in Farmer Brown's field, but it is not a Pegasus.
\item \label{pr.pegasus-UniqueHorse}
 If some horse has wings, then there is a unique horse that is in Farmer Brown's field.
\item \label{pr.pegasus-UniqueWinged}
 If there is a horse that is in Farmer Brown's field, then there is a unique horse that is in Farmer Brown's and has wings.
\end{problist}
\end{exers}


%\fix{glossary?}
%free variable
%bound variable
%scope


%\solutions
%\problempart
%\label{pr.wiff{\QL}}
%For each of the following: (a) Is it a wff of {\QL}, allowing for notational conventions? (b) Is it an assertion of {\QL}?
%\begin{assertlist}
%\item $\forall x\forall y[(Rxy \eand Ryx) \eif \exists zRzz]$
%\end{assertlist}

%%\solutions
%\problempart
%\label{pr.free{\QL}}
%Identify which variables are bound and which are free.
%\begin{assertlist}
%\item $\exists x Lxy \eand \forall y Lyx$
%\item $\forall x Ax \eand Bx$
%\item $\forall x (Ax \eand Bx) \eand \forall y(Cx \eand Dy)$
%\item $\forall x\exists y[Rxy \eif (Jz \eand Kx)] \eor Ryx$
%\item $\forall x_1(Mx_2 \eiff Lx_2x_1) \eand \exists x_2 Lx_3x_2$
%\end{assertlist}


%\problempart
%\begin{assertlist}
%\item Are there any wffs of {\QL} that contain more than one x-quantifier? If your answer is yes, give an example.
%\end{assertlist}




%\problempart
%\label{pr.BarbaraEtc}
%These are syllogistic figures identified by Aristotle and his successors, along with their medieval names. Translate each deduction into {\QL}.
%\begin{description}
%\item[Barbara] All $B$s are $C$s. All $A$s are $B$s.
%	\therefore\  All $A$s are $C$s.
%\item[Baroco] All $C$s are $B$s. Some $A$ is not $B$.
%	\therefore\  Some $A$ is not $C$.
%\item[Bocardo] Some $B$ is not $C$. All $A$s are $B$s.
%	\therefore\  Some $A$ is not $C$.
%\item[Celantes] No $B$s are $C$s. All $A$s are $B$s.
%	\therefore\  No $C$s are $A$s.
%\item[Celarent] No $B$s are $C$s. All $A$s are $B$s.
%	\therefore\  No $A$s are $C$s.
%\item[Cemestres] No $C$s are $B$s. No $A$s are $B$s.
%	\therefore\  No $A$s are $C$s.
%\item[Cesare] No $C$s are $B$s. All $A$s are $B$s.
%	\therefore\  No $A$s are $C$s.
%\item[Dabitis] All $B$s are $C$s. Some $A$ is $B$.
%	\therefore\  Some $C$ is $A$.
%\item[Darii] All $B$s are $C$s. Some $A$ is $B$.
%	\therefore\  Some $A$ is $C$.
%\item[Datisi] All $B$s are $C$s. Some $A$ is $B$.
%	\therefore\  Some $A$ is $C$.
%\item[Disamis] Some $B$ is $C$. All $A$s are $B$s.
%	\therefore\  Some $A$ is $C$.
%\item[Ferison] No $B$s are $C$s. Some $A$ is $B$.
%	\therefore\  Some $A$ is not $C$.
%\item[Ferio] No $B$s are $C$s. Some $A$ is $B$.
%	\therefore\  Some $A$ is not $C$.
%\item[Festino] No $C$s are $B$s. Some $A$ is $B$.
%	\therefore\  Some $A$ is not $C$.
%\item[Baralipton] All $B$s are $C$s. All $A$s are $B$s.
%	\therefore\  Some $C$ is $A$.
%\item[Frisesomorum] Some $B$ is $C$. No $A$s are $B$s.
%	\therefore\  Some $C$ is not $A$.
%\end{description}






%\solutions
%\problempart
%\label{pr.{\QL}candies}
%Using the given symbolization key, translate each English-language assertion into {\QL}.
%\begin{ekey}
%\item[\univ ] The set of all candies.
%\item[C(x)] $x$ has chocolate in it.
%\item[M(x)] $x$ has marzipan in it.
%\item[S(x)] $x$ has sugar in it.
%\item[T(x)] Boris has tried $x$.
%\item[B(x,y)] $x$ is better than $y$.
%\end{ekey}
%\begin{problist}
%\item Boris has never tried any candy.
%\item Marzipan is always made with sugar.
%\item Some candy is sugar-free.
%%\item The very best candy is chocolate.
%\item No candy is better than itself.
%\item Boris has never tried sugar-free chocolate.
%\item Boris has tried marzipan and chocolate, but never together.
%%\item Boris has tried nothing that is better than sugar-free marzipan.
%\item Any candy with chocolate is better than any candy without it.
%%\item Any candy with chocolate and marzipan is better than any candy that lacks both.
%\end{problist}



%\problempart \label{pr.potluck}
%Using the given symbolization key, translate each English-language assertion into {\QL}.
%\begin{ekey}
%\item[\univ ] people and dishes at a potluck
%\item[R(x)] $x$ has run out.
%\item[T(x)] $x$ is on the table.
%\item[F(x)] $x$ is food.
%\item[P(x)] $x$ is a person.
%\item[L(x,y)] $x$ likes $y$.
%\item[e] Eli
%\item[f] Francesca
%\item[g] the guacamole
%\end{ekey}
%\begin{problist}
%\item All the food is on the table.
%\item If the guacamole has not run out, then it is on the table.
%\item Everyone likes the guacamole.
%\item If anyone likes the guacamole, then Eli does.
%\item Francesca only likes the dishes that have run out.
%\item Francesca likes no one, and no one likes Francesca.
%\item Eli likes anyone who likes the guacamole.
%\item Eli likes anyone who likes the people that he likes.
%\item If there is a person on the table already, then all of the food must have run out.
%\end{problist}



%\problempart
%Using the given symbolization key, translate each English-language assertion into {\QL}. % with identity. The last assertion is ambiguous and can be translated two ways; you should provide both translations. (Hint: Identity is only required for the last four assertions.)
%\\ \hint{``=''~is required for the last two assertions.}
%\begin{ekey}
%\item[\univ ] people
%\item[K(x)] $x$ knows the combination to the safe.
%\item[S(x)] $x$ is a spy.
%\item[V(x)] $x$ is a vegetarian.
%\item[T(x,y)] $x$ trusts $y$.
%\item[h] Hofthor
%\item[i] Ingmar
%\end{ekey}
%\begin{assertlist}
%\item Hofthor is a spy, but no vegetarian is a spy.
%\item No one knows the combination to the safe unless Ingmar does.
%\item No spy knows the combination to the safe.
%\item Neither Hofthor nor Ingmar is a vegetarian.
%\item Hofthor trusts a vegetarian.
%\item Everyone who trusts Ingmar trusts a vegetarian.
%\item Everyone who trusts Ingmar trusts someone who trusts a vegetarian.
%\item Only Ingmar knows the combination to the safe.
%\item Ingmar trusts Hofthor, but no one else.
%%\item The person who knows the combination to the safe is a vegetarian.
%%\item The person who knows the combination to the safe is not a spy.
%\end{assertlist}



\subsection{Bound variables}

Recall that an assertion is a statement that is either true or false.
For example, consider the following symbolization key:
\begin{multicols}{2}
\begin{ekey}
\item [\univ] The set of all students.
\item [M(x)] $x$ is taking a math class.
\item [a] Anna
\end{ekey}
\end{multicols}
\noindent Then:
\begin{itemize}
\item $M(a)$ is an assertion. Either Anna is taking a math class, or she is not.
\item $M(x)$ is \emph{not} an assertion. The letter~$x$ is a variable, not any particular object. (We call $x$ a \define[variable!free]{free variable}.) If we plug in a particular value for~$x$ (such as~$a$), then we will have an assertion. However, until some value is plugged in for~$x$, we cannot say whether the expression is true or false. So the expression is not an assertion if the variable remains free.
\item $\exists x, M(x)$ and $\forall x, M(x)$ are assertions. The letter $x$ is a variable in both of these expressions, but it is no longer free, because it is acted on by the quantifier. (We call $x$ a \define[variable!bound]{bound variable}.) 
\end{itemize}
An important principle of {\QL} is that, in an assertion, each variable must be bound by some quantifier:
\factoidbox{Assertions cannot have free variables.}

\begin{exers} \label{FreeVarExer}
Suppose that $p$ is a constant, but all other lower-case letters represent variables.
For each of the following,
% want to be able to reference (a) and (b) (this assumes enumiv counter is not being used !!!)
\setcounter{enumiv}{0}\renewcommand{\theenumiv}{\alph{enumiv}}%
\makeatletter\renewcommand{\p@enumiv}{}\makeatother
\refstepcounter{enumiv}\label{FreeVarExer-free}\pref{FreeVarExer-free}~does it have a free variable? 
\refstepcounter{enumiv}\label{FreeVarExer-assert}\pref{FreeVarExer-assert}~is it an assertion?
\begin{tasks}(2)
\task\fixtask \label{FreeVarExer-L(x,y)}%
 $\forall x\in X, (x \mathrel{L} y)$
\task\fixtask \label{FreeVarExer-T(y,p)}%
 $(p \in S) \eand \exists y \in Y, (y  \mathrel{T} p)$
\task\fixtask \label{FreeVarExer-v=z}%
 $\forall v \in V, \bigl( (\exists!\, y \in Y, v  \mathrel{R} y) \eif (v=z) \bigr)$
\task\fixtask \label{FreeVarExer-xinT}%
 $y \in Y \eand \bigl(\forall x \in X, (x \in T) \bigr)$
\task\fixtask \label{FreeVarExer-L(x,p)}%
 $(p \mathrel{L} p) \eif \exists x, (x \mathrel{L} p)$
\task\fixtask \label{FreeVarExer-L(x,x)}%
 $\forall x \in X, (x \mathrel{L} x)$
\end{tasks}
\end{exers}




\section{Negations} \label{sect.predicate.negation}

Recall part of the symbolization key of \cref{sec.quantifiers}:
\begin{ekey}
\item[\univ] The set of all people.
\item[A] The set of all angry people.
\item[H(x)] The set of all happy people.
%\item[T_1(x,y)] $x$ is at least as tall as $y$.
%\item[T_2(x,y)] $x$ is at least as tough as $y$.
%%\item[B(x,y,z)] $y$ is between $x$ and $z$.
%\item[d] Donald
%\item[g] Gregor
%\item[m] Marybeth
\end{ekey}

Consider these further assertions:
\begin{assertlist}
\item[\ex{q.ne}] No one is angry.
\item[\ex{q.na}] Not everyone is happy.
%\item[\ex{q.en}] There is someone who is not happy.
\end{assertlist}

\assert{q.ne} can be paraphrased as, ``It is not the case that someone is angry\rlap.'' (In other words, ``It is not the case that there exists a person who is angry\rlap.'') This is the negation of the assertion that there exists an angry person, so it can be translated using ``not'' and ``there exists'': $\enot \exists x, (x \in A)$. 

It is important to notice that \assert{q.ne} is equivalent to the assertion that ``Everyone is nonangry\rlap.'' This assertion can be translated using ``for all'' and ``not'': $\forall x, \enot (x \in A)$, or, in other words, $\forall x, (x \notin A)$. 
%Both of these are acceptable translations, because they are logically equivalent. 
%The critical thing is whether the negation comes before or after the quantifier.
In general:
\factoidbox{ $\enot \exists x,\script{A}$ is logically equivalent to $\forall x,\enot\script{A}$.%
%\\[5pt] $\enot \exists x \in X,\script{A}$ is logically equivalent to $\forall x \in X,\enot\script{A}$.
}
This means that the negation of a ``$\exists$''~assertion is a ``$\forall$''~assertion.
%In general, $\forall x,\script{A}$ is logically equivalent to $\enot\exists x,\enot\script{A}$. 
%This means that any assertion that can be symbolized with a universal quantifier can also be symbolized with an existential quantifier, and vice versa. One translation might seem more natural than the other, but there is no logical different in translating with one quantifier rather than the other. For some assertions, it will simply be a matter of taste.

\assert{q.na} says it is not true that everyone is happy. This is the negation of the assertion that everyone is happy, so it can be translated using ``not'' and~``$\forall$'': $\enot\forall x,(x \in H)$. 

Moreover, saying that not everyone is happy is the same as saying that someone is not happy. This latter assertion translates to $\exists x, (x \notin H)$. In general:
\factoidbox{$\enot \forall x,\script{A}$ is logically equivalent to $\exists x,\enot\script{A}$.%
%\\[5pt] $\enot \forall x \in X,\script{A}$ is logically equivalent to $\exists x \in X,\enot\script{A}$.
}
%This is logically equivalent to \assert{q.en} and so could also be translated as $\exists x, \enot H(x)$.
This means that the negation of a ``$\forall$''~assertion is a ``$\exists$''~assertion.

Just as for ``$\forall x$'' and ``$\exists x$\rlap,'' the bounded quantifiers ``$\forall x \in X$'' and ``$\exists x \in X$'' are interchanged under negation:
\factoidbox{$\neg \forall x \in X, \script{A}$ is logically equivalent to ``$\exists x \in X, \neg \script{A}$.
\\[5pt]
$\neg \exists x \in X, \script{A}$ is logically equivalent to ``$\forall x \in X, \neg \script{A}$.
}
There is no fundamental difference between this and the previous examples; we have simply replaced $\univ$ with the set~$X$.

In summary: if you need to negate an assertion that starts with a quantifier, switch the quantifier to the other one (from $\exists$ to $\forall$ or vice-versa), and then continue, negating the remainder of the assertion.

To perform the additional negations, you will want to remember the following rules from \cref{BasicEquivs}:
\factoidbox{ 
\bf Rules of Negation \\[10pt]
\rm
$\enot(A \eor B)$ is logically equivalent to $\enot A\eand \enot B$. \\[6pt]
$\enot(A \eand B)$ is logically equivalent to $\enot A\eor \enot B$. \\[6pt]
$\enot(A \eif B)$ is logically equivalent to $A \eand \enot B$.  \\[6pt]
$\enot \enot A$ is logically equivalent to $A$.
}
%Thus, when negating, we interchange $\eor$ with~$\eand$, but $\eif$ has a special rule of its own.
%To negate $\eiff$, recall that $\script{A}\eiff\script{B}$ is equivalent to $(\script{A}\eif\script{B}) \eand (\script{B}\eif \script{A})$, and use the rules for $\eand$ and $\eif$.

\begin{eg}
Let us simplify the assertion
\begin{align} \label{FirstDeMorganEg}
\tag{$*$}
\enot \forall s \in S, \biggl( \bigl( (s \in A) \eor (s \in B) \bigr) \eand \bigl( (s \in C) \eif (s \notin D) \bigr) \biggr) .
\end{align}
We bring $\enot$ inside the quantifier, switching from $\forall$ to~$\exists$:
$$\exists s \in S, \enot \biggl( \bigl( (s \in A) \eor (s \in B) \bigr) \eand \bigl( (s \in C) \eif (s \notin D) \bigr) \biggr) .$$
Now, we switch $\eand$ to~$\eor$, and apply $\enot$ to each of the two terms:
$$\exists s \in S, \biggl( \enot \bigl( (s \in A) \eor (s \in B) \bigr) \eor \enot \bigl( (s \in C) \eif (s \notin D) \bigr) \biggr) .$$
Next, the connective $\eor$ in the left term is changed to~$\eand$ (and $\enot$~is applied to the subterms), and the rule for negating $\eif$ is implied to the right term:
$$\exists s \in S, \biggl( \bigl( \enot (s \in A) \eand \enot (s \in B) \bigr) \eor \bigl( (s \in C) \eand \enot (s \notin D) \bigr) \biggr) .$$
Finally, we use the abbreviation $\notin$ in the first two terms, and eliminate the double negative in the final term:
$$\exists s \in S, \biggl( \bigl( (s \notin A) \eand (s \notin B) \bigr) \eor \bigl( (s \in C) \eand (s \in D) \bigr) \biggr) .$$
This final result is logically equivalent to Assertion~\pref{FirstDeMorganEg} above.
\end{eg}

The same principles apply to negating assertions in English. 

\begin{eg}
Suppose that we want to negate
\begin{quote}
``Every umbrella either needs a new handle or is not big enough\rlap.''
\end{quote}
We create a symbolization key:
\begin{ekey}
\item[U]The set of all umbrellas.
\item[H] The set of all umbrellas that need a new handle.
\item[B] The set of all umbrellas that are big enough.
\end{ekey}
Now we can translate the assertion as
$\forall u \in U, \bigl( (u \in H) \eor (u \notin B)\bigr).$
Negating this, we have $$\enot\forall u \in U, \bigl( (u \in H) \eor (u \notin B)\bigr).$$
We have just learned that this is equivalent to
$$\exists u \in U, \enot\bigl( (u \in H) \eor (u \notin B)\bigr),$$
which
can be simplified to
$$\exists u \in U, \bigl((u \notin H) \eand \enot(u \notin B)\bigr),$$
and finally, eliminating the double negative, this is equivalent to
$$\exists u \in U, \bigl((u \notin H) \eand (u \in B)\bigr).$$
Now we translate back to English:
\begin{quote}
``There is some umbrella that does not need a new handle and is  big enough\rlap.''
\end{quote}
%Note that 
%\begin{itemize}
%\item the universal quantifier (``every'') has changed to the existential quantifer (``there is''), 
%\item ``or'' has changed to ``and\rlap,''
%and
%\item  the subassertions (``needs a new handle'' and ``is not big enough'') have been negated.
%\end{itemize}
\end{eg}

Applying these rules systematically will enable you to simplify the negation of any assertion (no matter whether it is expressed in English or in {\QL}).

English is more open to interpretation and inexactitude than {\QL}. Therefore, when we need to negate an English assertion in this chapter, we translate it into {\QL}, perform the negation, and translate back.  You will also be expected to do this.  Later, when you are doing proofs, you might be able to work directly with the English version, although you may find it helpful to keep the {\QL} version in mind.  

%From this point on, you may apply any of the rules for negation to simplify assertions in a proof.  In a two-column proof, the justification will be ``$\enot$-simplify\rlap.''


\begin{warn}
To make an assertion, quantifiers must be applied to predicates --- they cannot stand by themselves. That is, an assertion must be of the form $\exists x \in X, P(x)$ or $\forall x\in X, P(x)$, not just $\exists x\in X$ or $\forall x \in X$.  For example, some students erroneously try to translate the assertion ``there exists an umbrella'' as \text{``$\exists u \in U$\rlap,''} but that is \textbf{not} an assertion. The problem is that it is not a complete sentence: it would translate into English as ``there exists an umbrella, such that\rlap.'' (Notice the ``such that'' left dangling at the end.)

One way to obtain a correct symbolization is to rephrase the original assertion as: ``there exists something that is an umbrella\rlap.'' This translates to $\exists x, (x \in U)$, which is a correct symbolization. Its negation simplifies to $\forall x, (x \notin U)$, which means ``every thing that exists is not an umbrella\rlap.''

If $\exists u \in U$ were an assertion, then, by applying the rules for negation, its negation would be ``$\forall u \in U, \enot$\rlap,'' which is not a complete sentence: its English translation is ``for all~$u$ in~$U$, it is not true that\rlap.'' 
To avoid such mistakes, remember that every quantifier must always be followed by a predicate. 
\end{warn}

%\assert{q.en} is most naturally paraphrased as, ``There is some $x$, such that $x$ is not happy\rlap.'' This becomes $\exists x, \enot H(x)$. Equivalently, we could write $\enot\forall x, H(x)$.

%Although we have two quantifiers in {\QL}, we could have an equivalent formal language with only one quantifier. We could proceed with only the universal quantifier, for instance, and treat the existential quantifier as a notational convention. We use square brackets [ ] to make some assertions more readable, but we know that these are really just parentheses ( ). In the same way, we could write ``$\exists x$'' knowing that this is just shorthand for ``$\enot \forall x \enot$\rlap.'' There is a choice between making logic formally simple and making it expressively simple. With {\QL}, we opt for expressive simplicity. Both $\forall$ and $\exists$ will be symbols of {\QL}.

\begin{exers}
\label{pr.EnglishNegate}
Negate each of the assertions in \cref{pr.{\QL}alligators}.
Express your answer both in the language of {\QL} and in English (after simplifying).
\end{exers}

\begin{exers} \label{QLNegate}
Negate each of the following assertions of {\QL}
 (and simplify, so that $\enot$ is not applied to anything but predicates or assertion variables). \emph{Show your work!}
 \begin{problist}
 \item \label{QLNegate-LMMN}
$(L \eif \enot M) \eand (M \eor N)$
 \item \label{QLNegate-ABC}
$\bigl( (a \in A) \eand (b \in B) \bigr) \eor (c \in C)$
 \item \label{QLNegate-APQR}
$\forall a \in A, \Bigl( \bigl( (a \in P) \eor (a \in Q) \bigr) \eand (a \notin R) \Bigr)$ 
 \item \label{QLNegate-ATCQR}
$\forall a \in A, \Bigl( (a \in T) \eif \exists c \in C, \bigl( (c \in Q) \eand ( c \mathrel{R} a) \bigr) \Bigr)$
 \item \label{QLNegate-ALBC}
$\forall x, \biggl( (x \in A) \eand \Bigl( \exists \ell \in L, \bigl( (x \mathrel{B} \ell ) \eor (\ell \in C) \bigr) \Bigr) \biggr)$
 \item \label{QLNegate-ABEDC}
$A \eif \Bigl( \bigl( \exists x \in X, (x \in B) \bigr) \eor \bigl( \forall e \in E, \exists d \in D, (e \mathrel{C} d) \bigr) \Bigr)$
 \item \label{QLNegate-ABCDKZ}
$\forall a \in A, \exists b \in B, \exists c \in C, \forall d \in D, \Bigl( (a \mathrel{K} b) \eand \bigl( (a \mathrel{Z} c) \eor (b > d) \bigr) \Bigr)$
  \end{problist}
\end{exers}


\begin{exers} \label{aInANegateEx}
Simplify each assertion.  \emph{Show your work!}
\begin{problist}
\item \label{aInANegateEx-PoQ}
$\neg \forall a \in A, \bigl( (a \in P) \eor (a \in Q) \bigr)$
\item \label{aInANegateEx-PaQ}
$\neg \exists a \in A, \bigl( (a \in P) \eand (a \in Q) \bigr)$
\item \label{aInANegateEx-AC}
$\neg \forall x \in X, \exists y \in Y, \bigl( (x \in A) \eand (x \mathrel{C} y) \bigr)$
\item \label{aInANegateEx-RTM}
$\neg \forall s \in S, \biggl(  (s \in R) \eif \Bigl( \exists t \in T, \bigl(  (s \neq t) \eand (s \mathrel{M} t) \bigr) \Bigr) \biggr)$
\end{problist}
\end{exers}

%\begin{rem}
%Mathematicians sometimes use a crossed-out symbol to represent a negation. In particular, we have already used the symbol $\neq$ for ``is \textbf{not} equal to\rlap,'' and the symbol $\notin$ for ``is not an element of\rlap.'' 
%Similarly, $\nexists$ is an abbreviation for $\enot\exists$, so, for example, ``$\nexists x \in X, (x \in A)$'' means ``there does \textbf{not} exist $x \in X$, such that $x \in A$\rlap.''
%This can be simplified to ``$\forall x \in X, (x \notin A)$\rlap.''
%\end{rem}

\begin{rem}
Unfortunately, there is no nice, compact way of negating assertions involving uniqueness.  For example, if we want to say ``It is not the case that there is a unique person who owes Hikaru money\rlap,'' we need to say that  ``Either no one owes Hikaru money, or more than one person owes Hikaru money\rlap.''  This translates to 
$$(H = \emptyset) \eor \bigl(\exists h_1 \in H, (\exists h_2 \in H, h_2 \neq h_1)\bigr).$$
%Although it is sometimes necessary to negate assertions involving uniqueness, we will not expect you to be able to do so at this point.  The example above should give you an idea of how to proceed, if you do 
In general, if you come across a situation where you want to negate an assertion that involves uniqueness, it is a good idea to rewrite the assertion without using ``$\exists!$\rlap.'' You should have no difficulty negating this rephrased assertion.
\end{rem}

% provide some exercises !!!


\subsection{Vacuous truth}

Note that if the assertion
	$$ \exists x \in A, \enot P(x)$$
is true (where $A$ is any set and $P(x)$ is  any unary predicate), then there must exist an element~$a$ of~$A$, such that $P(a)$ is false. Ignoring the last condition (about $P(a)$), we know that $a \in A$, so $A \neq \emptyset$. That is, we know:
	$$ \text{If the assertion \ $\exists x \in A, \enot P(x)$ \  is true, then $A \neq \emptyset$.} $$
So the contrapositive is also true:
	$$ \text{If $A = \emptyset$, then the assertion \ $\exists x \in A, \exists P(x)$ \ is false.} $$
Therefore, the assertion $\exists x \in \emptyset, \enot P(x)$ is false, so its negation is true:
	\factoidbox{The assertion $\forall x \in \emptyset, P(x)$ is true.}%
Since $P(x)$ is an arbitrary predicate, this means that any assertion about \emph{all} of the elements of the empty set is true; we say it is \define{vacuously true}.
The point is that there is nothing in the empty set to contradict whatever assertion you care to make about all of the elements.

\begin{eg}
If you say, ``All of the people on Mars have purple skin\rlap,'' and there are not any people on Mars, then you have spoken the truth --- otherwise, there would have to be some person on Mars (whose skin is not purple) to provide a counterexample.
\end{eg}

In summary:
\factoidbox{any assertion about \emph{all} of the elements of the empty set is \emph{vacuously true}.}

%This is related to the concept that ``If pigs fly, then cows are green\rlap.'' is a true assertion.  As long as it is impossible to produce a flying pig and a cow that is not green to falsify the assertion false, it is true by default.

\begin{exers} \label{VacuousExer}
Which of the following English assertions are vacuously true (in the real world)?
\begin{problist}
\item \label{VacuousExer-quintuplets}
 All quintuplets are sickly.
\item \label{VacuousExer-cards}
 All standard playing cards that are numbered fifteen, are green.
\item \label{VacuousExer-prime}
 All prime numbers that are divisible by 12, have 5 digits.
\item \label{VacuousExer-moon}
 All people who have been to the moon are men.
\item \label{VacuousExer-dead}
 All people who do not breathe are dead.
\end{problist}
\end{exers}





\section{The introduction and elimination rules for quantifiers} \label{IntroElimQuantSect}

As you know, there are two quantifiers ($\exists$ and~$\forall$). Each of these has an introduction rule and an elimination rule, so there are $4$~rules to present in this section. 
Proofs in {\QL} can use both of these rules, plus all of the rules of {\SL} (such as the rules of negation and the basic theorems, including introduction and elimination rules), and also any other theorems that have been previously proved.




\subsection{\texorpdfstring{$\exists$}{Exists}-introduction}\index{exists ($\exists$)!-introduction}
\label{ExistsIntroSect}

We need to determine how to prove a conclusion of the form 
$\exists x \in X, \dots$. 
For example, in a murder mystery, perhaps Inspector Thinkright gathers the suspects in a room and tells them, ``Someone in this room has red hair\rlap.'' That is a $\exists$-statement. (With an appropriate symbolization key, in which $P$~is the set of all of the the people in the room, and $R(x)$~is the predicate ``$x$~has red hair\rlap,'' it is the assertion $\exists p \in P, R(p)$.) How would the Inspector convince a skeptic that the claim is true? The easiest way would be to exhibit an explicit example of a person in the room who has red hair. For example, if Jim is in the room, and he has red hair, the Inspector might say,
\begin{quote}
``Look, Jim is sitting right there by the door, and now, when I take off his wig, you can see for yourself that he has red hair. So I am right that someone in this room has red hair\rlap.'' 
\end{quote}
In general, the most straightforward way to prove $\exists p \in P, R(p)$ is true is to find a specific example of a~$p$ that makes $R(p)$ true. That is the essence of the $\exists$-intro rule. 

Here is a principle to remember:
\factoidbox{The proof of an assertion that begins\\
``there exists~$x \in X$, such that\dots''
\\will usually be based on the statement ``Let $x =\raise 2pt \hbox{\boxit{\phantom{x}}}$\,\rlap,''
\\where the box is filled with an appropriate element of~$X$.}

\begin{otherterm}
Most mathematicians are not familiar with the terminology of introduction rules and elimination rules. 
Instead of saying this is the $\exists$-introduction rule, they would call it ``proof by constructing an example\rlap,'' or ``giving an explicit example\rlap,'' or other words to the same effect.
\end{otherterm}

Here are some proofs that use $\exists$-introduction, but we cannot do very much with only one quantifier rule --- the examples will be more interesting when we have more rules to work with.


\begin{eg}
Prove there is a natural number~$n$, such that $n^2 = 64$.
\end{eg}
\begin{proof}
Let $n = 8 \in \natural$. Then $n^2 = 8^2 = 64$.
\end{proof}

%\begin{eg}
%Show that if $8 \in X$, then there exists $b \in \real$, such that $b^3 \in X$.
%\end{eg}
%
%\begin{proof}
%Let $b = 2 \in \real$. Then $b^3 = 2^3 = 8 \in X$, as desired.
%\end{proof}

\begin{eg}
Prove there is a real number~$c$, such that $5c^2 - 5c + 1 < 0$.
\end{eg}
\begin{proof}
Let $c = 1/2 \in \real$. Then 
	\begin{align*}
	5c^2 - 5c + 1 
	= 5 \left(\frac{1}{2}\right)^2 - 5 \left(\frac{1}{2}\right) + 1
	= \frac{5}{4} - \frac{5}{2} + 1
	= -\frac{1}{4}
	< 0 
	. & \end{align*}
	\end{proof}
% same example in the notation of functions:
%\begin{eg}
%Define $f \colon \real \to \real$ by $f(x) = 5x^2 - 5x + 1$. Prove there is a real number~$c$, such that $f(c) < 0$.
%\end{eg}
%\begin{proof}
%Let $c = 1/2 \in \real$. Then 
%	$$f(c) 
%	= 5c^2 - 5c + 1 
%	= 5 \left(\frac{1}{2}\right)^2 - 5 \left(\frac{1}{2}\right) + 1
%	= \frac{5}{4} - \frac{5}{2} + 1
%	= -\frac{1}{4}
%	< 0 ,$$
%as desired.
%	\end{proof}

\begin{eg}
Let $N = \{1,3,5,7\}$. Prove there exists $n \in N$, such that $n^3-11n^2+31n \neq 21$.
\end{eg}
\begin{proof}
Let $n = 5 \in N$. Then 
	\begin{align*}
	n^3-11n^2+31n 
	= 5^3-11(5^2)+31(5)
	= 125 - 11(25) + 155
	= 125 - 275 + 155
	= 5
	\neq 21 . \end{align*}
\end{proof}

\begin{exers} \label{ExistPfExers} \ 
\begin{enumerate}
\item \label{ExistPfExers-f}
Prove there is a real number~$r$, such that  $2r^2 + 9r + 4 = 0$. 
% same in the notation of functions:
%Define $f \colon \real \to \real$ by $f(x) = 2x^2 + 9x + 4$. Prove there is a real number~$r$, such that $f(r) = 0$.

\item \label{ExistPfExers-B}
Let $B = \{1,3,5,7\}$.
Prove there exists $b \in B$, such that $3b + 1 = (b-1)^2$.

\item \label{ExistPfExers-mn}
 Prove there exist natural numbers $m$~and~$n$, such that $m^2 = n^3 + 1 > 1$.
\\ \hint{Try \emph{small} values of $m$ and~$n$.}
%\item \label{ExistPfExers-map}
% (\emph{harder}) Suppose that a map is made by drawing $n$~intersecting circles. Give two different proofs that there is a $2$-colouring of this map:
%\begin{enumerate}
%\item \label{ExistPfExers-map-induct}
% Use a proof by induction.
%\item \label{ExistPfExers-map-NumCirc}
% Construct an explicit $2$-colouring, by assigning colours based on the number of circles that contain each region.
%\end{enumerate}

\item \label{ExistPfExers-3n2=5n+2}
Show there is an integer~$n$, such that $3n^2 = 5n + 2$.

\item \label{ExistPfExers-7x-5=a}
Assume $a$ is a real number. Show there is a real number~$x$, such that
$7x - 5 = a$.

%\item \label{ExistPfExers-x2+1=ax}
%Assume $a$ is a real number, such that $a^2 > 1$. Show there is a real number~$x$, such that $x(x-2a) = - 1$.
%
%\item \label{ExistPfExers-CirclesIntersect}
%(harder)
%Assume $a$ and~$r$ are real numbers, such that $a^2 \le 4r^2$. Show there exist real numbers $x$ and~$y$, such that
%	$$ x^2 + y^2 = r^2$$
%and
%	$$ (x-a)^2 + y^2 = r^2 .$$

\end{enumerate}
\end{exers}



\subsection{\texorpdfstring{$\exists$}{Exists}-elimination}\index{exists ($\exists$)!-elimination}
\label{ExistsElimSect}

Perhaps Inspector Thinkright knows that one of the men lit a match at midnight, but does not know who it was. The Inspector might say,
\begin{quote}
``We know that one of the men lit a match at midnight. Let us call this mysterious gentleman `Mr.~X\rlap.' Because right-handed matches are not allowed on the island, we know that Mr.~X is left handed. Hence, Mr.~X is not a butler, because all of the butlers in this town are right handed. \dots''
\end{quote}
and so on, and so on, telling us more and more about Mr.~X, based only on the assumption that he lit a match at midnight (and other facts that are known to be true).

The situation in mathematical proofs is similar. Suppose we know there exists an element of the set~$A$. Then it would be helpful to have a name for this mysterious element, so that we can talk about it. But a mathematician would not call the element ``Mr.~X'': if it is an element of the set~$A$, then he or she would probably call it~$a$ (or $a_1$ if there are going to be other elements of~$A$ to talk about).  In general, the idea of the $\exists$-elimination rule is:
\factoidbox{If $\exists x \in X, P(x)$ is known to be true, then we may 
\\ let $x$ be an element of~$X$, such that $P(x)$ is true.
}
In the remainder of the proof, we may assume only two things about~$x$: 
that $x \in X$, and that $P(x)$ is true.

\begin{eg}
Show that if there exists $a \in \real$, such that $a^3 + a + 1 = 0$, then there exists $b \in \real$, such that $b^3 + b - 1 = 0$.
\end{eg}
\begin{proof}
Assume there exists $a \in \real$, such that $a^3 + a + 1 = 0$. Let $b = -a$. Then $b \in \real$, and
	\begin{align*}
	 b^3 + b - 1
	&= (-a)^3 + (-a) - 1
	\\&= -a^3 - a - 1
	\\&= -(a^3 + a + 1)
	\\&= -0 
	&& \text{(by the definition of~$a$)}
	\\&= 0
	, \end{align*}
as desired.
\end{proof}
% same example in the notation of functions:
%\begin{eg}
%Define $f \colon \real \to \real$ and $g \colon \real \to \real$ by $f(x) = x^3 + x + 1$ and $g(x) = x^3 + x - 1$. Show that if there exists $a \in \real$, such that $f(a) = 0$, then there exists $b \in \real$, such that $g(b) = 0$.
%\end{eg}
%\begin{proof}
%Assume there exists $a \in \real$, such that $f(a) = 0$. Let $b = -a$. Then
%	\begin{align*}
%	 g(b) 
%	&= g(-a) 
%	\\&= (-a)^3 + (-a) - 1
%	\\&= -a^3 - a - 1
%	\\&= -(a^3 + a + 1)
%	\\&= -f(a)
%	\\&= -0 
%	\\&= 0
%	, \end{align*}
%as desired.
%\end{proof}

\begin{exers} \label{ExistElimEx}
Assume $A$ and~$B$ are sets of real numbers. 
\begin{problist}
\item \label{ExistElimEx-b>0}
Show that if there exists $a \in A$, such that $2a > 5$, then there exists $b \in A$, such that $b > 0$.
\item \label{ExistElimEx-3yinA}
Show that if there exists $x \in \real$, such that $x - 2 \in A$, then there exists $y \in \real$, such that $3y \in A$.
\item \label{ExistElimEx-AcapB}
Show that if $A \cap B \neq \emptyset$, then $A \neq \emptyset$.
\end{problist}
\end{exers}



\subsection{\texorpdfstring{$\forall$}{All}-elimination}\index{all ($\forall$)!-elimination}
\label{AllElimSect}

Perhaps Inspector Thinkright knows that Jeeves is a butler in the town, and that all of the butlers in the town are right handed. Well, then it is obvious to the Inspector that Jeeves is right handed. This is an example of $\forall$-elimination: if you know something is true about every element of a set, then it is true about any particular element of the set.
\factoidbox{If $\forall x \in X, P(x)$ is true, and $a \in X$, then $P(a)$ is true.}

\begin{eg} \label{x2=9Eg}
Suppose 
\begin{enumerate}
\item $C \subset \real$, 
and
\item \label{x2=9Eg-x2=9}
$\forall x \in \real, \bigl( (x^2 = 9) \eif (x \in C) \bigr)$.
\end{enumerate}
Show $\exists c \in \real, c \in C$.
\end{eg}
\begin{proof}
Let $c = 3 \in \real$. Then $c^2 = 3^2 = 9$, and letting $x = c$ in Hypothesis~\pref{x2=9Eg-x2=9}  tells us that
	$$( c^2 = 9) \eif ( c \in C) .$$
Therefore $c \in C$.
\end{proof}
% same example in the notation of functions:
%\begin{eg}
%Suppose 
%\begin{itemize}
%\item $f,g \colon \real \to \real$, 
%\item $f(x) = x^2 - 9$ for all $x \in \real$,
%and
%\item $\forall x \in \real, \bigl( f(x) = 0 \eif g(x) = 0 \bigr)$.
%\end{itemize}
%Show $\exists c \in \real, g(c) = 0$.
%\end{eg}
%\begin{proof}
%Let $c = 3 \in \real$. Then $f(c) = 3^2 - 9 = 0$, and, because $c \in \real$, we know 
%	$$\bigl( f(c) = 0 \bigr) \eif \bigl( g(c) = 0 \bigr) .$$
%Therefore $g(c) = 0$.
%\end{proof}

% haven't done functions yet, so can't use this example !!!
%\begin{eg}
%Assume 
%	\begin{enumerate}
%	\item $f \colon \real \to \real $, 
%	and
%	\item \label{f(a)=16-f(x)=x2}
%	for all $x \in \real$, we have $f(x) = x^2$.
%	\end{enumerate}
%Show there exists $a \in \real$, such that $f(a) = 16$.
%\end{eg}
%\begin{proof}
%Let $a = 4$. Then, from Assumption~\pref{f(a)=16-f(x)=x2}, we know
%	$$ f(a) = a^2 = 4^2 = 16 ,$$
%as desired.
%\end{proof}

\begin{eg}
Assume $A \neq \emptyset$ and $A \subset B$. Prove $\exists b, (b \in B)$.
\end{eg}
\begin{proof}
Because $A$ is not the empty set, we know it has at least one element; that is, we have $\exists x, (x \in A)$. Hence, we may let $a$ be some element of~$A$. Now, let $b = a$. Because $A \subset B$, we know that every element of~$A$ is an element of~$B$. In particular, since $b = a \in A$, this means that $b \in B$. 
%So $\exists b, (b \in B)$.
\end{proof}

\begin{warn}
When applying $\forall$-elimination, the variable does not need to be called~``$x$\rlap,'' (it could be $y$ or~$z$ or any other variable), and the constant does not need to be called~``$a$'' (it could be any element of~$X$). However, if the variable occurs more than once in the formula, it is important to replace \emph{all} of its occurrences with~$a$. For example, if $a \in X$, then, from $\forall x \in X, \bigl( A(x) \eif B(x) \bigr)$, we can conclude $A(a) \eif B(a)$, but \emph{not} $A(a) \eif B(x)$ or $A(x) \eif B(a)$.
%(In fact, the latter two expressions are not assertions, as they contain the variable~$x$, and $x$~is no longer bound by a quantifier.)
\end{warn}



%We now have enough rules to do interesting proofs with quantifiers. 
%Here are some exercises to give you some practice with this.


\begin{exers} \label{AllElimExers} \ 

\begin{problist}

\item  \label{AllElimExers-16}
Assume \  $\forall x \in \real, (x^2 \in Z)$.
\ Show $16 \in Z$.

\item  \label{AllElimExers-SupsetNotEmpty}
Assume 
	$A \subset B$
	and
	$A \neq \emptyset$.
Show $B \neq \emptyset$.

\item  \label{AllElimExers-BNotEmpty}
Assume
	\begin{enumerate} \makeatletter \renewcommand{\p@enumii}{} \makeatother
	\item \label{BNotEmpty-all}
for every $x \in A$, either $x \in B$, or $x < 0$,
	and
	\item \label{BNotEmpty-exists}
there exists $a \in A$, such that $a > 0$.
	\end{enumerate}
Show $B \neq \emptyset$.


% haven't defined functions yet, so can't use these exercises!!!
%\item \label{AllElimExers-g(x1)neqg(x2)}
%Assume 
%	\begin{enumerate} \makeatletter \renewcommand{\p@enumii}{} \makeatother
%	\item $g \colon \real \to \real$, and 
%	\item \label{g(x1)neqg(x2)-g(x)=y}
%	for all $y \in \real$, there exists $x \in \real$, such that $g(x) = y$. 
%	\end{enumerate}
%Show there exist real numbers $x_1$ and~$x_2$, such that $g(x_1) \neq g(x_2)$.
%
%\item \label{AllElimExers-f(x1)+g(x2)=1}
%Assume 
%	\begin{enumerate} \makeatletter \renewcommand{\p@enumii}{} \makeatother
%	\item $f \colon \real \to \real$,
%	\item $g \colon \real \to \real$, and 
%	\item \label{f(x1)+g(x2)=1-onto}
%	for all $y \in \real$, there exists $x \in \real$, such that $g(x) = y$. 
%	\end{enumerate}
%Show there exist real numbers $x_1$ and~$x_2$, such that $f(x_1) + g(x_2) = 1$.
%
%\item \label{AllElimExers-0<f(c)<1}
%Assume
%	\begin{enumerate} \makeatletter \renewcommand{\p@enumii}{} \makeatother
%	\item $f \colon \real \to \real$,
%	\item \label{0<f(c)<1-AB}
%	$A$ and $B$ are two subsets of~$\real$ that are \emph{not} disjoint,
%	\item \label{0<f(c)<1-A}
%	$\forall a \in A, \ f(a) < 1$,
%	and
%	\item \label{0<f(c)<1-B}
%	$\forall b \in B, \ f(b) > 0$.
%	\end{enumerate}
%Show there exists a real number~$c$, such that $0 < f(c) < 1$.
%
%\item \label{AllElimExers-AcapBNonempty}
%Assume 
%	\begin{enumerate} \makeatletter \renewcommand{\p@enumii}{} \makeatother
%	\item $f \colon \real \to \real$,
%	\item \label{AcapBNonempty-A}
%for all $x \in \real$, if $x^2 < 10$, then $f(x) \in A$,
%	and
%	\item \label{AcapBNonempty-B}
%for all $x \in \real$, if $x^3 > 10$, then $f(x) \in B$.
%	\end{enumerate}
%Show $A \cap B \neq \emptyset$.

\end{problist}

\end{exers}



 

%\begin{exers} \label{AllElimExistsIntroExers}
%Use the symbolization key
%\begin{ekey}
%\item[\univ] The set of all U of L students.
%\item[x \mathrel{L} y] $x$ likes $y$. 
%\item[b] Bobby
%\item[c] Cindy
%\end{ekey}
%Assume 
%$$\forall x,\Bigl(  \bigl( \exists y, (x \mathrel{L} y) \bigr) \eif \forall z, (z \mathrel{L} x) \Bigr)$$
%%\\& b \in U, 
%%\\& c \in U
%and
%$$ b \mathrel{L} c .$$
%For each of the following assertions:
%	\begin{enumerate} \renewcommand{\theenumi}{\alph{enumi}} \itemindent=2\parindent
%	\item \label{AllElimExistsIntroExers-translate}
%	 translate it into {\QL}, 
%	and 
%	\item  \label{AllElimExistsIntroExers-prove}
%	provide a proof in {\QL}.
%	\end{enumerate}
%%Which of the following conclusions are justified using only $\forall$-elimination and $\exists$-introduction?
%% \emph{Explain your answers.}
%\begin{problist}
%\item \label{AllElimExistsIntroExers-BobbyLikes}
% Bobby likes some student at the U of L.
% \item \label{AllElimExistsIntroExers-BobbyLikesBobby}
% Bobby likes himself.
%\item \label{AllElimExistsIntroExers-LikesBobby}
% Some student at the U of L likes Bobby.
%\item \label{AllElimExistsIntroExers-LikesHimself}
%Some student at the U of L likes himself or herself.
%% $\exists x, (x \mathrel{L} x)$.
%%\item \label{AllElimExistsIntroExers-L(x,y)}
%% $\exists x \in U, \exists y \in U, \bigl( ( x \mathrel{L} y) \eif \exists z \in U, (z \mathrel{L} x)\bigr).$
%\item \label{AllElimExistsIntroExers-LikesCindy}
% If there is a student at the U of L whom Cindy likes, then there is a student at the U of L who likes Cindy.
%\item \label{AllElimExistsIntroExers-IfThenBobbyLikes}
% If there is a student at the U of L who likes Bobby, then there is a student at the U of L whom Bobby likes.
%%\item \label{AllElimExistsIntroExers-L(z,x)}
%% $\exists x \in U, \Bigl( \bigl(\exists y\in U, (x \mathrel{L} y) \bigr) \eif \bigl(\forall z \in U, (z \mathrel{L} x) \bigr)\Bigr).$ 
%\end{problist}
%\end{exers}





\subsection{\texorpdfstring{$\forall$}{All}-introduction}\index{all ($\forall$)!-introduction}
\label{AllIntroSect}

If Inspector Thinkright needs to verify that all of the butlers in town have seen the aurora borealis, he would probably get a list of all the butlers, and check them one-by-one. That is a valid approach, but it could be very time-consuming if the list is very long. In mathematics, such one-by-one checking is often not just time-consuming, but impossible. For example, the set~$\natural$ is infinite, so, if we wish to show $\forall n \in \natural, (\text{$2n$ is even})$, then we would never finish if we tried to go through all of the natural numbers one-by-one. So we need to deal with many numbers at once. 

Consider the following simple deduction:
\begin{earg}
\item[]Every butler in town got up before 6am today.
\item[]Everyone who got up before 6am today, saw the aurora.
\conclusion Every butler in town saw the aurora.
\end{earg}

This is clearly a valid deduction in English.  Let us translate it into {\QL} to analyze how we were able to reach a conclusion about all of the butlers, without checking each of them individually.  Here is a symbolization key:
\begin{ekey}
\item[B] The set of all of the butlers in town.
\item[P] The set of all people.
\item[U(x)] $x$ got up before 6am today.
\item[S(x)] $x$ saw the aurora.
\end{ekey}
We can now translate our English deduction, as follows:
\begin{earg}
\item[]$\forall b \in B, U(b)$. 
\item[]$\forall p \in P, \bigl( U(p) \eif S(p) \bigr)$.
\conclusion $\forall b \in B, S(b)$.
\end{earg}
How do we justify the conclusion?  Well, suppose for a moment that we start to check every butler in town, and that $j$ represents Jimmy, who is one of the butlers in town.  Then our first hypothesis allows us to conclude $U(j)$.  Since Jimmy is a person, our second hypothesis allows us to conclude that $U(j) \eif S(j)$. Then, using $\eif$-elimination, we conclude $S(j)$.  But there was nothing special about our choice of Jimmy.  All that we know about him, is that he is a butler in the town.  So we could use exactly the same argument to deduce $S(b)$ for any butler~$b$ in the town.

This is how we justify a $\forall$-introduction.  If we can prove that the desired conclusion is true for an \emph{arbitrary} element of a set, when we assume \emph{nothing} about the element except that it belongs to the set, then the conclusion must be true for every element of the set.

We write the above deduction as follows:
\begin{thm}
Assume that every butler in town got up before 6am today. Also assume that everyone who got up before 6am today, saw the aurora. Then every butler in town  saw the aurora.
\end{thm}

\begin{proof}
Let $b$ represent an arbitrary butler in town. Then, since all of the butlers got up before 6am, we know that $b$ got up before 6am. By hypothesis, this implies that $b$~saw the aurora.  Since $b$ is an arbitrary butler in town, we conclude that every butler in town saw the aurora.
\end{proof}

This reasoning leads to the $\forall$-introduction rule: in order to prove that \emph{every} element of a set~$X$ has a certain property,  it suffices to show that an \emph{arbitrary} element of~$X$ has the desired property. For example, if we wish to prove $\forall b \in B, P(b)$, then our proof should start with the sentence ``Let $b$ be an arbitrary element of~$B$\rlap.'' (However, this can be abbreviated to: ``Given $b \in B$, \ldots'') After this, our task will be to prove that $P(b)$ is true, without assuming anything about~$b$ other than it is an element of~$B$.  
 \factoidbox{The proof of an assertion that begins
 ``for all $x \in X$\rlap,''
 \\ will usually begin with ``Let $x$ be an arbitrary element of~$X$''
 \\ (or, for short, ``Given $x \in X$\rlap,'').}

\begin{warn} 
It is important not to assume anything about~$x$ other than that it is an element of~$X$. If you choose~$x$ to be a particular element of~$X$ that has some special property, then your deduction will not be valid for \emph{all} elements of the set.
\end{warn}

\begin{eg} 
Suppose we would like to justify the following deduction:
\begin{quote}
All of the butlers in town dislike Jimmy, and Jimmy is a butler in town. Therefore, all of the butlers in town dislike themselves.
\end{quote}
Then it suffices to show, for an arbitrary butler~$b$, that $b$ dislikes~$b$. We might try the following proof:
\begin{proof}[Proof attempt]
Let $b$ be Jimmy, who is a butler in town.  Then, since all of butlers in town dislike Jimmy, we know that $b$ dislikes Jimmy. Since $\text{Jimmy} = b$, this means $b$ dislikes~$b$, as desired.  So every butler in town dislikes himself.
\end{proof}
This proof is certainly \emph{not} valid, however.  Letting $b = \text{Jimmy}$ does not make~$b$ an \emph{arbitrary} butler; rather, it makes~$b$ a very special butler --- the one that everybody dislikes. In this case, conclusions that are true about~$b$ are not necessarily true about the other butlers.
\end{eg}

Another point that should be emphasized is that an \emph{arbitrary} member of a set is not the same as a \emph{random} member of a set.  If we want to prove that all of the butlers have seen the aurora, it is not enough to choose a butler at random, ask if he saw the aurora and draw a conclusion about all of the butlers based on that single answer.  It is only if we can determine through logical deduction that \emph{no matter which} butler we choose, that person saw the aurora, that we can conclude that all of the butlers saw the aurora.




\begin{exer} \label{WhichQRule?}
Which of the $4$ quantifier rules does each deduction illustrate?
\begin{enumerate}
\item \label{WhichQRule?-AE}
 Everyone who ate in the cafeteria yesterday is sick today. Oh, no! Susie ate in the cafeteria --- she must be sick!
\item \label{WhichQRule?-EI}
 Susie ate in the cafeteria yesterday, so I'm sure that \emph{somebody} ate in the cafeteria yesterday.
\item \label{WhichQRule?-AI}
 Without knowing which of the athletes it was, I figured out that he or she must have eaten in the cafeteria yesterday. The only way that can be true is if every athlete ate in the cafeteria yesterday.
\item \label{WhichQRule?-EE}
 Our food reporter says that some woman knocked over a big box of lima beans while she was eating in the cafeteria yesterday. Whoever she is, let's call her ``Ms.~Clumsy\rlap.'' So this morning's headline can be ``Ms.~Clumsy spilled the beans!''
\end{enumerate}
\end{exer}



%Here are two applications of $\forall$-introduction in graph theory. The first is a proof of \cref{edges=halfsumvalence} that does not use induction. We consider only the out-valences, but the proof for in-valences is similar.

%\begin{thm} \label{arcs=sumoutvalence}
%The number of arcs of any simple digraph is exactly the same as the sum of the out-valences of the vertices of the digraph.
%\end{thm}

%\begin{proof}
%Let $D$ be any simple digraph, with vertex set~$V$ and arc set~$A$. We may write $V = \{v_1,v_2,\ldots,v_n\}$ (with all $v_i$'s distinct). For $i = 1,2,\ldots,n$, let 
%	\begin{itemize}
%	\item $d_i$ be the out-valence of~$v_i$, and
%	\item $A_i$ be the set of all arcs that begin at~$v_i$; that is,
%	$A_i = \{\, \vec{uw} \in A \mid u = v_i \,\}$.
%	\end{itemize}
%Then $d_i = \# A_i$, for each~$i$.
%Also, $A_1,A_2,\ldots,A_n$ are pairwise disjoint (because each arc begins at only one vertex) and 
%$A = A_1 \cup A_2 \cup \cdots \cup A_n$ (because each arc begins at some vertex~$v_i$). Therefore
%	\begin{align*}
%	\#A 
%	&= \#(A_1 \cup A_2 \cup \cdots \cup A_n)
%	\\&= \#A_1 + \#A_2 + \cdots + \#A_n && \text{(Rem.~\fullref{card(DisjointUnion)Rem}{many})}
%	\\&= d_1 + d_2 + \cdots + d_n
%	, \end{align*}
%as desired.
%\end{proof}

%Let us point out that this theorem for digraphs implies the corresponding theorem for graphs:

%\begin{cor}[(\cref{edges=halfsumvalence})]
%The number of edges of any simple graph is exactly one-half  the sum of the valences of the vertices of the graph.
%\end{cor}

%\begin{proof}
%Let $G$ be an arbitrary simple graph, with vertex set~$V$ and edge set~$E$. Create a directed graph $\vec{G}$ by replacing each edge with two oppositely directed arcs. That is, the vertex set of~$\vec{G}$ is~$V$, and the arc set of~$\vec{G}$ is
%	$$ \vec{A} = \{\, \vec{uv} \mid u,v \in V, \ uv \in E \,\} .$$
%Note that each edge $uv$ of~$G$ yields exactly~$2$ arcs of~$\vec{G}$ (namely, $\vec{uv}$ and $\vec{vu}$), so 
%	$$\#\vec{A} = 2 (\#E) .$$

%At any arbitrary $v \in V$, each edge~$uv$ of~$G$ incident with~$v$ yields exactly one arc of~$\vec{G}$ that begins at~$v$ (namely, $\vec{vu}$). Therefore, the valence of~$v$ in~$G$ is exactly equal to the out-valence of~$v$ in~$\vec{G}$. Since $v$ is an arbitrary vertex of~$G$, we conclude that, for every vertex, the valence in~$G$ is exactly equal to the out-valence in~$\vec{G}$. Therefore, adding up the the valences of the vertices in~$G$ is the same as adding up the out-valences of the vertices in~$\vec{G}$. By \cref{arcs=sumoutvalence}, this sum is $\#\vec{A} = 2(\#E)$. Dividing by~$2$ yields the desired result.
%\end{proof}

%\begin{exer}[(\emph{harder})] \label{k-criticalExer}
%A graph $G$ is \emph{$k$-critical} if $k$ colours are needed to vertex-colour $G$, but every graph obtained by deleting some vertex of $G$ (and all of its incident edges) can be coloured using $k-1$ colours.

%Prove that if $G$ is a $k$-critical graph, then every vertex has at least $k-1$ neighbours.
%\\ \hint{Prove the contrapositive: suppose there is some vertex that has at most $k-2$ neighbours.  Then delete this vertex (and all of its incident edges).}
%\end{exer}

%\begin{thm}
%For every $n \in \natural$, $n+n \ge n$.
%\end{thm}
%\begin{proof}
%Let $n$ be an arbitrary natural number.  Then $n\ge 0$.  Hence, $n+n \ge n+0$, so $n+n \ge n$.  Since $n$ was arbitrary, it is true that for every $n \in \natural$, $n+n \ge n$.

%Therefore, $\forall n \in \natural, n+n \ge n$.
%\end{proof}


%\begin{exers} \label{TranslateAndProve}
%% should revise this to use sets instead of predicates
%Using the given symbolization key, translate each theorem from {\QL} into English, and provide a proof.  (Note that you do not need to know what ``coprime'' or ``perfect'' means. Also, although the deductions are valid, some of them may have a conclusion that is false, because some of the hypotheses are not true.)
%\begin{ekey}
%\item[\univ] $\natural$
%\item[E(x)] $x$ is even.
%\item[x\mathrel{C}y] $x$ is coprime to $y$.
%\item[P(x)] $x$ is perfect.
%\end{ekey}
%\begin{problist}
%\item \label{TranslateAndProve-C(x,x)}
% $\forall x, \forall y, (x\mathrel{C}y),$ \therefore $\exists x, (x\mathrel{C}x)$.
%\item \label{TranslateAndProve-C(y,x)}
% $\forall x, \forall y, \bigl((x\mathrel{C}y) \eif (y\mathrel{C}x) \bigr),$ \therefore $\forall x, \forall y, \bigl((x\mathrel{C}y) \eiff (y\mathrel{C}x) \bigr).$
%%\item \label{TranslateAndProve-E(z)}
%% $\forall z, \bigl(E(z) \eor \enot E(z) \bigr)$
%\item \label{TranslateAndProve-C(x,y)}
% $\bigl(\forall x, (x\mathrel{C}x) \bigr) \eif \bigl(\exists x, \exists y, (x\mathrel{C}y)\bigr)$
%\item \label{TranslateAndProve-E(x)}
% $\forall y, \exists x, \bigl(E(y) \eif E(x) \bigr)$
%\item \label{TranslateAndProve-P(2)}
% $P(2) \eif \forall x, \bigl(E(x) \eiff E(2)\bigr)$, $E(2)$, $\enot E(1)$, \therefore $\enot P(2)$.
%\end{problist}
%\end{exers}


%\begin{exers} \label{TranslateAndContradict}
%Using the symbolization key given, translate each hypothesis from {\QL} into English, and use the given hypotheses to deduce a contradiction.
%\begin{ekey}
%\item[\univ] $\real$
%\item[\rational] The set of all rational numbers.
%\item[\natural] The set of all natural numbers.
%\item[\integer] The set of all integers.
%\item[x < y] $x$ is less than $y$.
%\end{ekey}
%\begin{problist}
%\item \label{TranslateAndContradict-Q(x)}
% $\natural \subset \rational $, \quad $\exists n, (n \in \natural)$, \quad $\forall x, (x \notin \rational)$
%\item \label{TranslateAndContradict-L(x,y)}
% $\exists x, \enot L(x,2)$, $\forall x, (\forall y, L(y,x))$
%\item \label{TranslateAndContradict-Z(x)}
% $\forall x, \bigl( N(x) \eif Q(x) \bigr)$, $\forall x, \bigl( N(x) \eif Z(x)\bigr)$, $\forall x, N(x)$, $\exists x, (\enot Q(x) \eor \enot Z(x))$
%\end{problist}
%\end{exers}




%In the following proof, we will take the following properties of the natural numbers to be assumed, without proof:
%\begin{itemize}
%\item the sum of any two natural numbers is a natural number;
%\item the product of any two natural numbers is a natural number;
%\item multiplication distributes over addition (in particular, $\forall m \in \natural, \bigl( \forall n \in \natural, (\forall k \in \natural, (n+k)m=nm+km)\bigr)$);
%\item addition can be cancelled (that is, $\forall m \in \natural, \bigl( \forall n \in \natural, (\forall k \in \natural, m+n=m+k \eif n=k )\bigr)$).
%\end{itemize}

%\begin{thm}
%Suppose that we know that $\exists m \in \natural, (\forall n \in \natural, n+m=n)$.  Then $\exists k \in \natural, (\forall n \in \natural, kn=k)$. 
%\end{thm}
%\begin{proof}
%Let $p$ represent the element of $\natural$ for which $\forall n \in \natural, n+p=n$.  Then for any $n \in \natural$, we have $pn \in \natural$, so by hypothesis, $pn+p=pn$.  Since $p$ is a natural number, our hypothesis also allows us to conclude that $p+p=p$.  Hence, $pn+p = pn = (p+p)n = pn+pn$ (the last equality uses the distributive law that we are assuming).  This string of equalities allows us to conclude that $pn+p=pn+pn$ for every $n \in \natural$.
%Now using cancellation to cancel $pn$ from both sides of this equation, we conclude that $pn=p$ for every $n \in \natural$.  Thus, there is some $k \in \natural$ (namely, $p$), for which $\forall n \in \natural, kn=k$.

%We have shown that if $\exists m \in \natural, (\forall n \in \natural, n+m=n)$, then $\exists k \in \natural, (\forall n \in \natural, kn=k)$. 
%\end{proof}

%In fact, the natural number 0 has all of the properties that we attributed to the natural number $p$ in this proof. Here we were able to show that one property of 0 (that 0 times anything is 0) can be deduced from another property of 0 (that adding 0 to any number leaves that number unchanged), even if we did not \emph{know} that 0 has both of these properties.






\section{Some proofs about sets}
\label{SetProofsSect}

To find proofs in {\QL}, you can use all of the strategies that were helpful in {\SL}: working backwards, working forwards, changing what you are looking at, breaking the proof into cases, and proof by contradiction are all important. The introduction and elimination rules for quantifiers just add some new options when you are working forwards or working backwards. In particular:
\begin{itemize}
\item If you have $\exists x, \script{A}(x)$, you will probably use $\exists$-elimination: assume $\script{A}(c)$ for some letter~$c$ that is not already in use, and then derive a conclusion that does not contain~$c$.
\item If the desired conclusion is $\forall x \in X,\script{A}(x)$, then your proof will almost certainly be based on $\forall$-introduction, so the first words of your proof will usually be ``Given $x \in X$,\ \dots''
\item If you have $\forall x,\script{A}(x)$, and it might be helpful to know $\script{A}(c)$ (for some constant~$c$), then you could use $\forall$-elimination.
\end{itemize}
%This \lcnamecref{SetProofsSect} provides some examples.

%%Students of mathematics are expected to be able to \emph{prove} assertions about unions and intersections. 
%%\setcounter{subsection}{-1}
%%\section{Using definitions in proofs}
%Before giving some examples of this,
%we should say a few words about how definitions are used in proofs.
%\factoidbox{Any term that has been defined may be interchanged \\ with its definition at any point in a proof.}
%% We will see examples of using previous theorems to justify assertions, later in this chapter.
%
%
%\begin{eg}
%Suppose, for the sake of argument, that we agree to 
%\begin{quote}
%define a dog as an animal with a tail, that barks. 
%\end{quote}
%Then if the assertion ``Matt is a dog'' appears in a proof, we can say, ``By definition (of dog), Matt is an animal with a tail, that barks\rlap.''  The $\eand$-elimination rule then justifies any of the assertions, ``Matt is an animal\rlap,'' ``Matt has a tail\rlap,'' and ``Matt barks\rlap.''  Likewise, if the assertion ``A coyote is an animal with a tail, that barks'' appears in a proof, we are justified in asserting, ``By definition (of dog), a coyote is a dog\rlap.''  While you might quarrel with this assertion, the fault lies in the definition that we have chosen, not in our logic.
%It is not acceptable to use any ``facts'' that you may believe you know about dogs, unless they are included in the definition, or can be deduced from given definitions and hypotheses.  In this example, we cannot assert ``By definition (of dog), Matt has a long tongue\rlap,'' because that was not part of our definition.
%\end{eg}
%
%That example was rather silly, but here is an example that is more realistic:
%
%\begin{eg} 
%%\ 
%%\begin{enumerate}
%%\item
% The notation $A \subset B$ has been defined to mean $\forall a \in A, ( a \in B )$. Therefore, if we know, say, that $X \subset Y$, then we can conclude $\forall x \in X, ( x \in Y )$. Conversely, if we know $\forall h \in H, (h \in M)$, then we can conclude that $H \subset M$.
%%\item Suppose that $A$, $B$ and $f$ are sets, and each element of $f$ is an ordered pair, $(a,b)$ such that  $a \in A$ and $b\in B$.  If we can prove that for every $a\in A$, there is a unique $b \in B$ such that $(a,b) \in f$, then we may conclude that, \emph{by definition}, $f$ is a function. 
%%\end{enumerate}
%\end{eg}


For example, now that we have all the rules of First-Order Logic, we can prove the following important fact that was stated on \cpageref{Mention2SetsEqual}.

\begin{eg} \label{EqualIffSubsets}
Assume $A$ and~$B$ are sets. 
We have $A = B$ if and only if $A \subset B$ and $B \subset A$.
\end{eg}

\begin{proof}
($\Rightarrow$) Assume $A = B$. 
Every set is a subset of itself (see \cref{SubsetFacts}), so we have 
$$ \text{$A = B \subset B$ \quad and \quad $B = A \subset A$,}$$
as desired.
%
%Therefore, if $A=B$ then $A \subset B$ and $B \subset A$.

($\Leftarrow$) Assume $A \subset B$ and $B \subset A$. We wish to show $A = B$; in other words, we wish to show 
	$$ \forall x,  (x \in A \eiff x \in B) .$$

Let~$x$ be arbitrary.

%\begin{itemize} \setlength{\leftskip}{\parindent}
\qquad($\Rightarrow$) Suppose $x \in A$. Since $A \subset B$, this implies $x \in B$.

\qquad($\Leftarrow$) Suppose $x \in B$. Since $B \subset A$, this implies $x \in A$.

\noindent Therefore, $x \in A \eiff x \in B$. 
Since $x$~is arbitrary, this implies $\forall x, (x \in A \eiff x \in B)$, as desired.
%We have shown that $A=B$ if and only if $A \subset B$ and $B \subset A$.
%\qed
%\end{itemize}
%\renewcommand{\qed}{}
\end{proof}


\begin{eg} \label{IntersectIsSubsetEg}
Suppose $A$, $B$, and~$C$ are sets (and $\univ$ is the universal set, as usual). Then:
\begin{tasks}(2)
\task\fixtask \label{IntersectIsSubsetEg-intersect}%
 $A \cap B \subset A$.
\task\fixtask \label{IntersectIsSubsetEg-union}%
 $A \subset A \cup B$.
\task\fixtask \label{IntersectIsSubsetEg-intersectU}%
$A \cap \univ = A$.
\task\fixtask \label{IntersectIsSubsetEg-transitive}%
If $A \subset B$ and $B \subset C$, then $A \subset C$.
\task\fixtask \label{IntersectIsSubsetEg-CapInCup}%
 $A \cap B \subset A \cup B$.
\task\fixtask \label{IntersectIsSubsetEg-InBothImplies}%
If $A \subset B$ and $A \subset C$, then $A \subset B \cap C$.
\end{tasks}
\end{eg}

\begin{proof}
\pref{IntersectIsSubsetEg-intersect} We wish to show that every element of $A \cap B$ is an element of~$A$. Given $x \in A \cap B$, we know, from the definition of $A \cap B$, that $x \in A$ and $x \in B$. In particular, $x \in A$, as desired.

\pref{IntersectIsSubsetEg-union} We wish to show that every element of $A$ is an element of $A \cup B$. 
Given $x \in A$, it is obviously true that either $x \in A$ or $x \in B$ (since, in fact, we know $x \in A$).  Therefore $x \in A \cup B$, as desired.

\pref{IntersectIsSubsetEg-intersectU} From \pref{IntersectIsSubsetEg-intersect}, we know that $A \cap \univ \subset A$, so it suffices to show that $A \subset A \cap \univ$. Given $a \in A$, we obviously have $a \in A$. Furthermore, since the universal set~$\univ$ contains every element that is under consideration, we also have $a \in \univ$. Hence $a \in A \cap \univ$, as desired.

\pref{IntersectIsSubsetEg-transitive}
 Let $a$ be an arbitrary element of~$A$. Since $A \subset B$, we know $a \in B$. Then, because $B \subset C$, we know $a \in C$. Since $a$ is an arbitrary element of~$A$, this implies $A \subset C$.

\pref{IntersectIsSubsetEg-CapInCup}
Given $x \in A \cap B$, we know $x \in A$ and $x \in B$. In particular, we have $x \in A$, so it is certainly true that either $x \in A$ or $x \in B$. Therefore $x \in A \cup B$. 
Since $x$ is an arbitrary element of $A \cap B$, this implies $A \cap B \subset A \cup B$, as desired.

\emph{Alternate proof of \pref{IntersectIsSubsetEg-CapInCup}.}
From parts \pref{IntersectIsSubsetEg-intersect} and~\pref{IntersectIsSubsetEg-union}, we know $A \cap B \subset A$ and $A \subset A \cup B$. So \pref{IntersectIsSubsetEg-transitive} 
%(with $A \cap B$ in the role of~$A$, $A$~in the role of~$B$, and $A \cup B$ in the role of~$C$) 
implies that $A \cap B \subset A \cup B$, as desired.

\pref{IntersectIsSubsetEg-InBothImplies}
Let $a$ be an arbitrary element of~$A$. Since $A \subset B$, we have $a \in B$. Similarly, since $A \subset C$, we also have $a \in C$. Having established that $a \in B$ and $a \in C$, we conclude that $a \in B \cap C$. 
Since $a$ is an arbitrary element of~$A$, this implies $A \subset B \cap C$.
\end{proof}



\begin{exers} \label{SetOpPfEx}
Assume $A$, $B$, and~$C$ are sets.
\begin{enumerate}
%\item Show $A \cap A = A$.
%\item Show $A \cup A = A$.
%\item Show $A \cap \emptyset = \emptyset$.
%\item Show $A \cup \emptyset = A$.
%\item Show $A \cap \univ = A$.
%\item Show $A \cup \univ = \univ$.
%\item Show $A \cap B = B \cap A$.
%\item Show $A \cup B = B \cup A$.
\item  \label{SetOpPfEx-ACapB=A}
Show that if $A \subset B$, then $A \cap B = A$.
\item  \label{SetOpPfEx-ACupB=B}
Show if $A \subset B$, then $A \cup B = B$.
%\item Show that $A \cap B = A \cup B$ if and only if $A = B$.
\item \label{SetOpPfEx-ABinAC}
Show that if $B \subset C$, then $A \cap B \subset A \cap C$.
%\item Show that if $C \subset A$ and $C \subset B$, then $C \subset A \cap B$.
\item \label{SetOpPfEx-AUBinC}
 Show that if $A \subset C$ and $B \subset C$, then $A \cup B \subset C$.
%\item Show that if $B \subset C$, then $A \cup B \subset A \cup C$.
%\item Show $A \cap (B \cap C) = (A \cap B) \cap C$.
%\item Show $A \cup (B \cup C) = (A \cup B) \cup C$.
%\item Show $A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$.
\item  \label{SetOpPfEx-A(BUC)=(AB)(AC)}
Show $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$.
\item  \label{SetOpPfEx-AsmB=}
 Show $A \sm B = A \sm (A \cap B)$.
 \item \label{SetOpPfEx-AcupB=}
 Let $X = A \cap B$, and show $A \cup B = (A \sm X) \cup (B \sm X) \cup X$.
%\item Show $\power(A) \cup \power(B) \subset \power(A \cup B)$.
\item  \label{SetOpPfEx-Power=Cup}
Show that if $\power(A \cup B) = \power(A) \cup \power(B)$, then either 
$A \subset B$ or $B \subset A$.
\hint{Prove the contrapositive. Choose $a \in A$ and $b \in B$, such that $a \notin B$ and $b \notin A$. Then $\{a,b\} \notin \power(A) \cup \power(B)$.}
\end{enumerate}
\end{exers}


\begin{exers} \label{DeMorganSetEx}
Suppose $A$ and~$B$ are sets.
\begin{enumerate}
%\item Show $A \sm B$ is a subset of~$A$.
%\item Show that $A \subset \comp{B}$ if and only if $B \subset \comp{A}$
%\item Show $\comp{\emptyset} = \univ$.
%\item Show $\comp{\univ} = \emptyset$.
%\item Show $\comp{A} = \univ \sm A$.

\item \label{DeMorganSetEx-AsmB}
Show $A \sm B = A \cap \comp{B}$.

\item \label{DeMorganSetEx-partition}
 Show $A = (A \sm B) \cup (A \cap B)$.
 
%\item Show that if $A \subset B$, then $\comp{B} \subset \comp{A}$.

\item \label{DeMorganSetEx-DM}
Prove De\,Morgan's Laws:
\noprelistbreak
\begin{multicols}{3}
\begin{enumerate} 
\item \label{DeMorganSetEx-DM-comp}
$\comp{\comp{A}} = A$. 
%\\ ({\em The complement of the complement is the original set.\/})
\item \label{DeMorganSetEx-DM-cap}
$\comp{A \cap B} = \comp{A} \cup \comp{B}$.
\item \label{DeMorganSetEx-DM-cup}
$\comp{A \cup B} = \comp{A} \cap \comp{B}$.
\end{enumerate}
\end{multicols}

\item \label{DeMorganSetEx-A=B}
Show that if $\comp{A} = \comp{B}$, then $A = B$.
\\\hint{Follows immediately from one of De\,Morgan's Laws.}
%\item Show $A \subset B$ if and only if $A \sm B = \emptyset$.
%\item Show that if $A \sm B = B \sm A$, then $A = B$.
%\item Show $A \cup B = (A \sm B) \cup (B \sm A) \cup (A \cap B)$.
\end{enumerate}
\end{exers}

\begin{exers} \label{DisjointEx}
Suppose $A$, $B$, and~$C$ are sets.
\begin{enumerate}
\item \label{DisjointEx-InComplement}
 Show that $A$ is disjoint from~$B$ if and only if $A \subset \comp{B}$.
\item \label{DisjointEx-smIsDisjoint}
Show $A \sm B$ is disjoint from~$B$.
\item \label{DisjointEx-SubsetDisjoint}
Show that if $A$ is disjoint from~$B$, and $C$ is a subset of~$B$, then $A$ is disjoint from~$C$.
\item  \label{DisjointEx-AsmBvsAcapB}
Show that $A \sm B$ is disjoint from $A \cap B$.
\item \label{DisjointEx-Both}
Show that $A$ is disjoint from $B \cup C$ iff $A$ is disjoint from both~$B$ and~$C$.
%\item Show $A \cap \comp{A} = \emptyset$.
%({\it Every set is disjoint from its complement.\/})
%\item Show that $A \sm B$, $B \sm A$, and $A \cap B$ are \define{pairwise disjoint}.
%That is, any two of these three sets are disjoint from each other.
%\item (harder) Suppose 
%\begin{itemize}
%\item $A_i$ and~$B_i$ are disjoint finite sets, for $i = 1,2$,
%\item $\#A_1 = \#A_2$,
%and
%\item $\#B_1 = \#B_2$.
%\end{itemize}
%Show $\#(A_1 \cup B_1) = \#(A_2 \cup B_2)$.
%\item \label{DisjointEx-card} 
%(harder) Show that if $A$ and~$B$ are disjoint and finite, then $\#(A \cup B) = \#A + \#B$.
%\\ \hint{If $f \colon \{1,2,\ldots,m\} \to A $ and $g \colon \{1,2,\ldots,n\} \to B$ are bijections, define $h \colon \{1,2,\ldots,m+n\} \to A \cup B$ by 
%$$h(i) = \begin{cases} 
%f(i) & \text{if $i \le m$} \\
%g(i-m) & \text{if $i > m$}
%. \end{cases}$$
%Show $h$ is a bijection.}
\end{enumerate}
\end{exers}

\begin{exers} \label{Venn3parts} \ 
	\begin{problist}
	\item \label{Venn3parts-union}
Show $A \cup B = (A \sm B) \cup (B \sm A) \cup (A \cap B)$.
	\item \label{Venn3parts-disjoint}
Show the three sets $A \sm B$, $B \sm A$, and $A \cap B$ are all disjoint from each other.
	\end{problist}
\end{exers}

Recall from \fullcref{card(DisjointUnion)Rem}{many} that sets $A_1,A_2,\ldots,A_n$ are \define[disjoint sets!pairwise-]{pairwise-disjoint} iff $A_i$ is disjoint from~$A_j$ whenever $i \neq j$.

\begin{exer} \label{PairDisjUnionEx}
Suppose the sets $A_1,A_2,\ldots,A_n$ are pairwise-disjoint. Show:
\begin{enumerate}
\item The sets $A_1,A_2,\ldots,A_{n-1}$ are pairwise-disjoint, if $n > 1$.
\item $A_n$ is disjoint from $A_1 \cup A_2 \cup \cdots \cup A_{n-1}$, if $n > 1$.
\end{enumerate}
\end{exer}






\goodbreak % !!!
\section{Counterexamples (reprise)} \label{FOCounterexamplesSect}

We have been discussing proofs in this \lcnamecref{ch.firstorder}, but you should keep in mind that counterexamples are also an important part of logic:
%The principle discussed in \cref{CounterexampleSect} also applies to {\QL}:
\factoidbox{To show that a deduction is valid, 
provide a proof. \\[5pt]
To show that a deduction is \emph{not} valid, provide a counterexample.}

\begin{eg}
Show that the following deduction is not valid:
 $$ \exists x, (x \in A), \qquad \therefore \ \forall x, (x \in A) .$$
%\begin{earg}
%\item[] $\exists x, (x \in A)$
%\conclusion $\forall x, (x \in A)$
%\end{earg}
\end{eg}

\begin{scratchwork}
To get the idea of what is going on, it may be helpful to translate the deduction into English. For example, we could use the symbolization key
	\begin{ekey}
	\item[\univ] things on the kitchen table
	\item[A] apples on the kitchen table
	\end{ekey}
In this setting, the deduction becomes:
	$$\text{There is an apple on the kitchen table. \quad \therefore\ Everything on the kitchen table is an apple.} $$
This deduction is obviously not valid: it is easy to imagine a situation in which one thing on the kitchen table is an apple, but something else on the kitchen table is not an apple.

To find the official solution, we will do something analogous, but using the notation of {\QL}, instead of talking about apples and tabletops.
In order to construct a counterexample, we want the hypothesis of the deduction to be true and the conclusion to be false. 
	\begin{itemize}
	\item To make the hypothesis $\exists x, (x \in A)$ true, we need something to be an element of~$A$. For example, we could let $1 \in A$.
	\item To make the the conclusion $\forall x, (x \in A)$ false, we want its negation to be true: we want $\exists x, (x \notin A)$ to be true. For example, we could arrange that $2 \notin A$.
	\end{itemize}
To satisfy the above two conditions, we let $A = \{1\}$. Since $1$ and~$2$ are the only elements mentioned in the discussion, we can let $\univ = \{1,2\}$. This results in the counterexample we were hoping to find.
\end{scratchwork}

\begin{solution}
We provide a counterexample. Let
	$$ \text{$\univ = \{1,2\}$ and $A = \{1\}$.} $$
%\begin{ekey}
%\item[\univ] $\{1,2\}$
%\item[A] $\{1\}$
%\end{ekey}
Then:
\begin{itemize}
\item[] $1 \in A$ is true, so $\exists x, (x \in A)$ is true,
so the hypothesis is true, 
\end{itemize}
but
\begin{itemize}
\item[] $2 \notin A$, so $\forall x, (x \in A)$ is false, so the conclusion is false.
\end{itemize}
Since we have a situation in which the hypothesis is true, but the conclusion is false, the deduction is not valid.
%A symbolization key that satisfies all the hypotheses of a deduction is called a \define{model} for the deduction. 
\end{solution}


\begin{eg}
Show that the following deduction is not valid:
	\begin{earg} \label{(xinA)and(xinB)Countereg}
	\item \label{(xinA)and(xinB)Countereg-forall}
	$\forall x, \bigl( (x \in A) \eor (x \in B) \bigr)$
	\item \label{(xinA)and(xinB)Countereg-Anot0}
 $A \neq \emptyset$
	\item \label{(xinA)and(xinB)Countereg-Bnot0}
 $B \neq \emptyset$
	\conclusion $\exists x, \bigl( (x \in A) \eand (x \in B) \bigr)$.
	\end{earg}
\end{eg}

\begin{scratchwork}
In order to construct a counterexample, we want all of the hypotheses of the deduction to be true and the \emph{negation} of the conclusion to be true. The negation of the conclusion is
	$$ \forall x, \bigl( (x \notin A) \eor (x \notin B) \bigr) ,$$
which is logically equivalent to
	\begin{align} \label{(xinA)and(xinB)Countereg-InA->NotinB}
	\forall x, \bigl( (x \in A) \eif (x \notin B) \bigr)
	. \end{align}
Now:
	\begin{itemize}
	\item To make \cref{(xinA)and(xinB)Countereg-Anot0} true, we may let $1 \in A$.
	\item To make \cref{(xinA)and(xinB)Countereg-Bnot0} true, we must put something in the set~$B$. However, it is important to note that \pref{(xinA)and(xinB)Countereg-InA->NotinB} tells us $1 \notin B$, so we must put something else into~$B$. For example, we may let $2 \in B$.
	\item Now, after $A$ and~$B$ have been constructed, we can make \cref{(xinA)and(xinB)Countereg-forall} true by letting $\univ = A \cup B$.
	\end{itemize}
To satisfy all three of these conditions, we may let $A = \{1\}$, $B = \{2\}$, and $\univ = A \cup B = \{1,2\}$.
\end{scratchwork}

\begin{solution}
We provide a counterexample. Let
	$$ \text{$\univ = \{1,2\}$, \quad $A = \{1\}$, \quad and \quad $B = \{2\}$.} $$
%\begin{ekey}
%\item[\univ] $\{1,2\}$
%\item[A] $\{1\}$
%\end{ekey}
Then:
\begin{enumerate}
\item We have
\begin{itemize}
\item $1 \in A$ is true, so $(1 \in A) \eor (1 \in B)$ is true,
and
\item $2 \in B$ is true, so $(2 \in A) \eor (2 \in B)$ is true.
\end{itemize}
Since $1$ and~$2$ are the only elements of~$\univ$, this implies, for every~$x$, that $(x \in A) \eor (x \in B)$ is true. So \cref{(xinA)and(xinB)Countereg-forall} is true.
\item $1 \in A$, so $A \neq \emptyset$. Hence, \cref{(xinA)and(xinB)Countereg-Anot0} is true.
\item $2 \in B$, so $B \neq \emptyset$. Hence, \cref{(xinA)and(xinB)Countereg-Bnot0} is true.
\end{enumerate}
However:
	\begin{itemize}
	\item $1 \notin B$, so $(1 \in A) \eand (1 \in B)$ is false, and
	\item $2 \notin A$, so $(2 \in A) \eand (2 \in B)$ is false.
	\end{itemize}
Since $1$ and~$2$ are the only elements of~$\univ$, this implies there is no~$x$ for which the assertion $(x \in A) \eand (x \in B)$ is true. Hence, the assertion $\exists x, \bigl( (x \in A) \eand (x \in B) \bigr)$ is false; in other words, the conclusion of the deduction is false.
Since we have a situation in which the hypothesis is true, but the conclusion is false, the deduction is not valid.
\end{solution}

\begin{eg} % from Fall 2011 Midterm Exam
Explain how you know the following deduction is \textbf{not} valid:
	$$ X \cap Y  \subset  D, \quad  \therefore   X  \subset Y \cup D.$$
\end{eg}

\begin{proof}[Solution]
We provide a counterexample.
Let $X = \{1\}$, $Y = \{2\}$, and $D = \{3\}$. 

Then $X \cap Y = \{1\} \cap \{2\} = \emptyset$, so $X \cap Y \subset D$, because the empty set is a subset of every set. This means the hypothesis is true.

However, $Y \cup D = \{2\} \cup \{3\} = \{2,3\}$. Therefore 
	$$ \text{$1 \in \{1\} = X$ and $1 \notin \{2,3\} = Y \cup D$, so $X \not\subset Y \cup D$.} $$
This means the conclusion is false.

Since we have a situation in which the hypothesis is true, but the conclusion is false, the deduction is not valid.
\end{proof}

\begin{exers} \label{FOCounteregEx}
Explain how you know that each of the following deductions is not valid.
\begin{problist}
\item \label{FOCounteregEx-inAandB}
$\exists x, (x \in A)$, \ $\exists x, (x \in B)$, \ \therefore\ $\exists x, \bigl( (x \in A) \eand (x \in B) \bigr)$
\item \label{FOCounteregEx-aneqb}
$\forall a \in A, \exists b \in B, (a \neq b)$, \ $A \neq \emptyset$, \ \therefore \ $\forall b \in B, \exists a \in A, (a \neq b)$.
\item \label{FOCounteregEx-UnionNotA}
$A \neq B$, \ \therefore \ $A \cup B \neq A$.
\item \label{FOCounteregEx-AneqB}
$\forall x \in A, (x \notin B)$, \ $\forall x \in B, (x \notin A)$, \ \therefore \ $A \neq B$.
\end{problist}
\end{exers}

\begin{exers} \label{FOPfNotValidEx}
Explain how you know that each of these deductions is \emph{not} valid.
\begin{problist}

\item \label{FOPfNotValidEx-AcupBinEcupF}
% from Fall 2010 Midterm Exam 
$A \cup B \  \subset \ E \cup F$, \quad  $\therefore \  A \cap B \ \subset \ E \cap F$.

\item \label{FOPfNotValidEx-AinBandXinY}
% from Fall 2010 Final Exam 
$ A \subset B$, \ $X \subset Y$, \qquad  $\therefore \  A \smallsetminus X \  \subset \ B \smallsetminus Y$.

\item \label{FOPfNotValidEx-AcapBnonempty}
% from Fall 2010 Makeup Final Exam
$ A \cap B \neq \emptyset$, \ $B \subset C$, \qquad $\therefore A \subset C$.

\item  \label{FOPfNotValidEx-Ex(xinP&xnotinQ)}
$\exists x, \bigl( (x \in P) \eand (x \notin Q) \bigr)$, \quad \therefore\ $\forall x, \bigl( (x \in P) \eif (x \notin Q) \bigr)$.

\item \label{FOPfNotValidEx-Ax(xRx)}
$\forall x \in X, \bigl( x \mathrel{R} x \bigr)$, \quad \therefore\ 
$\forall x_1 \in X, \forall x_2 \in X, \bigl( (x_1 \mathrel{R} x_2) \eif (x_2 \mathrel{R} x_1) \bigr)$

\end{problist}
\end{exers}

\begin{exers} \label{pr.validornot}
Determine whether each of the following deductions is valid, and justify your answer by giving a proof or a counterexample.
\begin{problist}
\item  \label{pr.validornot-Eu}
$\exists u \in U, (u \notin V)$, \ \therefore \ $\forall u \in U, (u \notin V)$.
\item  \label{pr.validornot-Ax}
$\forall x, \bigl( (x \in S) \eif (1 \in T) \bigr)$, \quad  $S \neq \emptyset$, \quad  \therefore\ $1 \in T$.
\item  \label{pr.validornot-AainA(ainB)}
$\forall a \in A, (a \in B)$, \quad $\forall b \in B, (b \in C)$,
 \quad \therefore\ $\forall a \in A,( a \in C)$.
\item  \label{pr.validornot-DcupE}
$D \cup E \neq \emptyset$, \quad $D \subset F$,
 \quad \therefore\ $D \cap F \neq \emptyset$.
\item  \label{pr.validornot-a1}
$\forall a_1 \in A, \forall a_2\in A, \bigl( (a_1 \mathrel{R} a_2) \eor (a_2 \mathrel{R} a_1) \bigr)$, \quad $2 \in A$,  \quad \therefore\ $2 \mathrel{R} 2$.
%\item $\bigl( \forall x\in X, P(x) \bigr) \eif \forall x \in X, Q(x)$, \quad $\exists x\in X, \enot P(x)$, \quad \therefore\ $\exists x \in X, \enot Q(x)$
%\item  \label{pr.validornot-Mnotempty}
%$(M \neq \emptyset) \eif (N \neq \emptyset)$, \quad $N = \emptyset$, \quad \therefore\ $\forall x , (x \notin M)$.
%\item  \label{pr.validornot-AxEy(xRy)}
%$\forall x \in X, \exists y\in Y, (x \mathrel{R} y)$, \quad \therefore\ $\exists y\in Y, \forall x\in X, (x \mathrel{R} y)$
%\item  \label{pr.validornot-EyAx(xRy)}
%$\exists y,\forall x, (x \mathrel{R} y)$, \quad \therefore\ $\forall x, \exists y, (x \mathrel{R} y)$
%\item $\exists x,\exists y, \bigl( (x \mathrel{R} y) \eor (y \mathrel{R} x) \bigr)$, \quad \therefore\ $(j \mathrel{R} j)$
\end{problist}
\end{exers}









%

%\begingroup \smaller

%\section{Quantifiers and two-column proofs (optional)}\label{sec.2-col-quant}

%Although we have moved away from the two-column proof format, you might be interested to (or find it helpful) to see how to use them with quantifiers. This section provide the two-column proof version of each of the rules that were introduced earlier in the chapter.  The reasoning that leads to these rules has already been provided, so this is little more than a list of the rules.

%We will use the following symbolization key throughout this section:
%\begin{ekey}
%\item[\univ] All people.
%\item[X] The set of all xylophone players.
%\item[\script{A}(x)] $x$ is acrobatic.
%\item[\script{B}] Bobby makes ice.
%\item[D(x)] $x$ has a dog.
%\item[c] Charlie.
%\end{ekey}

%\subsection{\texorpdfstring{$\forall$}{All}-elimination}

%Here is the general form of the $\forall$-elimination rule:

%\threecolpf{
%	\pfline{m}{\forall x, \script{A}(x)}{$\langle$\emph{whatever reason}$\rangle$}{Everyone is acrobatic.}
%	\pfline{}{\script{A}(c)}{\AllElim{m}}{Therefore Charlie is acrobatic.}
%}

%It also has a version for quantifying over a set:

%\threecolpf{
%	\pfline{m}{\forall{x} \in{X}, \script{A}({x})}{$\langle$\emph{whatever reason}$\rangle$}{All xylophone players are acrobatic.}
%	\pfline{n}{{c} \in{X}}{$\langle$\emph{whatever reason}$\rangle$}{Charlie is a xylophone player.}
%	\pfline{}{\script{A}({c})}{\AllElimSet{m}{n}}{Therefore Charlie is acrobatic.}
%}

%
%\subsection{\texorpdfstring{$\exists$}{Exists}-introduction}

%Here is the general form of the $\exists$-introduction rule:

%\threecolpf{
%	\pfline{m}{\script{A}(c)}{$\langle$\emph{whatever reason}$\rangle$}{Charlie is acrobatic.}
%	\pfline{}{\exists{x},\script{A}(x)}{\ExistIntro{m}}{Therefore, someone is acrobatic.}
%}

%
% 

%It also has a version for quantifying over a set:

%\threecolpf{
%	\pfline{m}{\script{A}(c)}{$\langle$\emph{whatever reason}$\rangle$}{Charlie is acrobatic.}
%	\pfline{n}{c \in X}{$\langle$\emph{whatever reason}$\rangle$}{Charlie is a xylophone player.}
%	\pfline{}{\exists{x \in X},\script{A}(x)}{\ExistIntroSet{m}{n}}{Therefore, some xylophone player is acrobatic.}
%}

%
%\subsection{\texorpdfstring{$\forall$}{All}-introduction}

%
%This is the schematic form of the $\forall$-introduction rule:

%\threecolpf{
%	\pfline{m}{\script{A}(a)}{$\langle$\emph{whatever reason}$\rangle$\\[3pt]
%	\textbf{Important:} \\ \it$a$ must not occur in any \\ \it undischarged assumptions.}
%	{$a$ is acrobatic \newline \vskip-11pt (\emph{we must have assumed nothing about $a$} \newline\emph{except that $a$ is a person})}
%	\pfline{}{\forall{x}, \script{A}(x)}{\AllIntro{m}}{Therefore, everyone is acrobatic.}
%}

%Note that we can do this for any constant that does not occur in an undischarged assumption and for any variable.

%Note also that the constant may not occur in any \emph{undischarged} assumption, but it may occur as the assumption of a subproof that we have already closed. For example, we can prove $\forall z, \bigl( D(z) \eif D(z) \bigr)$ without any hypotheses.

%\threecolpf{
%\hypend
%	\subproof{
%		\pfline{1}{D(f)}{assumption (want $D(f)$)}{Assume $f$ has a dog.}
%		\hypend
%		\pfline{2}{D(f)}{\Repeat{1}}{As previously mentioned, $f$ has a dog.}
%	}
%	\pfline{3}{D(f) \eif D(f)}{\IfIntro{1}{2}}{If $f$ has a dog, then $f$ has a dog.}
%	\pfline{4}{\forall z, \bigl(D(z) \eif D(z) \bigr)}{\AllIntro{3}}{Everyone who has a dog, has a dog.}
%}

%

%
% 

%
%Here is the version for quantifying over sets:

%\threecolpf{
%\subproof{
%	\pfline{m}{a \in X}{assumption}{Assume $a$ is a xylophone player.}
%	\hypend
%	\pfline{n}{\script{A}(a)}{$\langle$\emph{whatever reason}$\rangle$\\
%		\textbf{Important:} \\ \it$a$ must not occur in any \\ \it undischarged assumptions\\ \it other than ``$a \in X$\rlap.''}{$a$ is athletic. \newline \vskip-11pt (\emph{we must have assumed nothing about $a$except that $a$ is a xylophone player})}
%}
%\pfline{}{\forall{x \in X}, \script{A}(x)}{\AllIntroSet{m}{n}}{All xylophone players are athletic.}
%}

%
%\subsection{\texorpdfstring{$\exists$}{Exists}-elimination}

%This is the schematic form of the $\exists$-elimination rule: 

%\threecolpf{
%	\pfline{m}{\exists{x}, \script{A}(x)}{$\langle$\emph{whatever reason}$\rangle$}{Someone is athletic.}
%	\subproof{	
%		\pfline{n}{\script{A}(a)}{assumption}{Let $a$ represent an athletic person.}
%		\hypend
%		\pfline{o}{\script{B}}{$\langle$\emph{whatever reason}$\rangle$}{Bobby makes ice.}
%	}
%	\pfline{}{\script{B}}{\ExistElim{m}{n}{o}}{Bobby makes ice.}
%}
%\factoidbox{The constant $a$ must not appear in $\exists{x}, \script{A}(x)$, in \script{B}, \\ or in any undischarged assumption other than $\script{A}(a)$.}

%
%Here is the version for quantifying over sets:

%\threecolpf{
%	\pfline{m}{\exists{x \in X}, \script{A}(x)}{$\langle$\emph{whatever reason}$\rangle$}{There is an athletic xylophone player.}
%	\subproof{	
%		\pfline{n}{\script{A}(a)}{assumption}{Let $a$ represent an athletic person.}
%		\pfline{o}{a \in X}{assumption}{Assume also that $a$ is a xylophone player.}
%		\hypend
%		\pfline{p}{\script{B}}{$\langle$\emph{whatever reason}$\rangle$}{Bobby makes ice.}
%	}
%	\pfline{}{\script{B}}{\ExistElimSet{m}{n}{p}}{Bobby makes ice.}
%}
%\factoidbox{The constant $a$ must not appear in $\exists{x}, \script{A}(x)$, in \script{B}, \\ or in any undischarged assumption other than $\script{A}(a)$ and $a \in X$.}

%
%\subsection{Other rules}

%Just as for {\SL}, we allow any of the rules for simplifying negations to be used in a two-column proof, with ``rules of negation'' as the justification.

%Also, there are some additional rules involving equality that we have not formally introduced, but if you choose to continue to use two-column proofs, you may need them.

%The $=$-introduction rule is as follows:
%\threecolpf{
%	\pfline{}{c = c}{\EqualIntro}{$c$ is equal to itself.}
%}

%
%Notice that the \EqualIntro\ rule does not require referring to any prior lines of the proof. For any constant~${c}$, you can write ${c}={c}$ at any time, with only the \EqualIntro\  rule as justification.

%The $=$-elimination rule amounts to the fact that if $a=b$, then anything true about $a$ must also be true about $b$.  It has two versions:
%\threecolpf{
%	\pfline{m}{{a}={b}}{$\langle$\emph{whatever reason}$\rangle$}{$a$ is equal to $b$.}
%	\pfline{n}{\script{A}({a})}{$\langle$\emph{whatever reason}$\rangle$}{$a$ is athletic.}
%	\pfline{}{\script{A}({b})}{\EqualElim{m}{n}}{$b$ is athletic.}
%}

%\threecolpf{
%	\pfline{m}{{a}={b}}{$\langle$\emph{whatever reason}$\rangle$}{$a$ is equal to $b$.}
%	\pfline{n}{\script{A}({b})}{$\langle$\emph{whatever reason}$\rangle$}{$b$ is athletic.}
%	\pfline{}{\script{A}({a})}{\EqualElim{m}{n}}{$a$ is athletic.}
%}

%
%\begin{exers}[\normalfont ({optional})]
%Repeat the proofs from earlier sections of this chapter, using the two-column proof format.
%\end{exers}

%\endgroup % \smaller




\begin{summary}
\item {\QL} includes all of {\SL}, plus the quantifiers $\forall$ and $\exists$.
\item Translating between English and {\QL}.
\item The equals sign ($=$) is automatically included in every symbolization key.
\item The order of the quantifiers is important, because it can change the meaning of an assertion.
\item Uniqueness ($\exists!$)
\item Every variable in an assertion must be bound by a quantifier.
\item Rules for negating quantifiers:
\begin{itemize}
\item the negation of a ``$\forall$'' assertion is a ``$\exists$'' assertion;
\item the negation of a ``$\exists$'' assertion is a ``$\forall$'' assertion;
%\item the negation of a ``$\eand$'' assertion is a ``$\eor$'' assertion;
%\item the negation of a ``$\eor$'' assertion is a ``$\eand$'' assertion;
%\item a double negation is a positive assertion;
%\item there are also special rules for negating $\eif$ and $\eiff$.
\end{itemize}
\item Any assertion about all elements of $\emptyset$ is ``vacuously'' true.
\item Introduction and elimination rules for quantifiers.
\item Just as in {\SL}:
	\begin{itemize}
	\item To show that a deduction is valid, provide a proof.
	\item To show that a deduction is \emph{not} valid, provide a counterexample.
	\end{itemize}
\item Notation: 
\begin{itemize}
\item $\forall x$ (universal quantifier; means ``For all $x$'')
\item $\forall x \in X$ (universal quantifier; means ``For all $x$ in~$X$'')
\item $\exists x$ (existential quantifier; means ``There exists some $x$, such that\ldots'')
\item $\exists x \in X$ (existential quantifier; means ``There exists some $x$ in~$X$, such that\ldots'')
\item $\exists!\, x$ (means ``There is a unique $x$, such that\ldots'')
\item $\exists!\, x \in X$ (means ``There is a unique $x$ in~$X$, such that\ldots'')
%\item $\neq$, $\notin$, $\nexists$
\end{itemize}
\end{summary}


