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

\newtheorem{theorem}{Theorem}

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

\newif\ifanswers
\answerstrue


\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 Huth \& Ryan. Also read
the sample proofs in Section~2.3 and make sure you understand
how they fit together!


\section{Thinking in Predicate Logic}

Do Exercise 2.1.4(a-e,i), found on page 158 of Huth and Ryan.
Note that some relations like ``spouse'' don't have a predicate symbol for you to use; you'll
have to encode these as logical combinations involving the predicates you do have.

\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*{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.  Any proof involves using a
``classical'' rule like
proof-by-contradiction, or the law of the excluded middle, or (for the shortest proof)
$\lnot\lnot$-elimination.

But even constructive logicians will agree that
the formula ``isn't false,'' because
\[
\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's not the same
 as proof-by-contradiction.)
\bigskip


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

%%%
%%%


\end{document}

