\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\\
Fall Semester \os{1999}\\[16pt]

Assignment \#4 -- Propositional Logic: Hilbert Systems\\
\large
Due { \os{11}:\os{00}am}, Wednesday October \os{6}, \os{1999}
\end{center}

\vspace{0.25in}


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

Prove each of the following derived Hilbert rules sound by showing that
when you have a proof of each of the premises (the formulas on the top) you
can construct a proof of the conclusion (the formula on the bottom) without
using the rule. 


\begin{enumerate}

\item In class, we gave a derivation justifying the following rule which used the
deduction rule. Please give a derivation that uses only the pure Hilbert system
(consisting of the three axioms and {\it modus ponens}).

The Transitivity Rule: 
$$
\infer[]{A\imp C}{A\imp B & B\imp C}
$$

\end{enumerate}


For the rest, you may use any of the derived rules covered in class, and any of the
rules you have already proved. You will find the framework of most of these proofs in
section 2.9 of the text, but in a different style than used in class.


\begin{enumerate}
\item[2.] The Inverse Contrapositive Rule: 
$$
\infer[]{(\neg B)\imp(\neg A)}{A\imp B}
$$

\item[3.] The Inverse Double Negation Rule:
$$
\infer[]{\neg\neg A}{A}
$$

\item[4.] The And Rule:
$$
\infer[]{A\land B}{A & B} \quad [\mbox{really} \quad \infer[]{\neg(A\imp(\neg B))}{A
& B}]
$$

\item[5.] The Commutativity of Or Rule:
$$
\infer[]{A\lor B}{B\lor A} \quad [\mbox{really} \quad \infer[]{((\neg A)\imp 
B)}{((\neg B)\imp A)}]
$$


\end{enumerate}

\end{document}
