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

\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}[1]{\underset{#1}{\forall}}
\newcommand{\allType}[2]{\underset{#2}{\underset{#1}{\forall}}}
\newcommand{\exi}[1]{\underset{#1}{\exists}}
\newcommand{\exiType}[2]{\underset{#2}{\underset{#1}{\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{\arrow}{\rightarrow}

\pagestyle{empty}

\begin{document}

{\bf Computational Logic, WS 2018.
Homework 10, given Jan. 14, due Jan. 21.}

\bigskip

\noindent
1.
Find the sequent rules for the existential quantifier by using the rules for the universal quantifier.

\bigskip

\noindent
2.
Study the inference methods for the formula
$\exiType{x \in D}{C[x]}P[x]$ in the assumptions and in the goal.

\bigskip

\noindent
3.
 Prove by sequent calculus in both directions.
$$(\exi{x} P[x])\impl Q\ \lequiv\ (\all{x} P[x]\impl Q) .$$

\end{document}

 
