\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}}}
\newcommand{\nov}[1]{{\overline #1}}

\pagestyle{empty}

\begin{document}

{\bf Mathematical Logic, WS 2018.
Homework 4, given Nov 13, due Nov 20}

\bigskip

\bigskip

\noindent
1.
Prove in natural style, using inference rules of your choice:

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

\bigskip

\noindent
2. Prove the previous formula by sequent calculus, using inference rules of your choice.

\bigskip

\noindent
3.
Formalize (experimentally) the sequent proof rules used in the previous proof.
(You do not need to prove their correctness.)
 
\end{document}
