\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 6, given Dec 3, due Dec 10.}

\bigskip

\noindent
1.
Show the equivalence of the sequents
$\ \ \Phi, \not \varphi\ \ \ylc\ \ \varphi, \Psi\ \ $
and $\ \ \Phi \ \ylc\ \ \varphi, \Psi.$

\bigskip

\noindent
2.
Find the transformations of negated disjunction, negated implication,
and negated equivalence.

\bigskip

\noindent
3.
Construct the unique goal sequent calculus proof of:
$$(A \and B) \impl C\ \ \ylc\ \ (A \impl C) \or (B \impl C).$$
\bigskip

\noindent
4.
Construct the unique goal sequent calculus proof of:
$$(A \or B) \impl C\ \ \ylc\ \ (A \impl C) \and (B \impl C).$$

\bigskip

\noindent
5.
Evaluate the truth value of the formula
$$((\all_x (P[x] \impl P[f[x]])) \and P[a]) \impl P[f[f[a]]]$$
over the interpretation
$I$ having the domain $D = \{0, 1\}$ and $a_I = 0,$
$f_I[0] = 1,$ $f_I[1] = 0,$ $P_I[0] = \false,$ and $P_I[1] = \true.$

\bigskip

\noindent
6. (Optional)
Formulate the induction principle for formulae in first order predicate logic.


\end{document}