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

\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2012.
Homework 5, given Jan 10, due Jan 17.}

\bigskip

\noindent
1.
Find out the sequent rule for disjunction in the goal, using the $\not\and$ sequent calculus.

\bigskip

\noindent
2.
Find out the sequent rule for implication in the goal, using the $\not\and$ sequent calculus.

\bigskip

\noindent
3.
Prove by propositional sequent calculus:
$(A \impl C)\or (B \impl C)\ \ylc\ (A \and B) \impl C$.
Check if this proof must be modified for single-goal sequent calculus.

\bigskip

\noindent
4. Prove by predicate logic sequent calculus:
$(\exi_x P[x]) \impl Q\ \ylc \all_x (P[x] \impl Q)$.
Check if this proof must be modified for single-goal sequent calculus.

\bigskip

\noindent
5. Optional: Prove by propositional sequent calculus the equivalence between
the formulae\\
 $(A \impl C)\and (B \impl C)$ and $(A \or B) \impl C$.
Check if these proofs must be modified for single-goal sequent calculus.

\end{document}