\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{2001}\\[16pt]

Assignment \#7 -- Predicate Logic: Proof Theory\\
\large
Due { \os{11}:\os{00}am}, Friday, April \os{20}, \os{2001}
\end{center}

\vspace{0.25in}


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

\begin{enumerate}

\item Give Natural Deduction proofs of each of the following formulas (brackets are
used in place of parentheses in some formulas to make the structure clearer):
\begin{enumerate}

\item $\exists x [\forall y (p(x,y))] \imp \forall y [\exists x (p(x,y))]$

\item $\exists x[p(x) \imp q(x)] \imp [\forall x(p(x)) \imp \exists x (q(x))]$

\item Prove that any boletus is poisonous. That is, from open assumptions:
\begin{itemize}
\item $\forall x (f(x) \imp [m(x)\lor t(x)])$
\item $\forall x (b(x) \imp f(x))$
\item $\forall x ([t(x) \lor pp(x)] \imp  p(x))$
\item $\forall x (b(x) \imp \neg m(x))$
\end{itemize}
prove the conclusion $\forall x (b(x) \imp p(x))$


\item (extra credit) $[\forall x(p(x)) \imp \exists x (q(x))] \imp  \exists x[p(x)
\imp q(x)]$

\end{enumerate}


\item Give Gentzen Sequent Calculus proofs for each of the conclusions in the last
problem, including the extra credit (which is not extra credit in this problem).

\item Give Resolution Refutaion proofs for each of the conclusions in the first
problem, including the extra credit (which is not extra credit in this problem).

\end{enumerate}

\end{document}
