\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}}}
\newcommand{\nov}[1]{{\overline #1}}
\newcommand{\arrow}{\rightarrow}

\pagestyle{empty}

\begin{document}

{\bf Mathematical Logic, WS 2018.
Homework 7, given Dec. 11, due Jan 8.}

\bigskip

\noindent
1.
Prove by reduction to normal form:
$$\exi_x(P[x]\impl Q)\ \equiv\ (\all_x P[x])\impl Q .$$

\bigskip

\noindent
2.
Prove that if the formula $P[a]$ is satisfiable, then the formula
$\exi_x P[x]$ is also satisfiable.

\bigskip

\noindent
3.
Prove that if the formula $\all_x \exi_y P[x,y]$ is satisfiable, then the formula
$\all_x P[x,f[x]]$ is also satisfiable.

\bigskip

\noindent
4.
Show by refutation, normal form, and resolution that $G$ is a semantical logical consequence of $F_1, F_2, F_3$:

$F_1:\ \ \all_x(Q[x] \impl \neg P[x])$

$F_2:\ \ \all_x((R[x] \and \neg Q[x]) \impl \exi_y(T[x,y] \and S[y]))$

$F_3:\ \ \exi_x(P[x] \and \all_y(T[x,y] \impl P[y]) \and R[x])$

$G:\ \ \exi_x(S[x] \and P[x]).$
\bigskip

\end{document}

 
