\documentclass[12pt]{article}

\usepackage{proof}
\usepackage{fullpage}

\newcommand\os[1] {$\mit{#1}$}
%\newcommand\os[1]{#1}
 
\newcommand\imp\Rightarrow

%\input{qobitree}
\pagestyle{empty}

\begin{document}

\begin{center}
\large 
%\vspace*{-1.5cm}
Harvey Mudd College\\
Computer Science \os{80}\\
Logic for Computer Science\\
Spring Semester \os{2002}\\[16pt]

Assignment \#3 -- Propositional (mostly) Logic: Natural Deduction\\
\large
Due { \os{5}:\os{00}pm}, Friday March \os{1}, \os{2002}
\end{center}

\vspace{0.25in}


\newcommand{\G}{\Gamma}
\newcommand{\D}{\Delta}
\newcommand{\lra}{\longrightarrow}


\noindent{\bf(A)} Provide an encoding of the proof given in class that there exist two irrational numbers, $a$
and
$b$, such that $a^b$ is rational, as a natural deduction proof. While we are focused on propositional logic,
this uses a few features of first-order logic. You will need two additional rules from first-order natural
deduction:

$$
\infer[\forall_E]{\phi(t)}{\forall x (\phi(x))}
\qquad
\infer[\exists_I]{\exists x(\phi(x))}{\phi(x)}
$$

The first rule says that if some property holds for some value of $x$, then it certainly holds for any given term $t$ you substitute for $x$. For example, if we have the assumption $\forall x (\forall y ((ra(x) \land (x = y))\imp ra(y)))$ which says that if a number, $y$, is equal to a rational number, it is rational, we can use this to get the specific application of this assumption to two particular numbers used in the proof, as in:

$$
\infer[\forall_E]
    {((ra(2) \land (2 = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}}))\imp ra((\sqrt{2}^{\sqrt{2}})^{\sqrt{2}})}
    {\infer[\forall_E]
         {\forall y ((ra(2) \land (2 = y))\imp ra(y))}
         {\forall x (\forall y ((ra(x) \land (x = y))\imp ra(y)))}
    }
$$

The second rule says that if you have a specific value that a property holds for, then you certainly know that there is some value the property holds for. This will be useful in reaching the desired conclusion in each of the case arguments. For example, one of the cases would terminate with:

$$
\deduce{
\infer[\exists_I]
     {\exists x(\exists y ((ir(x) \land ir(y)) \land ra(x^y)))}
     {\infer[\exists_I]
          {\exists y ((ir({\sqrt{2}}) \land ir(y)) \land ra({\sqrt{2}}^y))}
          {(ir({\sqrt{2}}) \land ir({\sqrt{2}})) \land ra({\sqrt{2}}^{\sqrt{2}})}
     }}{\vdots}
$$


\vspace{.25in}
You may use any true equality or other obviously true property of arithmetic as an undischarged assumption in the proof.
For example, that $\forall x(ir(x) \equiv (\neg ra(x)))$. Unlike in the natural language proof, it should be
clear at the end exactly how what properties of arithmetic (like the one above about equality preserving
rationality)  are being used as assumptions.

\newpage
\noindent{\bf(B)} Give Natural Deduction proofs of each of the following formulas. That is,
give a Natural Deduction proof tree with the given formula as its conclusion,
and no undischarged assumptions. (Note, brackets are used in place of parentheses in
some formulas to make the structure clearer). 

Some of these proofs will require classical reasoning. In some cases cases it will be easiest using $RAA$. In others you may find that assuming $\phi\lor(\neg\phi)$ for some $\phi$ is easiest. If you choose to use the latter, then in the first place you do it you must expand the proof of that formula. For other uses you may just elide the proof by writing $$\phi\stackrel{\vdots}{\lor}(\neg\phi)$$

\vspace{.5in}

\begin{enumerate}

\item $[(p \land q) \imp r] \equiv [p\imp(q\imp r)]$

\item $(p \lor q) \imp [((p\imp r)\land (q\imp r))\imp r]$

\item $([(p\imp q)\imp p]\imp p)$

\item $(p\imp r)\equiv (\neg p \lor r)$


\item $(p\imp r)\equiv \neg(p\land \neg r)$


\end{enumerate}


\noindent{\bf(C)} In class we discussed that the	``triple-xor'' technique for exchanging
the values of two program variables is sound if and only if the formula 
$$((\Delta_{a_1} \land \ (\Delta_{b_1} \land \Delta_{a_2}))\imp ((a_2\equiv b_o)\land(b_1\equiv a)))$$
is valid (and provable), where $\Delta_{a_1}$,  $\Delta_{b_1}$, and $\Delta_{a_2}$ are the formulas
``defining'' the values of the intermediate variables $a_1$, $b_1$, and $a_2$, given respectively as:
\begin{eqnarray*}
(a_1&\equiv&((a_o\lor b_0)\land(\neg(a_0\land b_0)))) \\
(b_1&\equiv&((a_1\lor b_0)\land(\neg(a_1\land b_0)))) \\
(a_2&\equiv&((a_1\lor b_1)\land(\neg(a_1\land b_1))))
\end{eqnarray*}
Here I have expanded out the definition of exclusive-or into primative connectives.

In constructing the proof of this formula in Natural Deduction, it is necessary to produce a sub-proof with
the atomic formula $b_1$ as its conclusion and the formulas $a_0$, $\Delta_{a_1}$,  $\Delta_{b_1}$, and
$\Delta_{a_2}$ as open assumptions. Construct this sub-proof. As above, this proof requires classical
reasoning, and you may use either $RAA$ or an elided proof of a formula $\phi\lor \neg\phi$, as you prefer.
(Indeed, I found one to be useful in one spot, and the other in another.)
\end{document}
