\documentclass[11pt]{article}

\usepackage{homework,amssymb,eufrak,bussproofs,mylogic}

\EnableBpAbbreviations

\begin{document}

\soltitle{11}{Thursday, October 6}

\begin{list1} 
  
% \item[2.\hfill]
% \begin{list2}
% \item[(i)] \ \\
% \begin{prooftree}
% \AXM{[\fa x (\ph(x) \limplies \psi(x))]_2}
% \UIM{\ph(x) \limplies \psi(x)}
% \AXM{[\fa x \ph(x) ]_1}
% \UIM{\ph(x)}
% \BIM{\psi(x)}
% \UIM{\fa x \psi(x)}
% \RL{1}
% \UIM{\fa x \ph(x) \limplies \fa x \ph(x)}
% \RL{2}
% \UIM{(\fa x (\ph(x) \limplies \psi(x)) \limplies
% (\fa x \ph(x) \limplies \fa x \ph(x))}
% \end{prooftree}
% \item[(ii)] \ \\
% \begin{prooftree}
% \AXM{[\fa x \ph(x)]_2}
% \UIM{\ph(x)}
% \AXM{[\fa x \lnot \ph(x)]_1}
% \UIM{\lnot \ph(x)}
% \BIM{\bot}
% \RL{1}
% \UIM{\lnot \fa x \lnot \ph(x)}
% \RL{2}
% \UIM{\fa x \ph(x) \limplies \lnot \fa x \lnot \ph(x)}
% \end{prooftree}
% \item[(vi)] Forwards direction:
% \begin{prooftree}
% \AXM{\fa x (\ph(x) \land \psi(x))}
% \UIM{\ph(x) \land \psi(x)}
% \UIM{\ph(x)}
% \UIM{\fa x \ph(x)}
% \AXM{\fa x (\ph(x) \land \psi(x))}
% \UIM{\ph(x) \land \psi(x)}
% \UIM{\psi(x)}
% \UIM{\fa x \psi(x)}
% \BIM{\fa x \ph(x) \land \fa x \psi(x)}
% \end{prooftree}
% Backwards direction:
% \begin{prooftree}
% \AXM{\fa x \ph(x) \land \fa x \psi(x)}
% \UIM{\fa x \ph(x)}
% \UIM{\ph(x)}
% \AXM{\fa x \ph(x) \land \fa x \psi(x)}
% \UIM{\fa x \psi(x)}
% \UIM{\psi(x)}
% \BIM{\ph(x) \land \psi(x)}
% \UIM{\fa x (\ph(x) \land \psi(x))}
% % \RL{1}
% % \BIM{\fa x (\ph(x) \land \psi(x)) \liff (\fa x \ph(x) \land \fa x
% %   \psi(x))}
% \end{prooftree}
% \end{list2}

\item[3.\hfill] The first derivation is used in the second one, at the
  position marked * (there wasn't enough room to write it in).
\begin{list2}
\item \ 

\begin{prooftree}
\AXM{[p]_1}
\AXM{[p \liff \lnot p]_3}
\BIM{\lnot p}
\AXM{[p]_1}
\BIM{\bot}
\RL{1}
\UIM{\lnot p}
\AXM{[p \liff \lnot p]_3}
\BIM{p}
\AXM{[p]_2}
\AXM{[p \liff \lnot p]_3}
\BIM{\lnot p}
\AXM{[p]_2}
\BIM{\bot}
\RL{2}
\UIM{\lnot p}
\BIM{\bot}
\RL{3}
\UIM{\lnot (p \liff \lnot p)}
\end{prooftree}
\item
\begin{prooftree}
\AXM{[\ex y \fa x (S(y,x) \liff \lnot S(x,x))]_2}
\AXM{[\fa x (S(y,x) \liff \lnot S(x,x))]_1}
\UIM{S(y,y) \liff \lnot S(y,y)}
\RL{*}
\UIM{\bot}
\RL{1}
\BIM{\bot}
\RL{2}
\UIM{\lnot \ex y \fa x (S(y,x) \liff \lnot S(x,x))}
\end{prooftree}
\end{list2}

\item[4.\hfill] Forwards direction:
\begin{prooftree}
\AXM{[\ex x (\ph(x) \land \psi)]_2}
\AXM{[\ph(x) \land \psi]_1}
\UIM{\ph(x)}
\UIM{\ex x \ph(x)}
\AXM{[\ph(x) \land \psi]_1}
\UIM{\psi}
\BIM{\ex x \ph(x) \land \psi}
\RL{1}
\BIM{\ex x \ph(x) \land \psi}
\RL{2}
\UIM{\ex x (\ph(x) \land \psi) \limplies \ex x \ph(x) \land \psi}
\end{prooftree}

Backwards direction:
\begin{prooftree}
\AXM{[\ex x \ph(x) \land \psi]_2}
\UIM{\ex x \ph(x)}
\AXM{[\ph(x)]_1}
\AXM{[\ex x \ph(x) \land \psi]_2}
\UIM{\psi}
\BIM{\ph(x) \land \psi}
\UIM{\ex x (\ph(x) \land \psi)}
\RL{1}
\BIM{\ex x (\ph(x) \land \psi)}
\RL{2}
\UIM{\ex x \ph(x) \land \psi \limplies \ex x (\ph(x) \land \psi)}
\end{prooftree}

\item[7.\hfill]
Forwards direction:
\begin{prooftree}
\AXM{[\lnot \ex x \ph(x)]_2}
\AXM{[\ph(x)]_1}
\UIM{\ex x \ph(x)}
\BIM{\bot}
\RL{1}
\UIM{\lnot \ph(x)}
\UIM{\fa x \lnot \ph(x)}
\RL{2}
\UIM{\lnot \ex x \ph(x) \limplies \fa x \lnot \ph(x)}
\end{prooftree}

Backwards direction:
\begin{prooftree}
\AXM{[\ex x \ph(x)]_2}
\AXM{[\ph(x)]_1}
\AXM{[\fa x \lnot \ph(x)]_3}
\UIM{\lnot \ph(x)}
\BIM{\bot}
\RL{1}
\BIM{\bot}
\RL{2}
\UIM{\lnot \ex x \ph(x)}
\RL{3}
\UIM{\fa x \lnot \ph(x) \limplies \lnot \ex x \ph(x)}
\end{prooftree}

\item[9.\hfill] \ 

\begin{prooftree}
\AXM{\fa x L(x,b)}
\UIM{L(b,b)}
\AXM{\fa x (L(b,x) \limplies x = m)}
\UIM{L(b,b) \limplies b = m}
\BIM{b=m}
\end{prooftree}

\item[10.\hfill]
For $I_2$:
\begin{prooftree}
\AXM{\fa {x,y,z}(x = y \land z = y \limplies x = z)}
\UIM{u = u \land v = u \limplies u = v}
\AXM{\fa x (x = x)}
\UIM{u = u}
\AXM{[v = u]_1}
\BIM{u = u \land v = u}
\BIM{u = v}
\RL{1}
\UIM{v = u \limplies u = v}
\UIM{\fa {v, u} (v = u \limplies u = v)}
\end{prooftree}
In this derivation, I've combined instances of the $\forall$ rules. On the
top left, note that I am substituting $u$, $u$, and $v$ for $x$, $y$,
and $z$ respectively.

For $I_3$, use $I_2$:
\begin{prooftree}
\AXM{\fa {x,y,z} (x = y \land z = y \limplies x = z}
\AXM{[x = y \land y = z]_1}
\UIM{x = y}
\AXM{[x = y \land y = z]_1}
\UIM{y = z}
\RL{*}
\UIM{z = y}
\BIM{x = y \land z = y}
\BIM{x = z}
\RL{1}
\UIM{x = y \land y = z \limplies x = z}
\UIM{\fa {x,y,z} (x = y \land y = z \limplies x = z)}
\end{prooftree}
Here the derivation of $I_2$ is used at *.

\item[13.\hfill] \ 

\begin{prooftree}
\AXM{[\ph]_1}
\UIM{\ph \lor \lnot \ph}
\AXM{[\lnot (\ph \lor \lnot \ph)]_2}
\BIM{\bot}
\RL{1}
\UIM{\lnot \ph}
\UIM{\ph \lor \lnot \ph}
\AXM{[\lnot (\ph \lor \lnot \ph)]_2}
\BIM{\bot}
\RL{2 RAA}
\UIM{\ph \lor \lnot \ph}
\end{prooftree}

\end{list1}

\end{document}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: