\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 2006.
Homework 2, given Oct 19, due Nov 9}

\bigskip

\noindent
1. 
Prove by using the truth table the equivalence:\\
$A \and (B \or C)\ \equiv\ (A \and B) \or (A \and C).$


\bigskip

\noindent
2. 
Give a natural style proof of the formula:\\
$((B \or C) \and (B \impl A) \and (C \impl D)) \impl (A \or D).$


\bigskip

\noindent
3. 
Construct the sequent proof-tree of the formula:\\
$((A \or B) \impl C)\ \impl\ ((A \impl C) \and (B \impl C)).$



\bigskip

\noindent
4. 
Formulate the sequent rule for the situation when the goal is a disjunction,
and prove it using the sequent rules of the ``small calculus''.



\end{document}
