\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 4, given Nov 23, due Nov 30}

\bigskip

\noindent
1. Find the sequent rule for the disjunction in the assumptions,
by using the equivalent transformation of a disjunction into a
formula containing only $\and$ and $\not$ and by using the rules
of the small calculus given in the lecture for formulae containing
only $\and$ and $\not.$

\bigskip

\noindent
2. Perform the same exercise for the case of implication in the conclusions.


\bigskip

\noindent
3. Perform the same exercise for the situation when the assumptions
include $\not \phi$ and $\phi \or \psi.$ (It is similar to the modus ponens
rule.)

\bigskip

\noindent
4. Prove that the following sequent rule is correct:

$$
\frac
{\Phi\ \ylc\ \phi}
{\Phi\ \ylc\ \phi \or \psi}
$$

\bigskip

\noindent
5. (Optional) 
Give an example of a concrete correct sequent for which the previous
sequent rule does not lead to a proof.


\end{document}
