\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\#3 Spring 2012} {\em Out: 02/01/2012. Due: 02/08/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 {\em model} where the assertion does not hold.
Some of the problems are adapted from Huth and Ryan.

\paragraph{Convention} All predicates are denoted by upper-case letters. All variables are denoted by
lower-case letters late in the alphabet (such as $x,y,z$). All atomic constants are denoted by
lower-case letters early in the alphabet (such as $a,b,c$).

\begin{enumerate}
\item Negating an Existential Negative means Universal Positive:
\[
\begin{nd}
\hypo {1} 
{\neg (\exists x) \neg P(x)}
	\by{premise}{}
\have {2} 
{(\forall x) P(x)}
	\by{goal}{}
\end{nd}
\]

\item One of the Distributive Laws for Quantifiers:
\[
\begin{nd}
\hypo {1} {(\forall x)[P(x) \vee Q(x)]}
	\by{premise}{}
\have {2} {(\forall x) P(x) \vee (\forall x) Q(x)}
	\by{goal}{}
\end{nd}
\]


\item The Other Part of the Distributive Laws for Quantifiers:
\[
\begin{nd}
\hypo {1} {(\exists x)[P(x) \wedge Q(x)]}
	\by{premise}{}
\have {2} {(\exists x) P(x) \wedge (\exists x) Q(x)}
	\by{goal}{}
\end{nd}
\]


\item Irreflexive and Transitive means Never Having to Be Symmetric:
\[
\begin{nd}
\hypo {1} {(\forall x)(\forall y)(\forall z)[(E(x,y) \wedge E(y,z)) \imp E(x,z)]}
	\by{premise}{}
\hypo {2} {(\forall x) \neg E(x,x)}
	\by{premise}{}
\have {3} {(\forall x)(\forall y)[E(x,y) \imp \neg E(y,x)]}
	\by{goal}{}
\end{nd}
\]


\item Universal Modus Ponens:
\[
\begin{nd}
\hypo {1} {(\forall x)[P(x) \imp (Q(x) \vee R(x))]}
	\by{premise}{}
\hypo {2} {\neg (\exists x)[P(x) \wedge R(x)]}
	\by{premise}{}
\have {3} {(\forall x)[P(x) \imp Q(x)]}
	\by{goal}{}
\end{nd}
\]

\item Triple Substitution:
\[
\begin{nd}
\hypo {1} {(\forall x)[P(x) \imp (\forall y) E(y,y,\hat{b})]} 
	\by{premise}{}
\hypo {2} {(\forall x)(\forall y)[E(\hat{a},y,x) \imp F(x,y,y)]}
	\by{premise}{}
\have {3} {P(\hat{a}) \imp (\exists x) F(x,\hat{c},\hat{c})}
	\by{goal}{}
\end{nd}
\] 

\item Law of Included Middle:
\[
\begin{nd}
\hypo {1} {(\forall x)(\exists y) L(x,y)}
	\by{premise}{}
\have {2} {(\forall x)(\forall y)[L(x,y) \imp (\exists z)(L(x,z) \wedge L(z,y))]}
	\by{goal}{}
\end{nd}
\]


\item Existential Tag:
\[
\begin{nd}
\hypo {1} {(\exists x)[P(x) \vee (\forall y)(E(x,y) \imp P(y))]} 
	\by{premise}{}
\hypo {2} {(\forall x)[E(x,\hat{a}) \wedge \neg P(\hat{a})]}
	\by{premise}{}
\have {3} {(\exists x) P(x)}
	\by{goal}{}
\end{nd}
\] 

\item Quantified Proof by Cases:
\[
\begin{nd}
\hypo {1} {(\forall x)(\forall y)[(B(y) \vee C(x)) \imp Z(y)]} 
	\by{premise}{}
\hypo {2} {(\forall x)(\exists y)[A(x) \imp Z(y)]}
	\by{premise}{}
\hypo {3} {(\exists x)[A(x) \vee B(x)]}
	\by{premise}{}
\have {4} {(\exists x) Z(x)}
	\by{goal}{}
\end{nd}
\] 

\item Existential Modus Tollens:
\[
\begin{nd}
\hypo {1} {(\forall x)[A(x) \imp Z(x)]} 
	\by{premise}{}
\hypo {2} {(\exists x)[B(x) \wedge Z(x)] \wedge (\exists x)[B(x) \wedge \neg Z(x)]} 	
	\by{premise}{}
\have {3} {\neg (\forall x)[B(x) \imp A(x)]}	
	\by{goal}{}
\end{nd}
\] 


\item Reducibility:
\[
\begin{nd}
\hypo {1} {(\forall x)(\forall y)[(E(x,\hat{a}) \wedge E(\hat{a},y)) \imp E(x,y)]} 
	\by{premise}{}
\hypo {2} {(\forall x)[P(x) \imp E(\hat{a},x)]}
	\by{premise}{}
\hypo {3} {(\exists x)[P(x) \wedge E(x,\hat{a})]}	
	\by{premise}{}
\have {4} {(\exists x)(P(x) \wedge (\forall y)[P(y) \imp E(x,y)])}
	\by{goal}{}
\end{nd}
\] 

\item Contrapositive Law for Quantifiers:
\[
\begin{nd}
\hypo {1} {(\forall x)(\forall y)(A(x) \imp B(y))}	
	\by{premise}{}
\have {2} {(\exists y)[\neg B(y)] \imp (\forall x)[\neg A(x)]}
	\by{goal}{}
\end{nd}
\]

\item Contrapositive Law Reversed:
\[
\begin{nd}
\hypo {1} {(\exists y)[\neg B(y)] \imp (\forall x)[\neg A(x)]}
	\by{premise}{}
\have {2} {(\forall x)(\forall y)(A(x) \imp B(y))}	
	\by{goal}{}
\end{nd}
\]

\item Yet Another Contrapositive Law for Quantifiers:
\[
\begin{nd}
\hypo {1} {(\exists x)(\forall y)(A(x) \imp B(y))}	
	\by{premise}{}
\have {2} {\neg (\forall x)A(x) \vee (\forall y)B(y)}
	\by{goal}{}
\end{nd}
\]

\item Existential Loops:
\[
\begin{nd}
\hypo {1} {(\forall x)(\forall y)[(P(x) \wedge P(y)) \imp (E(x,y) \imp E(y,x))]} 
	\by{premise}{}
\hypo {2} {(\forall x)(\forall y)(\forall z)\{[(P(x) \wedge P(y)) \wedge P(z)] \imp 
		[(E(x,y) \wedge E(y,z)) \imp E(x,z)]\}} 	
	\by{premise}{}
\have {3} {(\forall x)([P(x) \wedge (\exists z)(P(z) \wedge E(x,z))] \imp E(x,x))}	
	\by{goal}{}
\end{nd}
\] 


\end{enumerate}


\newpage 

\begin{footnotesize}
\paragraph{Natural Deduction Rules for Predicate 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}
\]

\item Universal Introduction $\forall\mathcal{I}$ and Universal Elimination $\forall\mathcal{E}$:
\[
\begin{nd}
\hypo {1} {\alpha(a)}
\have {3} {(\forall x) \alpha(x)}
\end{nd}
\begin{nd}
\hypo {1} {(\forall x) \alpha(x)}
\have {2} {\alpha(a)}
\end{nd}
\]
Here $a$ stands for an arbitrary (free) constant.

\item Existential Introduction $\exists\mathcal{I}$ and Existential Elimination $\exists\mathcal{E}$:
\[
\begin{nd}
\hypo {1} {\alpha(a)}
\have {3} {(\exists x) \alpha(x)}
\end{nd}
\begin{nd}
\hypo {1} {(\exists x) \alpha(x)}
\have {2} {\alpha(\hat{a})}
\end{nd}
\]
Here $a$ stands for some constant (free or otherwise) and $\hat{a}$ stands for a bound (not free) constant.



\end{enumerate}

\end{footnotesize}

\begin{small}
\paragraph{Example} Prove or disprove this quarter of DeMorgan's Law for Quantifiers:
\[
(\forall x)[\neg P(x)] \vdash \neg (\exists x) P(x).
\]
Prove! Here is the derivation using Natural Deduction rules:
\[
\begin{nd}
\hypo {1} {(\forall x)[\neg P(x)]} 	\by{premise}{}
\open
\hypo {2} {(\exists x) P(x)}		\by{assumption}{}
\have {3} {P(\hat{a})} 			\Ee{2} 
\have {4} {\neg P(\hat{a})} 		\Ae{1}
\have {5} {\bot}			\ne{3,4}
\close

\have {6} {\neg (\exists x) P(x)}	\ni{2-5}
\end{nd}
\]
\end{small}


\end{document}



