\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 2017.
Homework 5, given Nov. 23, due Nov 30.}

\bigskip

\noindent
1.
Bring into prenex NF, CNF, and Skolem normal form:
$$ (\all_x P[x]) \impl (\exi_x Q[x])$$

\bigskip

\noindent
2. 
Bring into prenex NF, CNF, and Skolem normal form:
$$\all_x \all_y((\exi_z (P[x,z] \and P[y,z])) \impl \exi_y Q[x,y,u])
$$

\bigskip

\noindent
3. 
Construct the Herbrand universe (partially -- $H_0, H_1, H_2$) for the formula:
$$\all_x (P[x,a] \impl P[g[a,a],x])
$$

\bigskip

\noindent
4. Are these unifiable ?
$$ Q[f[a],g[x]],\ Q[y,y]$$

\bigskip

\end{document}

 
