\documentclass[12pt]{article}
\usepackage{amsfonts}
 
\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\newcommand{\ovneg}[1]{{\overline{#1}}}
\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 Automated Reasoning, WS 2017.
Homework 3, given Dec 6, due Jan 10}

\bigskip

\bigskip

\noindent
1.
Discover the sequent rules for the existential quantifier,
by using the rules for the universal quantifier, the deMorgan equivalences,
and the rules for negation.

\bigskip

\noindent
2.
Construct the sequent calculus proofs for:
$$ ((\all_x P[x]) \impl Q) \lequiv (\exi_x (P[x] \impl Q)) $$
and
$$ ((\exi_x P[x]) \impl Q) \lequiv (\all_x (P[x] \impl Q)) $$

\end{document}
