\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 2007.
Homework 4, given Nov 8, due Nov 15.}

\bigskip

\noindent
1.
Show how to transform a sequent which has an universally quantified formula
in the goal, by moving the quantifier in front of the sequent (analoguous to
the transformation of the sequent which has an existentially quantified
formula in the assumptions, which was shown during the lecture).

\bigskip

\noindent
2.
For the inference rule for the sequents having an existentially quantified
formula in the goal, prove the equivalence of the two sequents using the
definition of the semantics.

\bigskip

\noindent
3.
For the inference rule for the sequents having an existentially quantified
formula in the goal, prove the equivalence of the two sequents using
the rule for the universal goal in the assumptions and the appropriate
propositional rules.

\bigskip

\noindent
4.
Prove by definition that
$$ P[a], \all_x (P[x] \impl P[f[x]])\ \elc\ P[f[f[a]]].$$

\end{document}
