\documentclass[12pt]{cas-handout}

\anumber{2}
\title{Propositional Logic}
\duedate{11:00am, Wednesday, September 19}

\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. Illegible answers
    will get no credit. (For this reason, the grutors recommend \LaTeX.
    But it's up to you.)
 \item The assignments web page has links to some resources for
    formatting your proofs.
 \item Make sure your submission includes your name!
\end{itemize}

\hrule

\subsection*{Reading}

In Huth \& Ryan, review Chapter 1 \emph{up to and including} Section 1.4.1
(except for Section 1.3, which you are free to skip). \textbf{Pay particular
attention to the example proofs in Section 1.2, since they'll get you in the right
mindset to do proofs of your own!}
\bigskip

\noindent There are further hints on doing proofs on the last page of this handout.

\clearpage

\subsection*{Exercises}

\begin{enumerate}
\item Give proofs for the following propositions from Exercise 1.2
  (pages 79--80) of Huth \& Ryan: 1(p), 1(s), 3(c), 3(e), 3(l).


\item \textbf{Pierce's Law} is the formula
\[
((p \to q) \to p) \to p
\]
\begin{enumerate}
\item By using truth tables, show that Pierce's law is a tautology,
  (i.e., that \[\models ((p \to q) \to p) \to p,\] or equivalently
  that this formula is true under every valuation).
\item Prove Pierce's Law.

\begin{quote}
  \small
  \textbf{Hint}: \it As mentioned in class (and in Section 1.2.5 of
  Huth \& Ryan), \emph{constructive} propositional logic rejects the
  use of ``indirect'' arguments.  Consequently, in constructive logic
  one cannot use the excluded middle ($\vdash p\lor\neg p$),
  double-negation elimination ($\neg\neg p\vdash p$), or proof by
  contradiction (if $\neg p\vdash \bot$, then $\vdash p$) for an
  arbitrary proposition $p$. It turns out that in constructive logic, Pierce's
  Law is not provable. Therefore, your proof has to involve at least one
  use of a classical rule.
\end{quote}
\end{enumerate}

\item \textbf{Proof or No Proof?}
For each of the following, either show there is no proof
(by finding a valuation/model that makes the assumptions true
and the conclusion false),
or provide a natural deduction proof.

\begin{enumerate}
\item Premise: $\lnot p \lor (q\to p)$.  Conclusion: $\lnot p\land q$.
\item Premise: $p\to q$ and $\lnot p\to q$. Conclusion: $q$.
\item Premise: $p\to q\to r$. Conclusion: $q \to p\to r$.
\item Premise: $p\to q\to r$. Conclusion: $p \to r\to q$.
\item Premise: $(p \to q) \to r$. Conclusion: $p \to q\to r$.
\item Premise: $p\to q$ and $s\to t$. Conclusion: $p \lor s \to q \land t$.
\end{enumerate}

\clearpage

\item \textbf{OS Wars}: Consider the following argument:
\begin{itemize}
\item Premise 1:  If my computer runs Windows, then Microsoft got my money.
\item Premise 2:  If my computer runs Mac OS X, then Apple got my money.
\item Conclusion: At least one of the following statements is true:
  \begin{itemize}
  \item If my computer runs Mac OS X, then Microsoft got my money
  \item If my computer runs Windows, then Apple got my money
  \end{itemize}
\end{itemize}

\goodbreak

Either provide a formal proof that this argument holds, or find a
valuation where the assumptions are
true but the conclusion is false.  You may want to
abbreviate certain propositions (e.g., as $p$, $q$, etc.) for
the purposes of your valuation or your proof, but be sure to
define any such abbreviations.

\item Recall that
\[
\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)\\
\end{array}
\]
Suppose we want to prove that
\[
x\in (A\setminus B)\cup(A\cap C) \quad \to \quad x\in A \setminus (B\setminus C).
\]
\begin{enumerate}
  \item Translate the statement into a propositical-logic statement involving the
     three predicates $x\in A$, $x\in B$, and $x\in C$.
  \item Give a natural deduction proof of this statement. Be careful to use only the official
    natural deduction rules, and not other properties of sets or logic.
  \item Give a proof that if $x\in (A\setminus B)\cup(A\cap C)$ then $x\in A \setminus (B\setminus C)$ in ``mathematical English,'' in
    a form that would convince a Mathematics professor.
  \item How are the two proofs similar? How are the two proofs different?
\end{enumerate}


\item Answer the following survey questions:
\begin{enumerate}
\item How long did you spend on this assignment?
\item What was easiest?  What was most difficult?
\item With whom, if anyone, did you collaborate with on this assignment?
\end{enumerate}

\end{enumerate}

\subsection*{Further Hints}

\begin{itemize}
\item Make sure you understand all the sample proofs in Section~1.2!

\item A common question is ``What do I do with an \emph{assumption}
  of the form $\lnot A$?''. The answer is ``It depends.''

However, the
  most common pattern is to show that other assumptions (either those
  you were given or those you have assumed inside a box) imply $A$,
  and then use the fact that you've reached a contradiction.

  [See
  lines 3--5 in the left half of Example 1.20, or lines 2--4 in the
  second proof on page 25.]

\item Another common question is ``How do I prove a \emph{conclusion}
  of the form $A\lor B$?''  The answer is ``It depends.''

  However, unless you can show
  that $A$ is definitely true or that $B$ is
  definitely true, the most common pattern is to use proof by cases
  (a.k.a. or-elimination). In one case prove $A$ (and hence $A\lor B$
  by or-introduction), and the other case prove $B$ (hence $A \lor
  B$). In either case, $A\lor B$, so we can conclude it must be true.

  Which two cases? Well, if you already have some other
  disjunction around (assumed or proved)
  you might do cases on which half is true.
  Alternatively, you can use the law of the excluded middle
  to prove your own disjunction $C\lor\lnot C$ (for some specific
  and relevant formula $C$); then do
  one case where $C$ is assumed, and one case where $\lnot C$ is assumed.

  [See Example~1.24.]



\end{itemize}



\end{document}
