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

Assignment \#7 -- Predicate Logic: Proof Theory\\
\large
Due { \os{5}:\os{00}pm}, Friday, December \os{13}, \os{2002}
\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).

\end{enumerate}

\end{document}
