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

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\newcommand{\ForAll}[1]{\underset{#1}\forall}
\newcommand{\Exists}[1]{\underset{#1}\exists}

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

\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2012.
Homework 4, given Nov 15, due Nov 22.}

\bigskip

\noindent
1.
Evaluate the truth of the formula
$(P[a]\and(\ForAll{x} (P[x]\impl P[f[x]])))\impl P[f[f[a]]] $
under the interpretation $I$:\\
~~~ $D = \{0,1,2\};$\\
~~~ $a_I = 1;$\\
~~~ $f_I[0]=2,\ f_I[1]=2,\ f_I[2]=0;$\\
~~~ $P_I[0]=\false,\ P_I[1]=\true,\ P_I[2]=\false.$

\bigskip

\noindent
2.
Find counterexamples $\varphi,\psi$ which disprove the false equivalences:
$$(\Exists{x} \varphi) \and (\Exists{x} \psi) \ \equiv\ \Exists{x} (\varphi \and \psi),$$
$$(\ForAll{x} \varphi) \or (\ForAll{x} \psi) \ \equiv\ \ForAll{x} (\varphi \or \psi).$$

\bigskip

\noindent
3.
Prove the following equivalence by reducing both sides to CNF:
$$(\ForAll{x} P[x]) \impl Q\ \equiv\ \Exists{x} (P[x] \impl Q).$$

\bigskip

\noindent
4.
Prove that if the formula $\Exists{x}P[x]$ is satisfiable, then the formula $P[a]$ is also satisfiable.

\bigskip

\noindent
5.
Prove that if the formula $\ForAll{x}P[x, f[x]]$ is satisfiable, then the formula $\ForAll{x}\Exists{y}P[x, y]$ is also satisfiable.

\end{document}