\documentclass[12pt]{cas-handout}
\usepackage{amsfonts,amsthm,multicol}
\usepackage{eulervm,paralist}
\newtheorem{theorem}{Theorem}

\anumber{3}
\title{Predicate Logic}
\duedate{11:00am, Wednesday, September 21}

\begin{document}
\maketitle 

\begin{itemize}
  \item Emails about this assignment should be directed to
    \helpalias.
  \item The usual collaboration rules apply. You may \emph{discuss} an
    exercise with any other student(s) currently taking CS 81 as long as:
    \begin{itemize}
      \item You contribute equally;
      \item You come away from this discussion only with
        \emph{understanding in your head} --- no written materials or
        computer notes may be retained;
      \item Your submission is authored solely by you, on a separate
        occasion.
   \end{itemize}
  \item You should refer only to materials from this semester of CS 81 (lecture
   notes, handouts, textbooks, grutors, profs, etc.).
 \item Bring a writeup/printout to class on the due date. Illegible answers
    will get no credit. (For this reason, the grutors like you to use \LaTeX.
    But it's up to you.)
 \item Make sure your submission includes your name!
\end{itemize}

\hrule

\section*{Reading}
Review Sections 2.1--2.3 of Huth \& Ryan. Pay particular attention to
the sample proofs in Section~2.3; make sure you understand
how they fit together.


\eject

\section{Thinking in Predicate Logic}

Do Exercise 2.1.4(a-k), found on page 158 of Huth and Ryan.

\goodbreak

\section{Formal Logic}
Give natural deduction proofs of the following:


\newcommand{\ex}[1]{\strut{\scriptsize \\\mbox{}\hfill (#1)}}
\newcommand{\eg}[1]{\ex{e.g., #1}}

\begin{enumerate}
\item $\exists x.\ (R(x)\to B(x)) \vdash 
  (\forall x.\ R(x)) \to (\exists x.\ B(x))$
\eg{$R(x) =$ ``$x$ is red'', $B(x) =$ ``$x$ is bacon-flavored''}


\item $(\forall x.\ L(x)) \lor (\forall x. F(x)) \vdash \forall x.\ (L(x) \lor F(x))$
\eg{$L(x) =$ ``$x$ is lost'', $F(x) =$ ``$x$ is found''}

\item $\forall x.\ (I(x) \lor U(x)) \vdash 
(\forall x.\ I(x)) \lor (\exists x. U(x))$
\eg{$I(x) =$ ``$x$ is interesting'', $U(x) =$ ``$x$ is unremarkable''}

\item $\forall x.\ (p \to Q(x)) \vdash p \to \forall x. Q(x)$
\eg{$p =$ ``I'm wearing earplugs'', $Q(x) =$ ``$x$ is quiet''}

\item $\vdash \exists x.\ (D(x) \to \forall y.\
  D(y))$
\ex{The ``drinker's paradox'': there is at least one person 
satisfying ``if he/she drinks beer, then everyone drinks beer.''}

\item $\lnot(\exists x.\, U(x)) \lor (\forall x.\, V(x)),\ 
       p{\to}\forall x.\,D(x) \ \vdash \ 
       \forall y.\,\forall z.\ ((\lnot U(z)\lor\, V(y)) \land (p\to D(y)))$
\eg{$U(x) =$ ``$x$ is a unicorn'', $V(x) =$ ``$x$ is a vegetable'',
    $p = $ ``I'm hungry'', $D(x) =$ ``$x$ is delicious''}

\item $\forall x.\ \lnot S(x,x), \ 
       \forall x.\,\forall y.\,\forall z.\ S(x,y)\land S(y,z) \to
       S(x,z)  \ \vdash\ 
       \forall x.\,\forall y. S(x,y) \to \lnot S(y,x)$
\eg{$S(x,y) =$ ``movie $x$ is a sequel to movie $y$''}
\end{enumerate}

\section{Informal Logic}

Here is some background in set theory:  for all sets $X$ and $Y$ and
all elements $z$,
\[
\begin{array}{l}
  z \not\in X \iff \lnot(z\in X)\\
  z \in (X \cup Y) \iff (z \in X) \lor (z \in Y)\\
  z \in (X \cap Y) \iff (z \in X) \land (z \in Y)\\
  z \in (X \setminus Y) \iff (z \in X) \land \lnot(z \in Y)\\
  X \subseteq Y \iff \forall x.\ (x\in X \to x\in Y)\\
  X = Y \iff (X \subseteq Y) \land (Y \subseteq X)\\
  X \mathop{\mathrm{meets}} Y \iff \exists z.\ z\in (X\cap Y)\\
\end{array}
\]

\goodbreak

For each of the following two propositions, give
\begin{enumerate}
\item[(a)] 
a proof in \emph{mathematical English}. (For the first
  one, you only need to complete the proof provided.) Your proof should
  be 1--3 paragraphs of English text, as one might find in a 
  (very precise) math book or textbook. 

  The only mathematical symbols in your proof should be 
  set-theory symbols ($\in$, $\not\in$, $\subseteq$, $\cup$, etc.). 
  Do not include any formal logic
  symbols ($\forall$, $\exists$, $\land$, $\lnot$, etc.)

  Your proof should be complete and without holes. They will probably
  not be great literature but, where possible, strive for clarity.

 \item[(b)] Identify
   four natural deduction rules that correspond to (explicit or implicit)
   steps in your proof, and at least one part of each proof to
   which that rule corresponds.
 \end{enumerate}

\begin{enumerate}
\item $A \setminus (B \setminus C) = (A\setminus B) \cup (A \cap C)$.

\begin{enumerate}
\item 
  \begin{proof}
    Let $x\in A\setminus (B\setminus C)$ be given.  Then $x\in A$ and
    $x\not\in B\setminus C$. That is, $x\not\in B$ or $x\in C$. If
    $x\not\in B$, then $x\in A\setminus B$; if $x\in C$ then $x\in
    A\cap C$. In either case, $x \in (A\setminus B) \cup (A \cap
    C)$. Thus $A\setminus (B\setminus C) \subseteq (A\setminus
    B) \cup (A \cap C)$.

\ldots
  \end{proof}

\end{enumerate}
 

\item If $A \mathop{\mathrm{meets}} B$, then 
$A \cup B \not\subseteq (A \setminus B) \cup (B \setminus A)$.
\end{enumerate}




\section*{Extra Credit [10\%]}


The formula 
$\lnot\lnot p\to p$
is a tautology, but it is not provable in constructive
(a.k.a. intuitionistic) logic.  That is, to prove it you need to use a
non-constructive rule like 
proof-by-contradiction, or the law of the excluded middle, or (for
a trivial proof) $\lnot\lnot$-elimination.

On the other hand, even constructive logicians will agree that
the formula isn't false;
$
\lnot\lnot(\lnot\lnot p\to p)
$
\emph{is} provable constructively, without any 
non-constructive rules. Provide a constructive proof.
 (You will need $\lnot$-introduction, but that
is a rule \emph{different} from proof-by-contradiction.)
\bigskip


\noindent [This problem is nontrivial; 
don't spend too much time on it unless
you find it interesting!]

\end{document}

