\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}}}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2008.
Homework 7, given Dec 11, due Dec 18.}

\bigskip

\noindent
1.
Prove that the quantifier can be eliminated if there are no occurrences of the
quantified variable.

\bigskip

\noindent
2.
Prove that the part of the formula containing no occurrences of the
quantified variable can be moved out of the quantifier scope.

\bigskip

\noindent
3.
Investigate the possibility of splitting the universally and the existentially
quantified conjunctions and disjunctions.
(For instance find a counterexample for the split of the existentially
quantified conjunction.)
\bigskip

\end{document}