\documentclass[12pt]{article}
\usepackage{amsfonts}

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\renewcommand{\and}{\wedge}
\renewcommand{\or}{\vee}
\newcommand{\impl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow} %equivalence as logical connective
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
%\equiv is already defined for === semantic equivalence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
\newcommand{\true}{{\mathbb{T}}}
\newcommand{\false}{{\mathbb{F}}}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2007.
Homework 2, given Oct 18, due Oct 25}

\bigskip

\noindent
1.
Prove the correctness and the reversibility of the sequent rule for negation in the
conclusions.

\bigskip

\noindent
2. 
Prove the correctness and the reversibility of the sequent rule for conjunction in
the assumptions.

\bigskip

\noindent
3. 
Find the sequent rule for disjunction in the assumptions, by using the rules of
the small calculus for negation and conjunction.

\bigskip

\noindent
4.
Find the sequent rule for ``modus tollens'' (the assumptions contain an implication
and the negation of the conclusion of the implication), by using the rules
for negation, conjunction, and disjunction.

\bigskip

\noindent
5.
Using unique--goal sequent calculus, prove the formula:
$$ ((A \impl C) \or (B \impl C))\ \impl\ ((A \and B) \impl C). $$ 




\end{document}
