\documentclass{exam}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{tikz}
\usetikzlibrary{arrows}
\usepackage{pgfplots}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{tabularx,ragged2e}
\usepackage{hyperref}
\usepackage{color}
\usepackage{enumerate}
\usepackage{tabularx,ragged2e}
\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
            \node[shape=circle,draw,inner sep=2pt] (char) {#1};}}

\newcommand{\dd}{\mathrm{d}}
\renewcommand*{\arraystretch}{2}
\cfoot{}
\begin{document}

\begin{coverpages}
\begin{center}{\huge MATH 2510 - EXAM 2 FALL 2019 \\
\vspace*{0.4in}
%\large Name: \makebox[3in]{\hrulefill}\\
SOLUTION
}
\end{center}

\begin{flushleft}\vspace{0.5in}
Thursday, 7 March \\
Instructor: Tom Cuchta
\end{flushleft}

\textbf{Instructions:}
\begin{itemize}
	\item  Show all work, clearly and in order, if you want to get full
	credit. If you claim something is true \textbf{you must show work backing up your claim}. I reserve the right to take off points if I cannot see how you arrived at your answer (even if your final answer is correct).
	\item Justify your answers algebraically whenever possible to ensure full credit. 	
	\item  Circle or otherwise indicate your final answers.
	\item  Please keep your written answers brief; be clear and to the point.
	\item  Good luck!
\end{itemize}

\begin{center}
\textbf{\underline{Axioms of first order arithmetic}} \\
\begin{enumerate}
\item $(\forall x)(0 \neq Sx)$ 
\item $(\forall x)(\forall y)(Sx=Sy \rightarrow x=y)$ 
\item $(\forall y)(y=0 \vee (\exists x)(Sx=y))$ 
\item $(\forall x)(x+0=x)$ 
\item $(\forall x)(\forall y)(x+Sy=S(x+y))$
\item $(\forall x)(x \cdot 0=0)$ 
\item $(\forall x)(\forall y)(x \cdot Sy=(x\cdot y)+x)$
\item $(\forall x)(\forall y)(x+y=y+x)$ 
\item $(\forall x)(\forall y)(x \cdot y = y \cdot x)$
\end{enumerate}
\end{center}

\end{coverpages}

\begin{questions}
\question[9] Translate the sentence into symbols using quantifiers.
\begin{parts}
\part[3] Some mammals are egglayers. \\
\textit{Solution}: $\exists x (Mx \wedge Ex)$
\part[3] No cats are insects.\\
\textit{Solution}: $\forall x(Cx \rightarrow \neg Ix)$
\part[3] All groups are quasigroups. \\
\textit{Solution}: $\forall x(Gx \rightarrow Qx)$
\end{parts}

\question[14] Prove $L \rightarrow \neg M$ from the premises $D \vee \neg L$ and $M \rightarrow \neg D$. \\
\textit{Solution}: \\
\[ \begin{array}{lll}
1 & (1) D \vee \neg L & \text{Premise} \\
2 & (2) M \rightarrow \neg D & \text{Premise} \\
1 & (3) \neg L \vee D & \vee-\text{commutativity on (1)} \\
1 & (4) L \rightarrow D & \text{equivalence of disjunction and implication on (3)} \\
2 & (5) \neg \neg D \rightarrow \neg M & \text{contraposition of (2)} \\
2 & (6) D \rightarrow \neg M & \text{replacing double negation on (5)} \\
1,2 & L \rightarrow \neg M & \text{syllogism on (4) and (6)}
\end{array}\]

\question[14] Prove $\neg \forall x Ax$ from the premises $\forall x Bx$ and $(\exists x \neg Ax) \vee (\exists x \neg Bx)$.
\[ \begin{array}{lll}
1 & (1) \forall x Bx & \text{Premise} \\
2 & (2) (\exists x \neg Ax) \vee (\exists x \neg Bx) & \text{Premise} \\
1 & (3) \neg \exists x \neg Bx & \text{negation of } \exists \text{ on (1)} \\
1,2 & (4) \exists x \neg A x & \text{m.t.p. on (2) and (3)}
\end{array}\]
\newpage 
\question[17] Prove $\exists x (Cx \wedge \neg Nx)$ from the premises $\forall x (Nx \rightarrow \neg Lx)$ and $\exists x (Lx \wedge Cx)$. \\
\textit{Solution}: \\
\[ \begin{array}{lll}
1 & (1) \forall x (Nx \rightarrow \neg Lx) & \text{Premise} \\
2 & (2) \exists x (Lx \wedge Cx) & \text{Premise} \\
2 & (3) L\alpha \wedge C\alpha & \exists \text{-elimination on (2)} \\
1 & (4) N\alpha \rightarrow \neg L \alpha & \forall \text{-elimination on (1)} \\
1 & (5) \neg \neg L\alpha \rightarrow \neg N\alpha & \text{contrapositive of (4)} \\
1 & (6) L\alpha \rightarrow \neg N\alpha & \text{replacing double negation on (5)} \\
2 & (7) L\alpha & \wedge \text{-elimination on (3)} \\
1,2 & (8) \neg N\alpha & \rightarrow\text{-elimination on (6) and (7)} \\
1,2 & (9) C\alpha & \wedge\text{-elimination on (3)} \\
1,2 & (10) C\alpha \wedge \neg N\alpha & \wedge\text{-introduction on (8) and (9)} \\
1,2 & (11) \exists x (Cx \wedge \neg Nx) & \exists\text{-introduction on (10)}
\end{array} \]

\question[14] Prove $\neg\Big(\neg (x=y) \vee \neg(y=z)\Big) \rightarrow (x=z)$ in pure identity theory (i.e. the theory with no axioms). \\
\textit{Solution}: \\
\[ \begin{array}{lll}
1 & (1) \neg \Big( \neg(x=y) \vee \neg (y=z) \Big) & \text{Premise} \\
1 & (2) \neg \neg (x=y) \wedge \neg \neg (y=z) & \text{DeMorgan law on (1)} \\
1 & (3) \neg \neg (x=y) & \wedge\text{-elimination on (2)} \\
1 & (4) \neg\neg (y=z) & \wedge\text{-elimination on (2)} \\
1 & (5) x=y & \text{double negation on (3)} \\
1 & (6) y=z & \text{double negation on (4)} \\
1 & (7) x=z & \text{substitution of ``=" on (5) and (6)} \\
\{\} & (8) \neg \Big( \neg(x=y) \vee \neg (y=z) \Big) \rightarrow (x=z) & \text{conditional proof on (1) and (7)}
\end{array}\]
\newpage 

\question[15] In homework, we proved the following theorem of first order arithmetic:  
\[ SS0 + SSS0 = SSSSS0, \] 
which depended on Axioms 4 and 5. Use that fact (if you want!) to help prove $SSS0 + SSS0=SSSSSS0$ in first order arithmetic. \\
\textit{Solution}: \\
\[\begin{array}{lll}
\text{Ax.5} & (1) \forall x \forall y (x+Sy=S(x+y)) & \text{Axiom 5} \\
\text{Ax.5} & (2) \forall y (SSS0+Sy=S(SSS0+y)) & \forall\text{-elimination on (1), x=SSS0} \\
\text{Ax.5} & (3) SSS0+SSS0=S(SSS0+SS0) & \forall\text{-elimination on (2)},y=SS0 \\
\text{Ax.4,Ax.5} & (4) SS0+SSS0=SSSSS0 & \text{given theorem} \\
\text{Ax.4,Ax.5} & (5) SSS0+SSS0=SSSSSS0 & \text{``="-substitution on (3) and (4)}
\end{array}\]

\question[17] The theory of differential algebra is defined by the axioms
\begin{enumerate}[D1:]
\item $\forall u \forall v \Big( \partial (u \cdot v) = (\partial u) \cdot v + u  \cdot (\partial v) \Big)$
\item $\forall u \forall v \Big( \partial (u+v)=\partial u + \partial v \Big)$
\end{enumerate} 
Prove 
\[ \forall u \forall v \Bigg( \partial (f \cdot g + h \cdot k) = \Big( (\partial f) \cdot g + f \cdot (\partial g)  \Big) + \Big( (\partial h) \cdot k + h \cdot (\partial k) \Big) \Bigg) \]
in differential algebra. \\
\textit{Solution}: \\
\[ \begin{array}{lll}
D2 & (1) \forall u\forall v\Big( \partial(u+v) = \partial u + \partial v \Big) & \text{Axiom D2} \\
D2 & (2) \forall v\Big(\partial( f\cdot g+v) = \partial (f\cdot g) + \partial v \Big) & \forall\text{-elimination on (1),} u=f\cdot g \\
D2 & (3) \partial (f\cdot g + h \cdot k) = \partial(f \cdot g) + \partial (h \cdot k)  & \forall\text{-elimination on (2)}, v=h\cdot k \\ 
D1 & (4) \forall u \forall v \Big( \partial ( u \cdot v ) = (\partial u) \cdot v + u \cdot (\partial v) \Big) & \text{Axiom D1} \\
D1 & (5) \forall v \Big( \partial(f \cdot v) = (\partial f)\cdot v + f \cdot (\partial v) \Big) & \forall\text{-elimination on (4)}, u=f \\
D1 & (6) \partial (f \cdot g) = (\partial f) \cdot g + f \cdot (\partial g) & \forall\text{-elimination on (5)}, v=g \\
D1 & (7) \forall v \Big( \partial(h \cdot v) = (\partial h)\cdot v + h \cdot (\partial v) \Big) & \forall\text{-elimination on (4)}, u=h \\
D1 & (8) \partial(h \cdot k) = (\partial h) \cdot k + h \cdot (\partial k) & \forall\text{-elimination on (7)}, v=k \\
D1, D2 & (9) \partial(f \cdot g + h\cdot k) = \Big( (\partial f) \cdot g + f \cdot (\partial g) \Big) + \Big( (\partial h)\cdot k + h \cdot (\partial k) \Big) & \text{``="-substitution on (3), (6), and (8)}
\end{array}\]
\end{questions}

\newpage 

\renewcommand*{\arraystretch}{1}

\begin{center} \underline{Propositional Consequences} \end{center}
\vspace{0.1in}

\begin{tabular}{|l|l|l|}
\hline 
From... & Consequence & Name \\
\hline
$P$ & $\neg \neg P$ & double negation \\
$\neg \neg P$ & $P$ & double negation \\
$F, G$ & $F \wedge G$ & $\wedge$-introduction \\
$F$ & $F \vee G$ & $\vee$-introduction \\
$F \wedge G$ & $G \wedge F$ & $\wedge$-commutativity \\ 
$F \vee G$ & $G \vee F$ & $\vee$-commutativity \\
$F \wedge G$ & $F$ & $\wedge$-elimination \\
$F, F\rightarrow G$ & $G$ & $\rightarrow$-elimination \\
$F \vee G$ & $\neg ( \neg F \wedge \neg G)$ & DeMorgan \\
$\neg (\neg F \wedge \neg G)$ & $F \vee G$ & DeMorgan \\
$F \wedge G$ & $\neg (\neg F \vee \neg G)$ & DeMorgan \\
$\neg (\neg F \vee \neg G)$ & $F \wedge G$ & DeMorgan \\
$F \leftrightarrow G$ & $(F \rightarrow G) \wedge (G \rightarrow F)$ & Biconditional \\
$(F \rightarrow G) \wedge (G \rightarrow F)$ & $F \leftrightarrow G$ & Biconditional \\
$P \rightarrow Q$ & $\neg Q \rightarrow \neg P$ & contraposition \\
$\neg P, P \vee Q$ & $Q$ & modus tollendo ponens (m.t.p.) \\
$P \rightarrow Q$, $Q \rightarrow R$ & $P \rightarrow R$ & syllogism \\
$P \rightarrow Q$ & $\neg P \vee Q$ & equivalence of disjunction and implication \\
$\neg P \vee Q$ & $P \rightarrow Q$ & equivalence of disjunction and implication \\
$(P \vee R) \wedge (P \vee \neg R)$ & $P$ & proof by cases \\
\hline
\end{tabular}

\noindent \textbf{Rule of conditional proof}: if $G$ is a consequence of $P_1, \ldots, P_n$ and an additional premise $F$, then $F \rightarrow G$ is a consequence of $P_1, \ldots, P_n$

\noindent \textbf{Proof by contradiction}: if the contradiction $G \wedge \neg G$ is a consequence of premises $P_1, \ldots, P_n$ and an additional premise $F$, then $\neg F$ is a consequence of the premises $P_1, \ldots, P_n$

\noindent \textbf{Replacing double negations inside of a formula}: If $\neg \neg P$ appears as a subformula of a formula $F$, then the formula $G$, where $G$ is the same as $F$ except that $\neg \neg P$ is replaced with $P$, may be concluded.

\noindent \textbf{Substitution of propositionally equivalent statement}: If a statement $Q$ is propositionally equivalent to a statement $P$, then any instance of $Q$ inside any statement may be replaced with $P$.

\noindent \textbf{$\forall$-elimination}: The formula $\forall x Px$ can be replaced with $P\alpha$, where $\alpha$ is \textbf{\textit{any}} constant or variable.

\noindent \textbf{$\forall$-introduction}: The formula $\forall x Px$ can be concluded whenever $Pv$ was previously concluded, \textbf{only when} $v$ is a variable.

\noindent \textbf{$\exists$-elimination}: From $\exists x Px$, one can conclude $P\alpha$, where $\alpha $ is a constant \textit{that has not previously been used in the proof}. 

\noindent \textbf{$\exists$-introduction}: If $P\alpha$ is known, where $\alpha$ is a \textit{constant or a variable}, then $\exists x Px$ can be concluded.

\noindent \textbf{Rule of negating $\forall$}: From $\neg \forall x Px$ can conclude $\exists x \neg Px$ and vice versa.

\noindent \textbf{Rule of negating $\exists$}: From $\neg \exists x Px$ can conclude $\forall x \neg Px$ and vice versa.

\noindent \textbf{Reflexivity of $=$}: $\forall x (x=x)$

\noindent \textbf{Symmetry of $=$}: $\forall x \forall y (x=y \rightarrow y=x)$

\noindent \textbf{Transitivity of $=$}: $\forall x \forall y \forall z \Big( (x=y \wedge y=z) \rightarrow x=z \Big)$

\noindent \textbf{Substitution of ``$=$"}: If $x=y$, then $x$ may be replaced with $y$ anywhere there is an $x$ not inside of a quantifier. (example: $Px \wedge Qy$ ok to replace with $Py \wedge Qy$ but $\exists x (Px \wedge Qy)$ is not ok to replace)
\end{document}
