\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 \#5 -- Propositional Logic: Gentzen Sequent Calculus\\
\large
Due { \os{11}:\os{00}am}, Monday November \os{18}, \os{2002}
\end{center}

\vspace{0.25in}


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

\begin{enumerate}

\item Give Classical Gentzen Sequent Calculus 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 $[(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}


\item Consider the the intuitionistic sequent calculus in which the
right hand side of the sequent is restricted to a single fomula (Greek letters denote
sets of formulas, roman letters denote individual formulas):

$$\small
\infer[id]{\G,A\lra A}{} \qquad \infer[\bot]{\G,\bot\lra A}{}
$$

$$\small
\infer[\land_L]{\G,A\land B\lra C}{\G,A,B\lra C}\qquad
\infer[\land_R]{\G\lra A\land B}{\G\lra A & \G\lra B}
$$

$$\small
\infer[\lor_L]{\G,A\lor B\lra C}{\G, A\lra C & \G,B\lra C}\qquad
\infer[\lor_{R_1}]{\G\lra A\lor B}{\G\lra A}\qquad 
\infer[\lor_{R_2}]{\G\lra A\lor B}{\G\lra B}
$$

$$\small
\infer[\imp_L]{\G,A\imp B\lra C}{\G\lra A & \G,B\lra C}\qquad
\infer[\imp_R]{\G\lra A\imp B}{\G,A\lra B}
$$

$$\small
\infer[\neg_L]{\G, \neg A\lra C}{\G\lra A}\qquad
\infer[\neg_R]{\G\lra \neg A}{\G,A\lra \bot} 
$$

Prove that this version of the sequent calculus is sound (for the fragment of
propositional calculus it covers) by showing that whenever there is a derivation of a
sequent $\G\lra A$ in this system, then there is a Natural Deduction proof of the
formula $A$ in which the open assumptions (non-discharged leaves) form a set
$\D\subseteq\G$. 

(Hint: Use complete induction on the height of the sequent calculus proof.)


\end{enumerate}

\end{document}
