\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 2007.
Homework 7, given Dec 13, due Jan 10.}

\bigskip

\noindent
1.
In the usual theory of natural numbers,
find a contradiction introduced by the definition:
$$\all_{x, y} P[x] \lequiv (x + y = 0).$$
\bigskip

\noindent
2.
In the theory of real numbers, consider the predicate $P$ defined by:
$$\all_{x, y} P[x, y] \lequiv \exi_t (x = \sin{t} \and y = \cos{t}).$$
Study the possibility of defining a function $f$ by:
$$\all_{x, y} f[x] = y \lequiv P[x, y],$$
or an alternative formula in which $x$ and/or $y$ must obey some condition
or/and the equivalence is replaced by an implication.

\bigskip

\noindent
3.
Reformulate the verification condition
$$\all_{x:I_F:\not Q[x]} \all_y (O_F[R[x], y] \impl I_C[x, y])$$
such that $R[x]$ is not used, but the specification of $R$.

\bigskip

\noindent
4.
Reformulate the verification condition
$$\all_{x:I_F:\not Q[x]} \all_y (O_F[R[x], y] \impl O_F[x, C[x,y]])$$
such that $R[x]$ and $C[x, y]$ are not used, but the specifications
of $R$ and $C$.

\bigskip

\end{document}
