\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 2008.
Homework 8, given Dec 18, due Jan 8.}

\bigskip

We denote by $t$ a ground term, by $P$ a predicate symbol,
and by $f$ a function symbol.
Prove the following using the definition of the semantics in first order
predicate logic:

\noindent
1.
$ P[t]\ \elc\ \exi_x P[x].$

\bigskip

\noindent
2.
$ P[t]\ \and\ \all_x \not P[x]$ is unsatisfiable.

\bigskip

\noindent
3.
$ \all_x P[x]\ \elc\ \all_{y, z} P[f[y, z]].$


\bigskip

\end{document}