\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 2018.
Homework 5, given Nov. 20, due Dec. 4.}

\bigskip

\noindent
1.
Using the sequent rules for $\not$ and $\and$,
find the sequent rule for $\or$ in the goal.

\bigskip

\noindent
2. 
Using the sequent rules for $\not, \and,$ and $\or$,
find the sequent rule for $\impl$ in the goal.

\bigskip

\noindent
3.
Using the sequent rules for $\not, \and, \or,$ and $\impl$,
find the sequent rule for $\lequiv$ in the assumptions.

\bigskip

\noindent
4.
Using the sequent rules for $\not, \and, \or,$ and $\impl$,
find the sequent rule for $\lequiv$ in the goal.

\bigskip

\noindent
5.
Apply the sequent rules presented in the lecture and the onew found above
for constructing the sequent proof of:

$(A \and B) \impl C\ \lequiv\ (A \impl C) \or (B \impl C)$

\bigskip

\noindent
6.
Apply the sequent rules presented in the lecture and the onew found above
for constructing the sequent proof of:

$(A \or B) \impl C\ \lequiv\ (A \impl C) \and (B \impl C)$

\bigskip

\noindent
7.
Define inductively the function FreeVars[$\varphi$] which gives the set of free variables of a first order predicate logic formula $\varphi.$


\end{document}

 
