\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 3, given Oct 25, due Nov 8.}

\bigskip

\noindent
1.
For the example given in the student-script at page 49 (subsection 5.1),
evaluate the truth value $\langle P[x] \impl Q[f[x],a]\rangle^I_{x \leftarrow 2}.$

\bigskip

\noindent
2. 
Prove by definition that
$(\exi_x (P[x] \or Q[x])) \lequiv ((\exi_x P[x]) \or (\exi_x Q[x])).$

\bigskip

\noindent
3. 
Give a counterexample for 
$(\exi_x (P[x] \and Q[x])) \lequiv ((\exi_x P[x]) \and (\exi_x Q[x])).$

\bigskip

\noindent
4.
Prove by definition that if $\all_x \exi_y P[x, y]$ is satisfiable,
then $\all_x P[x, f[x]]$ is satisfiable.

\bigskip

\noindent
5.
Transform the following formula into Skolem normal form:\\
$\all_x \all_y ((\exi_z P[x, y, z]) \and ((\exi_u Q[x, u]) \impl \exi_v Q[y, v])).$




\end{document}
