\documentclass{article}
\usepackage{hyperref}
\usepackage{enumerate}
\usepackage{amssymb}
\usepackage[normalem]{ulem}
\renewcommand*{\arraystretch}{2}

\begin{document}
\flushleft \underline{Homework 3 (solution) -- MATH 2510 Spring 2018} \\
\vspace{1mm}
\textbf{\#1.6}: Show that the following statements are equivalent: \\
\begin{enumerate}
\item $F \equiv G$, 
\item $\vDash F \leftrightarrow G$, and
\item $(F \wedge \neg G) \vee (\neg F \wedge G)$ is unsatisfiable.
\end{enumerate}
\textit{Solution}: First we show that if $F \equiv G$, then $\vDash F \leftrightarrow G$:
$$\begin{array}{|l|l|l|l|}
\hline 
F & G & F \leftrightarrow G \\
\hline
1 & 1 & 1 \\
\not{1} & \not{0} & \not{0}\\
\not{0} & \not{1} & \not{0}\\
0&0 & 1 \\
\hline
\end{array}$$  
In other words, we see in those rows for which $F \equiv G$ (i.e. $F \vDash G$ and $G \vDash F$, which means ``whenever $F$ is $1$ it follows that $G$ is $1$" and vice versa -- so we ignore the middle two rows!!), it is the case that $\vDash F \leftrightarrow G$ (i.e. $F \leftrightarrow G$ is a tautology). 

Now we show that if $\vDash F \rightarrow G$, then $(F \wedge \neg G) \vee (\neg F \wedge G)$:
$$\begin{array}{|l|l|l|l|l|l|l|l|l|}
\hline 
F & G & F \leftrightarrow G & \neg F & \neg G & F \wedge \neg G & \neg F \wedge G & (F \wedge \neg G) \vee (\neg F \wedge G)\\
\hline
1&1&1&0&0&0&0&0 \\
\not{1}&\not{0}&\not{0}&\not{0}&\not{1}&\not{1}&\not{0}&\not{1} \\
\not{0}&\not{1}&\not{0}&\not{1}&\not{0}&\not{0}&\not{1}&\not{1} \\
0&0&1&1&1&0&0&0 \\
\hline
\end{array}$$
which shows that when considering the rows which make $F \leftrightarrow G$ a tautology, that $(F \wedge \neg G) \vee (\neg F \wedge G)$ is unsatisfiable.

Finally, we will show that if $(F \wedge \neg G) \vee (\neg F \wedge G)$ is unsatisfiable, then $F \equiv G$. 

$$\begin{array}{|l|l|l|l|l|l|l|}
\hline
F & G & (F \wedge \neg G) \vee (\neg F \wedge G) \\
\hline
1&1&0 \\
\not{1}&\not{0}&\not{1} \\
\not{0}&\not{1}&\not{1} \\
0&0&0 \\
\hline
\end{array}$$
From this we can observe that $F \vDash G$, because in any row for which $F$ is true, it is also true that $G$ is true. Similarly, we observe that $G \vDash F$ because in any row for which $G$ is true, it follows that $F$ is true. Therefore $F \equiv G$.

\textbf{\# 1.9}: The Cut rule states that from the formulas $F \rightarrow G$ and $G \rightarrow H$, we can derive $F \rightarrow H$. Verify this rule by giving a formal proof. \\
\textit{Solution}: We have the set of formulas $\mathcal{F} = \{F \rightarrow G, G \rightarrow H\}$. We want to show that $\mathcal{F} \vdash F \rightarrow H$. \\
\begin{center}\begin{tabular}{|l|l|}
\hline
\underline{Statement} & \underline{Justification} \\
\hline
1. $\mathcal{F} \vdash F \rightarrow G$ & Assumption \\
2. $\mathcal{F} \vdash G \rightarrow H$ & Assumption \\ 
3. $\mathcal{F} \cup \{F\} \vdash F$ & Assumption \\
4. $\mathcal{F} \cup \{F\} \vdash G$ & $\rightarrow$-elimination on lines 1 and 3 \\
5. $\mathcal{F} \cup \{F\} \vdash H$ & $\rightarrow$-elimination on lines on lines 2 and 4 \\
6. $\mathcal{F} \vdash F \rightarrow H$ & $\rightarrow$-introduction on line 5 \\
\hline
\end{tabular}\end{center}

\textbf{\# 1.10}: \begin{enumerate}[(a)]
\item Let $\leftrightarrow$-Symmetry be the following rule: \\
Premise: $\mathcal{F} \vdash (F \leftrightarrow G)$ \\
Conclusion: $\mathcal{F} \vdash (G \leftrightarrow F)$ \\
Verify this rule by giving a formal proof.

\item Give a formal proof demonstrating that $\{(F \leftrightarrow G)\} \vdash (\neg F \leftrightarrow \neg G)$. \\
\end{enumerate}
\textit{Solution}: First we write a proof for $(a)$. We let $\mathcal{F} \vdash \{(F \leftrightarrow G)\}$ and we will prove that $\mathcal{F} \vdash \{(G \leftrightarrow F)\}$. \\
\begin{center}\begin{tabular}{|l|l|}
\hline
Statement & Justification \\
\hline
1. $\mathcal{F} \vdash F \leftrightarrow G$ & Assumption \\
2. $\mathcal{F} \vdash F \rightarrow G$ & $\leftrightarrow$-definition \\
3. $\mathcal{F} \vdash G \rightarrow F$ & $\leftrightarrow$-definition \\
4. $\mathcal{F} \vdash G \leftrightarrow F$ & $\leftrightarrow$-definition on lines 3 and 2 \\
\hline
\end{tabular}\end{center}
Now we will write a proof for $(b)$. Let $\mathcal{F} = \{(F \leftrightarrow G)\}$. We want to prove that $\mathcal{F} \vdash (\neg F \leftrightarrow \neg G)$. (\textit{next page})\\
\begin{center}\begin{tabular}{|l|l|}
\hline
Statement & Justification \\
\hline
1. $\mathcal{F} \vdash (F \leftrightarrow G)$ & Assumption \\
2. $\mathcal{F} \vdash F \leftrightarrow G$ & $(,)$-elimination on line 1 \\
3. $\mathcal{F} \vdash F \rightarrow G$ & $\leftrightarrow$-definition on line 2 \\
4. $\mathcal{F} \cup \{F\} \vdash F$ & Assumption \\
5. $\mathcal{F} \cup \{F\} \vdash F \rightarrow G$ & Monotonicity on line 3 \\
6. $\mathcal{F} \cup \{F\} \vdash G$ & $\rightarrow$-elimination on lines 4 and 5 \\
7. $\mathcal{F} \cup \{F\} \vdash  \neg \neg G$ & Double negation on line 6 \\
8. $\mathcal{F} \vdash F \rightarrow \neg \neg G$ & $\rightarrow$-introduction on line 7 \\
9. $\mathcal{F} \vdash \neg F \vee \neg \neg G$ & $\rightarrow$-definition on line 8 \\
10. $\mathcal{F} \vdash \neg \neg G \vee \neg F$ & $\vee$-symmetry on line 9 \\
11. $\mathcal{F} \vdash \neg G \rightarrow \neg F$ & $\rightarrow$-definition on line 10 \\
12. $\mathcal{F} \vdash G \rightarrow F$ & $\leftrightarrow$-definition on line 2 \\
13. $\mathcal{F} \cup \{G\} \vdash G$ & Assumption \\
14. $\mathcal{F} \cup \{G\} \vdash F$ & $\rightarrow$-elimination on lines 12 and 13 \\
15. $\mathcal{F} \cup \{G\} \vdash \neg \neg F$ & Double negation on line 14 \\
16. $\mathcal{F} \vdash G \rightarrow \neg \neg F$ & $\rightarrow$-introduction on line 15 \\
17. $\mathcal{F} \vdash \neg G \vee \neg \neg F$ & $\rightarrow$-definition on line 16 \\
18. $\mathcal{F} \vdash \neg \neg F \vee \neg G$ & $\vee$-symmetry on line 17 \\
19. $\mathcal{F} \vdash \neg F \rightarrow \neg G$ & $\rightarrow$-definition on line 18 \\
20. $\mathcal{F} \vdash \neg F \leftrightarrow \neg G$ & $\leftrightarrow$-definition on lines 11 and 19 \\
21. $\mathcal{F} \vdash (\neg F \leftrightarrow \neg G)$ & $(,)$-introduction on line 20 \\
\hline
\end{tabular}\end{center}
\newpage
\textbf{\# 1.12}: Prove the rule of ``$\rightarrow$-contrapositive" with a formal proof: \\
Premise: $\mathcal{F} \vdash F \rightarrow G$ \\
Conclusion: $\mathcal{F} \vdash \neg G \rightarrow \neg F$ \\
\textit{Solution}: Let $\mathcal{F}=\{F \rightarrow G\}$. Now prove \\
\begin{center}\begin{tabular}{|l|l|}
\hline
\underline{Statement} & \underline{Justification} \\
\hline
1. $\mathcal{F} \vdash F \rightarrow G$ & Assumption \\
2. $\mathcal{F} \cup \{F\} \vdash F \rightarrow G$ & Monotonicity on line 1 \\
3. $\mathcal{F} \cup \{F\} \vdash F$ & Assumption \\
4. $\mathcal{F} \cup \{F\} \vdash G$ & $\rightarrow$-elimination on lines 2 and 3 \\
5. $\mathcal{F} \cup \{F\} \vdash \neg \neg G$ & Double negative of line 4 \\
6. $\mathcal{F} \vdash F \rightarrow \neg\neg G$ & $\rightarrow$-introduction on line 5 \\
7. $\mathcal{F} \vdash \neg F \vee \neg \neg G$ & $\rightarrow$-definition \\
8. $\mathcal{F} \vdash \neg \neg G \vee \neg F$ & $\vee$-symmetry \\
9. $\mathcal{F} \vdash \neg G \rightarrow \neg F$ & $\rightarrow$-definition \\
\hline
\end{tabular}\end{center}

\textbf{Problem A}: Write a formal proof that shows $\{P, P \rightarrow Q\} \vdash Q$. \\
\textit{Solution}: Let $\mathcal{F}=\{ P, P \rightarrow Q\}$. \\
\begin{center}\begin{tabular}{|l|l|}
\hline
Statement & Justification \\
\hline
1. $\mathcal{F} \vdash P$ & Assumption \\
2. $\mathcal{F} \vdash P \rightarrow Q$ & Assumption \\
3. $\mathcal{F} \vdash Q$ & $\rightarrow$-elimination using lines 1 and 2 \\
\hline
\end{tabular}\end{center}

\textbf{Problem B}: Write a formal proof showing $\{P \rightarrow Q, Q \rightarrow R, S \vee \neg R, P\} \vdash S$.  \\
\textit{Solution}: Let $\mathcal{F} = \{P \rightarrow Q, Q \rightarrow R, S \vee \neg R, P\}$. \\
\begin{center}
\begin{tabular}{|l|l|}
\hline
Statement & Justification \\
\hline
1. $\mathcal{F} \vdash P \rightarrow Q$ & Assumption \\
2. $\mathcal{F} \vdash Q \rightarrow R$ & Assumption \\
3. $\mathcal{F} \vdash S \vee \neg R$ & Assumption \\
4. $\mathcal{F} \vdash P$ & Assumption \\
5. $\mathcal{F} \vdash \neg R \vee S$ & $\vee$-symmetry on line 3 \\
6. $\mathcal{F} \vdash R \rightarrow S$ & $\rightarrow$-definition on line 5 \\
7. $\mathcal{F} \vdash Q$ & $\rightarrow$-elimination on lines 1 and 4 \\
8. $\mathcal{F} \vdash R$ & $\rightarrow$-elimination on lines 2 and 7 \\
9. $\mathcal{F} \vdash S$ & $\rightarrow$-elimination on lines 6 and 8 \\
\hline
\end{tabular}
\end{center}
\end{document}