\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}}
\newcommand{\arrow}{\rightarrow}

\pagestyle{empty}

\begin{document}

{\bf Mathematical Logic, WS 2018.
Homework 8, given Jan 8, due Jan. 15.}

\bigskip

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

\bigskip

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

\bigskip

\noindent
3.
Prove by sequent calculus the two sequents corresponding to the equivalence:
$$\exi_x(P[x]\impl Q)\ \equiv\ (\all_x P[x])\impl Q .$$

\bigskip

\noindent
4.
Using the formulae:
$ S[0] = 0$ and
$ \all_n (S[n+1] = S[n] + n + 1),$
compute $S[3]$ by substitution and replacement.

\bigskip

\end{document}

 
