\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,amsfonts,amssymb}
\usepackage{fitch}

\newtheorem{theorem}{Claim}
\newcommand{\prf}{{\sl Proof}: }
\newcommand{\qed}{$\Box$}
\newcommand{\imp}{\rightarrow}

\begin{document}

\par\noindent{\bf CS81 HW\#2 Spring 2012} {\em Out: 01/25/2012. Due: 02/01/2012 (before class)} 
\paragraph{\bf Policy on homeworks}
\begin{enumerate}
\item {\em Collaboration}: 
	You may discuss a question with any other student currently taking CS81 provided:
	(i) both of you contribute equally; 
	(ii) you come away from any discussion with an understanding in your mind (and no archived solution of any form is retained); 
	(iii) your submission is your own work prepared by yourself on a separate occassion.

\item {\em Reference materials}: 
	You should only refer to materials from this semester of CS81 
	(class notes, handouts, textbooks, grutors, instructor, etc).

\item {\em Submission}:
	Your submission should be legible or is prepared using TeX.
\end{enumerate}

\paragraph{Prove or Disprove} 
If {\bf prove}, use only the Natural Deduction rules given below (augmented with the Copy rule).
If {\bf disprove}, provide a valuation or truth assignment which contradicts the assertion.
Some of these problems are adapted from Huth and Ryan.
\begin{enumerate}
\item The other half of the Distributive Law $((a \wedge b) \vee (a \wedge c)) \vdash (a \wedge (b \vee c))$.
\item One-half of De Morgan's Law: $(\neg a \vee \neg b) \vdash \neg(a \wedge b)$.
\item Implication as Disjunction: $(a \imp b) \vdash (\neg a \vee b)$.
\item Disjunction as Implication: $(\neg a \vee b) \vdash (a \imp b)$.
\item Disjunction of Premises implies Disjunction of Goals:\\
	 $\{(a \imp b), (c \imp d)\} \vdash ((a \vee c) \imp (b \vee d))$.
\item Conjunction of Premises implies Conjunction of Goals:\\
	$\vdash (a \imp b) \imp ((c \imp d) \imp ((a \wedge c) \imp (b \wedge d)))$.
\item Peirce's Law: $\vdash (((a \imp b) \imp a) \imp a)$.
\item Mangled Form of Peirce's Law: $\vdash (b \imp (a \imp (b \imp a)))$.
\item Negating (an Implication) means Swapping: $\neg(a \imp b) \vdash (b \imp a)$.
\item Distributive Law for Conjunction and Implication: $((a \imp b) \wedge (a \imp c)) \vdash (a \imp (b \wedge c))$.
\item De Morgan's Law for Implication:
	$((a \wedge b) \imp c) \vdash (a \imp c) \vee (b \imp c)$.
\item Pseudo Modus Tollens: $\{(a \imp (b \imp c)), \neg c, a\} \vdash \neg b$.
\item Yet Another Modus Tollens: $\{(a \imp (b \imp c)), \neg b, \neg c\} \vdash \neg a$.\\
	(if you choose {\bf prove}, do not employ Modus Tollens)
\item Cutting Rule: $\{(a \vee b), (\neg b \vee c)\} \vdash (a \vee c)$.
\item Goal Switching in Disjunction of Implications:
	$((a \imp x) \vee (b \imp y)) \vdash ((a \imp y) \vee (b \imp x))$.
\end{enumerate}


\newpage 

\begin{footnotesize}
\paragraph{Natural Deduction Rules (or Magnificent Seven Little Engines of Logic)}

\begin{enumerate}
\item Conjunction Introduction $\wedge\mathcal{I}$ and
Conjunction Eliminations $\wedge\mathcal{E}1$ and $\wedge\mathcal{E}2$:
\[
\begin{nd}
\hypo {1} {\alpha}
\hypo {2} {\beta}
\have {3} {(\alpha \wedge \beta)}
\end{nd}
\begin{nd}
\hypo {1} {(\alpha \wedge \beta)}
\have {2} {\alpha}
\end{nd}
\begin{nd}
\hypo {1} {(\alpha \wedge \beta)}
\have {2} {\beta}
\end{nd}
\]

\item Disjunction Introductions $\vee\mathcal{I}1$ and $\vee\mathcal{I}2$, and
Disjunction Elimination $\vee\mathcal{E}$ (Proof by Cases):
\[
\begin{nd}
\hypo {1} {\alpha}
\have {2} {(\alpha \vee \beta)}
\end{nd}
\begin{nd}
\hypo {1} {\alpha}
\have {2} {(\beta \vee \alpha)}
\end{nd}
\begin{nd}
\have {1} {(\alpha \vee \beta)}
\open
\hypo {3} {\alpha}
\have {4} {\gamma}
\close
\open
\hypo {5} {\beta}
\have {6} {\gamma}
\close
\have {7} {\gamma}
\end{nd}
\]

\item Implication Introduction $\rightarrow\mathcal{I}$ and Implication Eliminations 
(Modus Ponens (MP) and Modus Tollens (MT)):
\[
\begin{nd}
\open
\hypo {1} {\alpha}
\have {2} {\beta}
\close
\have {3} {(\alpha \rightarrow \beta)}
\end{nd}
\begin{nd}
\hypo {1} {(\alpha \rightarrow \beta)}
\hypo {2} {\alpha}
\have {3} {\beta}
\end{nd}
\begin{nd}
\hypo {1} {(\alpha \rightarrow \beta)}
\hypo {2} {\neg\beta}
\have {3} {\neg\alpha}
\end{nd}
\]

\item Negation Introduction $\neg\mathcal{I}$ (Proof By Contradiction) and Negation Elimination $\neg\mathcal{E}$:
\[
\begin{nd}
\open
\hypo {1} {\alpha}
\have {2} {\bot}
\close
\have {3} {\neg \alpha}
\end{nd}
\begin{nd}
\hypo {1} {\alpha}
\hypo {2} {\neg \alpha}
\have {3} {\bot}
\end{nd}
\]

\item Falsehood Introduction $\bot\mathcal{I}$ and Falsehood Elimination $\bot\mathcal{E}$:
\[
\begin{nd}
\hypo {1} {\alpha}
\hypo {2} {\neg \alpha}
\have {3} {\bot}
\end{nd}
\begin{nd}
\hypo {1} {\bot}
\have {2} {\alpha}
\end{nd}
\]

\item 
Double Negation Introduction $\neg\neg\mathcal{I}$ and Double Negation Elimination $\neg\neg\mathcal{E}$:
\[
\begin{nd}
\hypo {1} {\alpha}
\have {2} {\neg\neg\alpha}
\end{nd}
\begin{nd}
\hypo {1} {\neg\neg\alpha}
\have {3} {\alpha}
\end{nd}
\]

\item Law of Excluded Middle (LEM):
\[
\begin{nd}
\have {1} {(\alpha \vee \neg\alpha)}
\end{nd}
\]

\end{enumerate}

\end{footnotesize}

\newpage

\begin{small}
\paragraph{Example} Prove or disprove this one-half of the Distributive Law:
\[
((a \vee b) \wedge c) \vdash (a \wedge c) \vee (b \wedge c).
\]
Prove! Here is the derivation using Natural Deduction rules:
\[
\begin{nd}
\hypo {1} {((a \vee b) \wedge c)} 	\by{premise}{}
\have {2} {(a \vee b)} 				\ael{1}
\open
\hypo {3} {a} 					\by{assumption}{}
\have {4} {c}  					\aer{1} 
\have {5} {(a \wedge c)} 		\ai{3,4}
\have {6} {(a \wedge c) \vee (b \wedge c)} \oil{5}
\close

\open
\hypo {7} {b}					\by{assumption}{}
\have {8} {c}  					\aer{1}	
\have {9} {(b \wedge c)}  		\ai{7,8}
\have {10} {(a \wedge c) \vee (b \wedge c)} \oir{8}
\close

\have {11} {(a \wedge c) \vee (b \wedge c)} \oe{2,3-6,7-10}
\end{nd}
\]
So,
$((a \vee b) \wedge c) \vdash (a \wedge c) \vee (b \wedge c)$ is {\em provable}
({\em derivable} or {\em valid}) under the Natural Deduction proof system.
\end{small}


\end{document}



