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

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

\newcommand{\ForAll}[1]{\underset{#1}\forall}
\newcommand{\Exists}[1]{\underset{#1}\exists}

\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}}}
\newcommand{\nov}[1]{{\overline{#1}}}

\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2015.
Homework 4, given Nov 5, due Nov 12.}

\bigskip

\noindent
1.
Construct the sequent rules for disjunction and for implication in the goal
($\ylc \or$ and $\ylc \impl$)
by ``elimination'' (that is: by applying rules which are already known).

\bigskip

\noindent
2.
Construct the sequent rules for disjunction applied to a set in assumptions and in goal and
study the situations when the set is unary and when the set is empty.

\bigskip

\noindent
3.
Construct the sequent rule for equivalence in the goal ($\ylc \lequiv$) by ``elimination''.
\bigskip

\noindent
4.
Construct the sequent rule for ``Modus Tollens'' (from $P$ and $(\not Q) \impl (\not P)$ one obtains $\not P$) by ``elimination''.

\bigskip

\noindent
5.
Prove by sequent calculus:
$$ (A \or B) \impl C\ \ylc\ (A \impl C) \and (B \impl C).$$
and the reverse:
$$
(A \impl C) \and (B \impl C)
\ \ylc\ 
(A \or B) \impl C.
$$

\end{document}
