
\section{Predicates}

\subsection{What are predicates?}

Predicates are similar to propositions but they depend on variables\.
$P(x,y,z)$ denotes a predicate on variables $x,y,z$\. 
Examples: 
\begin{itemize}
\item $P(x)$: $x$ is a prime number.
\item $Q(x)$: $x > 2$.
\item $R(x)$: $x$ is an odd number.
\end{itemize}
These predicates are {\em not} propositions, because they can be true
or false depending on the value of the variable $x$\.
When the value of $x$ is not specified, we say $x$ is \emph{unbound}\.  
Predicates are like functions from the domains of the variables to 
propositions.
\begin{itemize} 
\item $P(2)$ is true.
\item $R(2)$ is false.
\item $P(4) \vee R(3)$ is true.
\item $Q(3) \wedge R(4)$ is false.
\item $Q(1) \implies R(2)$ is true.
\end{itemize}

\subsection{Quantifiers}

Many propositions assert that something is true for all or some elements
of a given domain (e.g., all natural numbers)\.  
The following quantifiers presume a particular {\bf universe of
discourse} has been agreed upon in advance\.  
This is the set of elements which can be assigned to the quantified variables.
\begin{description}
\item[``$\forall$''] means ``for all.'' $\forall x P(x)$ is a statement
that is true iff $P(x)$ is true for {\em every} $x$ in the universe of
discourse. 
\item[``$\exists$''] means ``there exists.'' $\exists x P(x)$ is true
iff $P(x)$ is true for {\em at least one} $x$ in the universe of
discourse.
\item[``$\nexists$''] mean ``there does not exist'' (``there is no'').
\item[``$\exists !$''] means ``there exists {\em exactly} one.''
\item[``$\forall x \in S$''] means ``for every $x$ in the set $S$.''
$(\forall x \in S) P(x)$ is equivalent to $\forall x (x \in S \implies P(x)).$
\end{description}

Quantifiers can turn predicates into propositions\.
For example:
\[
\forall x (P(x) \wedge Q(x) \implies R(x))
\]
Each occurrence of $x$ is associated with the $\forall$ quantifier\.  
A variable occurrence associated with a quantifier in this way is 
said to be {\em bound}\.  
Since every variable in the expression above is bound, it is a
proposition\.  
If $P$, $Q$, and $R$ are the predicates defined above, this
proposition says ``every prime number greater than 2 is odd'' and is true.

{\bf Note:} $\forall x \exists y$ is {\em different} from $\exists y
\forall x$:
\begin{itemize}
\item Suppose $S(x,y)$ means student $x$ falls asleep in class $y$.
\item $\forall y \exists x P(x,y):$ ``In every class, some student falls asleep.''
\item $\exists x \forall y P(x,y):$ ``There exists a student who 
falls asleep in every class.''
\end{itemize}

\subsection{Deduction rules involving quantifiers}

\reading{Velleman 2.2, Rosen, p. 173}

We've already seen deduction rules for arbitrary propositions\.  
There are others special to propositions with quantifiers\.
First, for negating quantified statements:
\begin{itemize}
\item $\neg [\forall x S(x)]$ is equivalent to $\exists x \neg S(x)$. \\
  Example: $\forall x S(x):$  For all primes $x > 2$, $x$ is odd. \\
  $\exists x \neg S(x):$  There is some prime $x > 2$ such that $x$
is not odd.\\
  (Domain of discourse:  The set of primes $> 2$)
\item $\neg [\exists x S(x)]$ is equivalent to $\forall x \neg S(x)$. \\
  Example: $\exists x S(x):$  There is an even prime.\\
  $\forall x \neg S(x):$  All primes are not even.\\
  (Domain of discourse:  Primes)
\end{itemize}
There are four main rules for manipulating quantifiers in proofs:
\begin{description}
\item[Universal Generalization UG:] 
To prove something is true for all $x$ ($\forall x$), 
give a proof that works for any particular $x$.

\item[Universal Instantiation UI:] 
If a statement is true for all $x$ ($\forall x$), then it is true for
any particular $x$ we want to study.

\item[Existential Generalization EG: ] 
If we have exhibited one $x$ that satisfies some property, we have
proved one exists ($\exists x$).

\item[Existential Instantiation EI:] 
If we know that some $x$ exists satisfying a property ($\exists x$),
then we can choose one and use it in the proof.
\end{description}
Like axioms, these inference rules are {\em agreements\/} to
believe certain inferences\.  For example, the constructivists (e.g.
Brouwer) {\em reject} the claim that $\neg [\forall x \neg P(x)]$ implies
$\exists x P(x)$\.  They claim that to prove something exists, you
actually have to construct it\.  Brouwer retracted his most famous
theorem after he became a constructivist, since the proof was
nonconstructive.
