\documentclass[12pt]{article}
\usepackage{amsmath}
\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}}}
\newcommand{\ForAll}[1]{\underset{#1}\forall}
\newcommand{\Exists}[1]{\underset{#1}\exists}

\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2016.
Homework 8, given Dec 15, due Jan 12.}

\bigskip

\noindent
1.
Develop the sequent rules for existential quantified formulae in
the goal and in the assumptions, using the rules for universally quantified formulae.

\bigskip

\noindent
2.
Develop the sequent rules for the quantified conditional goal (universal, existential) using
the other rules.

\bigskip

\noindent
3. Prove by sequent calculus:
$(\Exists{x} P[x]) \impl Q\ \equiv\ \ForAll{x}(P[x] \impl Q)$.



\end{document}