\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 2016.
Homework 3, given Oct 27, due Nov 3.}

\bigskip

\noindent
1. Define the syntax and the semantics of disjunction over sets.
Study the special cases when the set is empty and when the set contains only one element.
%(See the style used in the lecture for studying the conjunction.)


\bigskip

\noindent
2. Write the equivalences of implication over one constant and one variable.

\bigskip

\noindent
3. Prove by reducing both sides to CNF:
$$ ((A \and B) \impl C)\ \equiv\ ((A \impl C) \or (B \impl C)).$$

\bigskip

\noindent
4. Prove by refutation, reduction to CNF, and resolution:
$$ A \impl C,\ B \impl C\ \elc\ (A \and B) \impl C$$ 
\end{document}

\bigskip

\noindent
6. Express the distributivity of disjunction over conjunction when they are
applied to sets. Study the special cases when sets are empty or contaion only
one element.
%(See the style used in the lecture for studying the distributivity of conjunction over disjunction.)

\bigskip

\noindent
3. Show validity by reducing to CNF:
$$ ((A \and B) \impl C)\ \impl\ ((A \impl C) \or (B \impl C)).$$

\bigskip

\noindent
5. Prove the correctness of the sequent rules for disjunction in the assumptions ($\and \ylc$)
and for negation in the goal ($\ylc \not$).

\bigskip

\noindent
3. Prove using the $\not \and$-sequent calculus:
$$ \not P,\ \not((\not P) \and Q)\ \ \ylc\ \ \not Q $$


