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

\newtheorem{theorem}{Theorem}
\newif\ifanswers
\answersfalse


\renewcommand{\H}{\tiny \Checkmark}
\newcommand{\CLOSE}{$\!_{\mbox{\XSolidBrush}}$}

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

\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.
%%%
%%%
 \item Make sure your submission includes your name!
\end{itemize}

\hrule

\section*{Reading}
\textbf{Review Section 2.4 of Huth \&
  Ryan.}

\section{Tableau Proofs}
For each of the following, give a tableau proof.
\begin{enumerate}
\item $\vdash \quad (p \to q) \lor (q \to r)$


\item $(p \land q)\to r,\ r\to s, q \land \lnot s \quad \vdash \quad \lnot p$


\item $(\exists x.\ P(x)) \to (\exists y. Q(y))\quad \vdash\quad \exists z.\
  (P(z) \to Q(z))$


\item $\forall x.\ \bigl((P(x) \to Q(x)) \land (Q(x)\to
P(x))\bigr) \quad \vdash\quad (\forall x.\ P(x)) \to (\forall x.\ Q(x))$


\end{enumerate}

\goodbreak

\section{Proof or No Proof?}
For each of the following, give a \textbf{natural deduction} proof
if one exists.
\smallskip

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{Induction, Revisited}


Whenever we define a set inductively, we get an ``induction principle'' that
justifies proof by induction on that set. It says that, if the base cases have some property,
and all formation rules preserve the property, then everything in the set satisfies
the property.
\smallskip

For example, if we define a set $N$ inductively by saying
\begin{itemize}
  \item $Z \in N$
  \item If $n\in N$ then $Sn \in N$
\end{itemize}
\noindent then the corresponding induction principle is: for any predicate/property $P$,
\[
  P(Z) \quad \land \quad (\forall n{\in} N.\ \ P(n) \to P(Sn)) \qquad \to \qquad (\forall n{\in} N.\ \ P(n)).
\]

The resulting set $N=\{Z, SZ, SSZ, SSSZ, \ldots\}$ is isomorphic to the set of natural numbers (i.e., $Z$ stands for zero and $S$ stands for successor). It is thus no coincidence that the induction principle for $N$ corresponds exactly to the principle of induction on natural numbers $\mathbb{N}$ familiar from your math classes: for any predicate/property $P$ we have
\[
  P(0) \quad \land \quad (\forall n{\in} \mathbb{N}.\ \ P(n) \to P(n{+1})) \qquad \to \qquad (\forall n {\in} \mathbb{N}.\ \ P(n)).
\]

\enlargethispage{2.2\baselineskip}
\vspace{-0.5em}


    \begin{enumerate}
      \item Consider the inductive proof you did for Problem 2 in Assignment 1. (If you had significant trouble with it, you can start from the proof in our Sample Solution on Sakai.) It implicitly relies a similar induction principle for counting numbers (whole numbers starting at one, rather than zero):\[
  P(1) \quad \land \quad (\forall n{\ge} 1.\ \ P(n) \to P(n{+1})) \qquad \to \qquad (\forall n {\ge} 1.\ \ P(n)).
\]
The conclusion of your proof is that $\forall n{\ge}1.\ \ P(n)$ holds for some property $P(n)$. Exactly what property $P(n)$ is this?


      \item The principle of induction on counting numbers tells us that in order to prove  $\forall n{\ge}1.~P(n)$, \ \ it suffices (e.g., by an Modus Ponens implicit in telling the reader that you are using ``proof by induction'') to prove \[ P(1) \quad \land \quad (\forall n{\ge} 1.\ \ P(n) \to P(n{+1})).\]
        Such a proof requires (at least) uses of $\land i$, $\forall i$, and two uses of ${\to}i$. These natural deduction rules aren't mentioned in your proof for Problem 2, but all the necessary pieces are there. Carefully explain what parts of your proof correspond (explicitly or implicitly) to uses of these three natural deduction steps.

      \item In Problem 1 of Assignment 1, the bogus proof that all horses are the same color is structured as a proof by induction, trying to prove that $\forall n{\ge}1.\ \ P(n)$ for a different property $P(n)$. What is $P(n)$ for this problem? [The problem with the proof is \emph{not} the inductive structure, but rather that the subproof of
        $\forall n{\ge} 1.\ \ P(n) \to P(n{+1})$ contains an error!]


    \end{enumerate}


\end{document}
