\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/7/2013 \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 (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.
    
    \item (5 points) \textbf{Predicate Logic} 
    
    Problem 2.1.3 from H \& R page 157.
    
    \item (10 points) \textbf{Free \& Bound Variables} 
    
    \begin{enumerate}
	\item In the formula below, or a copy of it, underline the
	occurrences of free variables and circle the occurrences of
	bound variables.  (Consider the variable right after a
	quantifier to be bound.)
	\[
	\Forall z\Big(P(x)\And\Forall x\Exists y\big(
           Q(y,f(z))\Implies R(g(g(w,x),f(y)))
           \big)\Big)
	\]
	
%%%
\newbox\theencirclebox
\newcount\encircleboxHt
\newcount\encircleboxWd
\newcount\encircleboxDp
%
\newcommand\encircle[1]{\ensuremath{%
{\setbox\theencirclebox=\hbox{$#1$}
\setlength\unitlength{1pt}
\encircleboxHt=\ht\theencirclebox \divide\encircleboxHt\unitlength
\encircleboxWd=\wd\theencirclebox \divide\encircleboxWd\unitlength
\encircleboxDp=\dp\theencirclebox \divide\encircleboxDp\unitlength
\begin{picture}(0,0)
\put(3,3){\circle{12}}
\end{picture}\box\theencirclebox}}}
%%%
\emph{Using the definitions included in the LaTeX file, the command
\{$\backslash$encircle x\} can be used to draw a letter with a circle
around it: {\encircle x}.  $\backslash$underline\{x\} will generate 
\underline{x}.}
	
	\item 
	Let $\phi$ be the formula in part~a.  Write out the formulas
	below, renaming bound variables when necessary to avoid
	``capture.''
	\begin{enumerate}\renewcommand{\theenumi}{\roman{enumi}}
	    \item $\phi[f(y)/x]$
	    \item $\phi[f(y)/z]$
	    \item $\phi[f(y)/w]$
	\end{enumerate}
    \end{enumerate}
    
    \item (10 points) \textbf{Proofs}
    
    Exactly one of the inferences below is correct.  Give a
    (constructive) proof of the correct member and a short intuitive
    explanation of why the other is incorrect.

    \begin{enumerate}
	\item $\Forall x(\phi\Or \psi)\Proves\Forall x \phi\Or\Forall
	x \psi$\quad and\quad

	\item $\Forall x \phi\Or\Forall x \psi\Proves\Forall x(\phi\Or
	\psi)$
    \end{enumerate}
    
    \item (10 points) \textbf{Bad Proof}
    
    Recall the axioms for an equivalence relation ${\sim}$:
    \begin{itemize}
	\item[] A0. $\Forall x \big(x\sim x\big)$
	\item[] A1. $\Forall x\Forall y\big(x\sim y\Implies y\sim x\big)$

	\item[] A2.  $\Forall x\Forall y\Forall z\big(x\sim
	y\Implies\big(y\sim z\Implies x\sim z\big)\big)$
    \end{itemize}

    Consider the following proof sketch that purports to prove that
    $\mathrm{A1,A2}\Proves{}\allowbreak\mathrm{A0}$.  Formalize the
    sketch and use your formulation to identify the error in it.

    \begin{quote}\noindent Let $x$ be arbitrary and suppose that
	$x\sim y$.  Then by A1, $y\sim x$.  Using these two facts, we
	may use A2 to conclude that $x\sim x$.  Because $x$ was
	arbitrary, we have $\Forall x\big(x\sim x\big)$.
    \end{quote}

    \item (10 points) \textbf{Proofs} 
    
    Problem 2.3.11ac from H \& R page 162.

\end{enumerate}

\end{document}
