\documentclass{article}
\usepackage{graphics}
\usepackage{fancyhdr}
\usepackage{amsmath}
\usepackage[topbottom,singlearrows]{logicsym}
\usepackage{multicol}


\newcommand{\coursenumber}{081}
\newcommand{\coursetitle}{Computability and Logic}

\topmargin  18pt  	% 27pt
\headheight 12pt  	% 12pt
\headsep    35pt 	% 45pt
\textheight 8.0in
\textwidth  6.2in

\oddsidemargin   22pt      % Left margin on odd-numbered pages.
\evensidemargin  22pt      % Left margin on even-numbered pages.
\marginparwidth  72pt       % Width of marginal notes.
\marginparsep    11pt      % Horizontal space between outer margin and 
                           % marginal note

\pagestyle{fancy}
\lhead{CSCI \coursenumber}
\chead{}
\rhead{\semester}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\newcommand{\semester}[0]{
     \ifnum\month>7{Fall}\fi
     \ifnum\month<8{Spring}\fi\  \number\year
}

\begin{document}

\begin{center}{\Large Homework 6}\\ \vspace{1 ex} Due midnight,
Thursday, 3/5/2015 \end{center}

\vspace{2 ex}
\noindent

Please submit your homework solutions online at  
\texttt{http://www.dci.pomona.edu/tools-bin/cs081upload.php}.  If you 
have more than one file to be turned in, please put it in a folder 
and zip it up before turning it in.

Problems from the texts are given in the form c.n where c is the 
chapter and n is the problem number.  Thus problem 2.7 is problem 7 
from Chapter 2.

\vspace{2 ex}

\begin{enumerate}
    
  
    \item (15 points) \textbf{Classical Rules}
    \label{Problem:ClassicalRules}
    
    Show that the following rules of inference are all equivalent to
    one another, in the sense that adding one to the constructive
    rules gives a logical system that proves the same theorems as
    adding any other to the constructive rules.

    \begin{multicols}{2}\raggedcolumns
	\begin{enumerate}
	    \item \Infer[c]{\Not\Not \phi}{\phi}{{\Not\Not}\mathrm{e}}

	    \item \Infer[c]{}{\Not \phi\Or \phi}{\textrm{LEM}}

	    \item \Infer[c]{\phi\Implies \psi&\Not \phi\Implies
	    \psi}{\multicolumn{2}{c}{\psi}}{\textrm{Cases}}

	    \item \Infer[c]{\phi\Implies \psi}{\Not \phi\Or \psi}{\textrm{CDI}}

	    \item PBC
	\end{enumerate}
    \end{multicols}

    Suggestion: For two rules, X and Y, show that X can be simulated
    by the constructive rules and Y. This will show that any theorem
    provable with~X is also provable with~Y. Create a cycle of five
    such proofs that run through all the rules.  You may choose any
    order for the cycle, as long as there is a loop with all five
    rules.

    LEM, which stands for ``law of the excluded middle,'' is standard
    jargon.  PBC is used by Huth and Ryan for ``proof by
    contradiction.''  CDI stands for ``classical definition of
    implication''; it is made up especially for this problem.


    \item (10 points) \textbf{De Morgan laws}

    In class, we gave a constructive proof of one direction of a De
    Morgan law, $\phi\Or \psi\Proves\Not(\Not \phi\And\Not \psi)$.  Is
    the converse, $\Not(\Not \phi\And \Not \psi)\Proves \phi\Or \psi$,
    constructively provable?  If so, give a constructive proof.  If
    not, give a classical proof and show how to derive the classical
    contradiction rule (or an equivalent rule from
    Problem~\ref{Problem:ClassicalRules}) from it.

    \item (10 points)\textbf{Adequacy}
    
    Problem 1.5.3ab from H \& R page 87.  Problem 1.5.3c can be done 
    for 5 points extra credit.
    
    \item (5 points) \textbf{Conjunctive Normal Form}
    
    Problem 1.5.7b from H \& R page 88.
    
    \item (5 points) \textbf{Horn Clauses} 
    
    Problem 1.5.16 from H \& R page 90.

    

\end{enumerate}

\end{document}
