\documentclass[12pt]{cas-handout}
\usepackage{amsmath,amsfonts,multicol}
\usepackage{paralist}
\usepackage{pdfpages}

\newtheorem{theorem}{Theorem}

\anumber{4}
\title{More Predicate Logic}
\duedate{11:00am, Wednesday, September 28}

\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{compactitem}
      \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{compactitem}
  \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

\bigskip\bigskip
\noindent
\textbf{Review Section 2.4 of Huth \&
  Ryan.}
\clearpage

\section{Proof or No Proof?}
For each of the following, give a natural deduction proof
if one exists. If there is no proof, you should
\begin{compactenum}
  \item Define a model that makes the assumptions true
and the conclusion false;
  \item Briefly explain why the assumptions are true and the conclusions
are false;
  \item \emph{Also}, find an alternate model that makes the
    conclusion \emph{true}. (It doesn't matter whether this new model
    makes the assumptions true or not; this is just more
   practice with models.)
\end{compactenum}

\bigskip

\begin{enumerate}
\item 
Assumption: $\forall x.\ \forall y.\ (S(x,y)\to S(y,x))$\\
Conclusion: $\forall x.\ \lnot S(x,x)$

\item 
Assumption: $\top$ (i.e., no assumption)\\
Conclusion: $\forall x.\ \forall y. 
   \bigl(S(x,y) \to \exists w.\ (S(x,w) \land S(w,y))\bigr)$

\item 
Assumption: $\forall x.\ \bigl((P(x) \to Q(x)) \land (Q(x)\to
P(x))\bigr)$\\
Conclusion: $(\forall x.\ P(x)) \to (\forall x.\ Q(x))$


\item 
Assumption: $(\forall x.\ P(x)) \to (\forall x.\ Q(x))$\\
Conclusion: $\forall x.\ \bigl((P(x) \to Q(x)) \land (Q(x)\to P(x))\bigr)$

\item 
Assumption: $(\forall x.\ P(x)) \to q$\\
Conclusion: $\forall x.\ (P(x) \to q)$

\item 
Assumptions: $\exists x. P(x)$, \qquad $\exists y. Q(y)$\\
Conclusion: $\exists z.\ (P(z) \land Q(z))$

\item 
Assumption: $(\exists x. P(x)) \lor (\exists y. Q(y))$\\
Conclusion: $\exists z.\ (P(z) \lor Q(z))$

\item 
Assumption: $\forall x.\ \exists y.\ S(x,y)$\\
Conclusion: $\exists y.\ \forall x.\ S(x,y)$
\end{enumerate}

\clearpage

\section{Bounded Quantifiers}

In class, we mentioned that the ``bounded quantifier'' notation 
(where we restrict the individuals being quantified over) can be 
translate into the more
primitive notions on the right.
\[
\begin{array}{l@{\qquad\longrightarrow\qquad}l}
  \exists x\in S.\ P(x) & \exists x.\ (x\in S \land P(x))\\
  \forall x\in S.\ P(x) & \forall x.\ (x\in S \to P(x))\\[10pt]

  \exists x\le n.\ P(x) & \exists x.\ (x\le n \land P(x))\\
\forall x\le n.\ P(x) & \forall x.\ (x\le n \to P(x))\\
\end{array}
\]

\noindent It might be unexpected that the translations are
different for the different quantifiers: bounded-$\exists$ becomes a
logical-and, while the translation of bounded-$\forall$ becomes an
implication.

\begin{enumerate}
\item Describe a model ${\cal M}_1$ (where the set of individuals is the set of
$\mathbb{N}$ of natural numbers, and the relation $\le$ is interpreted
as the actual less-than-or-equal-to relation on $\mathbb{N}$) that makes
\[
\forall x \le n.\ f(x) \le m
\] 
and hence
\[
\forall x.\ (x \le n \to f(x) \le m)
\]
true but makes
\[
\forall x.\ (x \le n \land f(x) \le m)
\]
false. (That is, complete the model by giving interpretations of the function
$f$ and the constants $n$ and $m$.)

\item Describe a model ${\cal M}_2$ (where the set of individuals is
  $\mathbb{N}$ and the relation $\le$ is interpreted as less-than-or-equal-to
  relation on $\mathbb{N}$) that makes 
\[
\exists x.\ (x \le n \to f(x) \le m)
\]
true but makes
\[
\exists x\le n.\ f(x) \le m
\] 
and hence
\[
\exists x.\ (x \le n \land f(x) \le m)
\]
false.
\end{enumerate}

\section{Mathematical English, Revisited}

Read the attached short excerpt from Crossley's \textit{Essential
  Topology}.\footnote{Because the Claremont Library has a subscription,
  this book (like many other CS and Math texts published 
  by Springer Verlag) is available as free PDFs 
  at \url{http://springerlink.com/} (for personal use only). There's
  one PDF per chapter, but if you have the \texttt{pdftk} 
  program installed, there's a very nice download script available
  at \url{http://milianw.github.com/springer_download/} to get books
  as single PDFs.}

\begin{enumerate}
\item Proposition 2.4, if made more explicit, would be
something like ``for all collections, if the collection consists of
of open sets, then the union of that collection is open''
(where ``is open'' has its own logical definition, in the box at the
top of the page).  Consider the proof.
  \begin{enumerate}
  \item If we translated this mathematical english into a formal
    natural deduction proof, what 
     rule(s) correspond to 
     the first sentence?
  \item What rule(s) corresponds to the
     next phrase ``if x lies in the union $x\in\bigcup_{i\in I} S_i$, \ldots''?
   \item The proof implicitly uses extential elimination, twice. What
     are the two existentials, and what is the conclusion (``$C$'')
     of the subproofs?

     [Hint: the second sentence is (in part) reminding you that by
     definition of the $\bigcup$ operator, the
     assumption $x\in\bigcup_{i\in I} S_i$ means
     $\exists i{\in}I.\ x{\in}S_i$. Also,
     the existential eliminations are nested so there's really 
     one common conclusion.]
 \end{enumerate}

\item Identify four steps (explicit or implicit) in the proof of
  Lemma 2.8 that correspond to natural-deduction rules.  (Each
  should be a different natural-deduction rule.)

\item Identify four steps (explicit or implicit) in the proof of
  Theorem 2.9 that correspond to natural-deduction rules.  (Each
  should be a different natural-deduction rule.)
\end{enumerate}

\includepdf[pages=-,landscape]{crossley-excerpt.pdf}

\end{document}
