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

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

\newcommand{\arrow}{\rightarrow}
\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{\ForAll}[1]{\underset{#1}\forall}
\newcommand{\Exists}[1]{\underset{#1}\exists}

\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2016.
Homework 7, given Nov 24, due Dec 1.}

\bigskip

\noindent
1. Compute the truth value:
$\langle P[x] \impl P[f[x]] \rangle^I_{\{x \arrow 1\}}$
with respect to the interpretation

$I:\ \{
D_I = \{0, 1\},\ 
a_I = 1,\ 
f_I = \{0 \arrow 1, 1 \arrow 0\},\ 
P_I = \{0 \arrow T, 1 \arrow F\}\}$.

\bigskip

\noindent
2. Prove by definition
$\not \Exists{x} \varphi\ \equiv\ \ForAll{x} \not \varphi$.

\bigskip

\noindent
3. Show by a counterexample that $\Exists{x}(\varphi \and \psi)$ is not
equivalent to $(\Exists{x} \varphi) \and (\Exists{x} \psi)$.

\bigskip

\noindent
4. Prove by reducing to normal form:
$(\Exists{x} P[x]) \impl Q\ \equiv\ \ForAll{x}(P[x] \impl Q)$.

\bigskip

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

\end{document}