\documentstyle[12pt]{article}

\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}
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2004.
Homework 4, given Oct 28, due Nov 04}

\bigskip

\noindent
1. Consider the sequent calculus definded by the axioms:
$$ {\cal A} = \{ \Phi \ylc \Psi\ |\ \Phi \intersect \Psi \ne \emptyset \}, $$

\noindent
and by the rules:
$$
\frac
{\Phi, \varphi_1, \varphi_2 \ylc \Psi}
{\Phi, \varphi_1 \and \varphi_2 \ylc \Psi}
\ {\footnotesize (\and\ylc)}
\ \ \ \ \ \ 
\frac
{\Phi \ylc \Psi, \varphi_1\ \ \ \Phi \ylc \Psi, \varphi_2}
{\Phi \ylc \Psi, \varphi_1 \and \varphi_2}
\ (\ylc\and)
$$

$$
\frac
{\Phi \ylc \Psi, \varphi}
{\Phi, \neg \varphi \ylc \Psi}
\ (\neg\ylc)
\ \ \ \ \ \ 
\frac
{\Phi, \psi \ylc \Psi}
{\Phi \ylc \Psi, \neg \psi}
\ (\ylc\neg)
$$

$$
\frac
{\Phi, \varphi' \ylc \Psi}
{\Phi, \varphi \ylc \Psi}
\ {{\rm if}}\ \varphi \equiv \varphi' \ (\equiv\ylc)
\ \ \ \ \ \ 
\frac
{\Phi \ylc \Psi, \psi' }
{\Phi \ylc \Psi, \psi }
\ {{\rm if}}\ \psi \equiv \psi' \ (\ylc\equiv)
$$
\bigskip


\noindent
Using this calculus, prove the correctness of the following sequent rules
(that is ``eliminate'' them, by showing how they can be simulated by the rules
of the above calculus):

$$
(a)\ \ \frac
{\Phi, \psi_1 \ylc \Psi, \psi_2}
{\Phi \ylc \Psi, \psi_1 \impl \psi_2}
$$

$$
(b)\ \ \frac
{\Phi, \psi_1 \ylc \Psi, \psi_2\ \ \ \ \Phi, \psi_2 \ylc \Psi, \psi_1}
{\Phi \ylc \Psi, \psi_1 \lequiv \psi_2}
$$

You may use the rule for ``$\impl$'' when eliminating the rule for
``$\lequiv$''.

\bigskip

\noindent
2. Using the same calculus as above, eliminate the rules:

$$
(c)\ \ \frac
{\Phi, \varphi_1, \varphi_2 \ylc \Psi}
{\Phi, \varphi_1, (\not \varphi_1) \or \varphi_2 \ylc \Psi}
$$

$$
(d)\ \ \frac
{\Phi, \not \psi_1\ \ylc\ \Psi, \psi_2}
{\Phi\ \ylc\ \Psi, \psi_1 \or \psi_2}
$$



\bigskip

\noindent
3. Write the following definition in the standard prefix syntax
of predicate logic:

A function $f$ is continuous if and only if:
$$ \all_{\epsilon > 0}\ \exi_{\delta > 0}\ \all_y\ 
   (|y - x| < \delta\ \impl\ |f(y) - f(x)| < \epsilon) $$

\bigskip

\noindent
4. Construct an interpretation for the formula:

$$((\all_x P(x) \impl P(f(x))) \and P(a)) \impl P(f(f(a))).$$


\bigskip

\noindent
5. Find an example of subformulae $\phi$ and $\psi$ for which the following
equivalence does not hold:
$$ \forall_x (\phi \or \psi)\ \equiv\ (\forall_x \phi) \or (\forall_x \psi). $$




\end{document}