\documentclass[11pt]{handout}

\usepackage{6044}
\usepackage{time}
\usepackage[fleqn]{amsmath}

\setlength{\textheight}{8in}
\setlength{\textwidth}{5.5in}
\setlength{\oddsidemargin}{.4in} 
\setlength{\evensidemargin}{0in} 
\parindent0in
\parskip\medskipamount

\newcommand{\ple}{\ensuremath{\vdash_\le\,}}

\def\f={\mathop{\Code{=}}}
\newcommand{\eqtn}[2]{\Code{( #1 = #2 )}}
\newcommand{\peqtn}[2]{\fortext{\proves \eqtn{#1}{#2}}}
\newcommand{\etrm}[1]{\Code{ = #1}}
\newcommand{\leqtn}[2]{\Code{( #1 <= #2 )}}

\makeatletter
\renewenvironment{description}
               {\list{}{\labelwidth\z@
                        \leftmargin1em
                        \itemindent-\leftmargin
                        \let\makelabel\descriptionlabel}}
               {\endlist}
\makeatother

\renewcommand*\descriptionlabel[1]{\hspace\labelsep
                                {\normalfont\bfseries #1}:}


\begin{document}
\handout{ps1-soln}{Problem Set 1 Solutions}{4 October 1996; typo 8 Oct}

\reminder {\bf QUIZ 1} in class on Monday, 7 October.

\medskip

\subsubsection*{Problem 3(a)}

We use structural induction on arithmetic expression $e$, to show that
\Code{\provable ($f$ = $g$)} implies
\[
    \Code{\provable (\subst{e}{x}{f} = \subst{e}{x}{g})}
\]
for any arithmetic expressions $e$, $f$, $g$, and variables~$x$.

\begin{description}

\item[Base case 1] $e$ is a constant or variable, $c$, distinct from~$x$.  Then
by the definition of substitution, $\subst{e}{x}{f}$ is actually the arithmetic
expression $c$.  Likewise, $\subst{e}{x}{g}$ is~$c$.  Since \Code{($c$ = $c$)}
is an instance of the reflexivity axiom, we immediately have \Code{\provable
($c$ = $c$)}.  In this base case, we did not need to use the hypothesis
\Code{\provable ($f$ = $g$)}.

\item[Base case 2] $e$ is the variable $x$.  Then by the definition of
substitution, $\subst{e}{x}{f}$ is the expression $f$.  Likewise
$\subst{e}{x}{g}$ is~$g$.  So this base case requires that we show that
\eqtn{$f$}{$g$} is provable.  But this is exactly the hypothesis
\Code{\provable ($f$ = $g$)}, so we are done.

\item[Structural induction case 1] $e$ is of the form \Code{$e_{1}$ + $e_{2}$}.
Assume \Code{\provable ($f$ = $g$)}.  Then by induction, we also have that
\[
    \Code{\provable (\subst{e_1}{x}{f} = \subst{e_1}{x}{g})},
\]
and
\[
   \Code{\provable (\subst{e_2}{x}{f} = \subst{e_2}{x}{g})}.
\]

We must now show that
\[
    \peqtn{\subst{\Code{($e_1$ + $e_2$)}}{x}{f}}{\subst{\Code{($e_1$ + $e_2$)}}{x}{g}}
\]

By \Code{+}-congruence from the first two equations above, we have
\[
    \peqtn{\subst{e_1}{x}{f} + \subst{e_2}{x}{f}}{\subst{e_1}{x}{g} + \subst{e_2}{x}{g}}.
\]

But by definition of substitution, the lefthand side of this equation is the
same as \Code{\subst{(e_1 + e_2)}{x}{f}}, and the righthand side is
\Code{\subst{(e_1 + e_2)}{x}{g}}, so we are done.

\item[Structural induction cases 2 \& 3] $e$ is of the form \Code{$e_{1}$ * $e_{2}$} or
\Code{-$e_{1}$}.  Essentially the same as case 1.
\end{description}

\subsubsection*{Problem 3(b)}

We use induction on the length of the equational
proof of \eqtn{$e$}{$g$} to show that \peqtn{$e$}{$g$} implies
\peqtn{\subst{e}{x}{f}}{\subst{g}{x}{f}}.

\begin{description}

\item[Base case] The proof of \eqtn{$e$}{$g$} is of length 1.  This means that
\eqtn{$e$}{$g$} is an axiom.  But then we claim that
\eqtn{\subst{e}{x}{f}}{\subst{g}{x}{f}} is another instance of the same axiom,
and so also has a proof of length 1.

We illustrate why the claim holds for the (commutativity of \Code{+})
axiom, \eqtn{$e_1$ + $e_2$}{$e_2$ + $e_1$}.  Namely, we claim
that the equation
\[
    \eqtn{\subst{\Code{($e_1$ + $e_2$)}}{x}{f}}{\subst{\Code{($e_2$ + $e_1$)}}{x}{f}}
\]

is also an instance of commutativity.  To see this, let $h_{1}$ be the
expression \subst{e_1}{x}{f} and $h_{2}$ be \subst{e_2}{x}{f}.
By the definition
of substitution, the lefthand side of the equation displayed above is
\Code{$h_{1}$ + $h_{2}$} and the righthand side is \Code{$h_{2}$ + $h_{1}$},
so the equation above is of the required form $\eqtn{$h_1$ + $h_2$}{$h_2$ + $h_1$}$.

The proofs of the claim for the other axioms follow similarly.

\item[Induction] The proof of \eqtn{$e$}{$g$} is of length $n+1$ for some
$n\geq 1$.

In this case we use the fact that the five\footnote{We don't need to count
(reflexivity), since it is an axiom.} formal inference rules of Handout 3,
Table 1, have a property similar to that claimed for the axioms.  Namely, if
we perform the same substitution on all the antecedents and the consequent of a
rule, we obtain another instance of the same rule.  The argument proving this
is similar to the argument above for the commutativity axiom.  We leave it to
the reader to check this fact.

Now, if \eqtn{$e$}{$g$} is an axiom, the proof for the Base case shows that
\peqtn{\subst{e}{x}{f}}{\subst{g}{x}{f}}.  Otherwise, \eqtn{$e$}{$g$} must
follow from an instance of an inference rule whose antecedents are equations
earlier in the formal proof.  By the claim above, substituting $f$ for $x$ into
the antecedents and consequent of this inference rule is another instance of
the rule.  But the antecedents must have proofs of length at most $n$, so by
induction, we have the result of substituting $f$ for $x$ in any antecedent
equation is also provable.  Now the equation
\eqtn{\subst{e}{x}{f}}{\subst{g}{x}{f}} is the consequent of the substituted
instance of the inference rule, and the substituted antecedents are provable,
so we conclude by Problem 2 that this consequent is also provable.
\end{description}


\subsubsection*{Problem 4(a)} Show that \peqtn{-$e$}{-1 * $e$}.

Remember that a {\em formal proof} of an arithmetic equation, ${\cal E}$,
is sequence ${\cal E}_{1},{\cal E}_{2},\dots$ of arithmetic equations
which fit together according to the inference rules of Handout 3 and which
end with ${\cal E}$.  Formal proofs are generally too long and tedious to
write out.

What follows is a real, {\em mathematical} proof---written in English with
mathematical notation---that {\em there exists a formal proof}.  Using the
mathematical properties of formal provability from Problems 2 and 3(a), we
can conclude that the formal proof exists without writing it out.

\begin{proof}
The sequence of two equations 
\[\begin{array}{l}
\eqtn{0 + (-$e$)}{-$e$},\\
\eqtn{-$e$}{0 + (-$e$)}
\end{array}\]
is a formal proof because the first equation is an instance of the
(identity for \Code{+}) axiom, and the second equation follows from the
first by the (symmetry) rule.  Hence,
\[\peqtn{-$e$}{0 + (-$e$)}.\]

Now observe that the equation \eqtn{0 + (-$e$)}{($e$*0) + (-$e$)}
follows from the equations \eqtn{0}{$e$*0} and \eqtn{-$e$}{-$e$} by the
(\Code{+}-congruence) rule.  From Figure 2 of Handout 3, we know
\peqtn{0}{$e$*0}, and of course \peqtn{-$e$}{-$e$} by the (reflexivity)
axiom.  So by the results of Problem 2, we conclude
\[\peqtn{(0 + (-$e$)}{($e$*0) + (-$e$)}.\]

It will be useful at this point to introduce some new notation:
\[\proves e_{1} \f= e_{2} \f= \cdots \f= e_{n}\]
is an abbreviation for the assertions \peqtn{$e_{i}$}{$e_{j}$} for all
$1\leq i,j\leq n$.  Note that if
\[\proves e_{1} \f= e_{2} \f= \cdots \f= e_{n}, \]
and for some $i\leq n,$
\[\peqtn{$e_{i}$}{$e_{n+1}$},\]
then by the formal inference rules (transitivity) and (symmetry), and the
results of Problem 2, we may conclude
\[\proves e_{1} \f= e_{2} \f= \cdots \f= e_{n+1} \f= e_{n+1}.\]

So we can summarize the two provable equations displayed above by the
``three-way'' equality
\[\proves \Code{-$e$} \etrm{0 + (-$e$)} \etrm{($e$*0) + (-$e$)}.\]

Now \peqtn{(1 + (-1))}{0} the (inverse for \Code{+}) axiom and (symmetry).
Substituting the two sides of this equation for \Code{x} in the expression
\Code{($e$*x) + (-$e$)}, we conclude from Problem 3(a) that
\[\peqtn{($e$*0) + (-$e$)}{($e$*(1 + (-1))) + (-$e$)}.\]

So we can attach \etrm{($e$*(1 + (-1))) + (-$e$)} to the three-way
equality to obtain the four-way equality
\[\proves \Code{-$e$} \etrm{0 + (-$e$)} \etrm{($e$*0) + (-$e$)} \etrm{($e$*(1 + (-1))) + (-$e$)}.\]

Continuing, we can attach
\[\etrm{($e$*1 + $e$*(-1)) + (-$e$)}\]
by the (distributivity) axiom and
substitution.  Next we attach
\[\etrm{(1*$e$ + $e$*(-1)) + (-$e$)}\]
by (commutativity of \Code{*}) and substitution, and
\[\etrm{($e$ + $e$*(-1)) + (-$e$)}\]
by (identity for \Code{*}) and substitution,
\[\etrm{(-$e$) + ($e$ + $e$*(-1))}\]
by (commutativity of \Code{+}),
\[\etrm{((-$e$) + $e$) + $e$*(-1)}\]
by (associativity of \Code{+}),
\[\etrm{($e$ + (-$e$)) + $e$*(-1)}\]
by (commutativity of \Code{+}) and substitution,
\[\etrm{0 + $e$*(-1)}\]
by (inverse for \Code{+}) and substitution,
\[\etrm{$e$ * (-1)}\]
by (identity for \Code{+}),
\[\etrm{-1 * $e$}\]
by (commutativity of \Code{*}).

Hence,
\[\peqtn{-$e$}{-1 * $e$}.\]
\end{proof}

\subsubsection*{Problem 4(b)}  Show that \peqtn{1}{-1 * (-1)}.
\begin{proof}
\[\proves \Code{1} \etrm{0+1} \etrm{1+0} \etrm{1+(-1 + (-(-1)))} \etrm{(1+(-1)) + (-(-1))} \etrm{0 + (-(-1))} \etrm{-(-1)}\]
where the successive equalities follow by (identity for
\Code{+}) \& (symmetry), (commutativity for \Code{+}), (inverse for
\Code{+}) \& substitution, (associativity), (inverse for
\Code{+}) \& substitution, and (identity for \Code{+}).  So
\[\peqtn{1}{-(-1)}.\]

But letting $e$ be \Code{-1} in 4(a), we have
\[\peqtn{-(-1)}{-1 * (-1)},\]
so by transitivity and Problem 2,
\[\peqtn{1}{-1 * (-1)}.\]

 \end{proof}

\subsubsection*{Problem 5}

Since $\widehat{n}$ and $\widehat{-n}$ were defined inductively for $n \ge 0$,
we use induction on $n \ge 0$ to show that $\mean{\widehat{n}}V = n$ and
$\mean{\widehat{-n}}V = -n$ for all valuations~$V$.

\begin{description}

\item[Base case]
$\mean{\widehat{0}}V = \mean{0}V = 0$.

\item[Induction case 1]
Assume $\mean{\widehat{n}}V = n$ for $n \ge 0$.  Then
\begin{align*}
\mean{\widehat{n+1}} V  &= \mean{(\Code{1} + \widehat{n})} V \\
                    &= \mean{\Code{1}} V + \mean{\widehat{n}} V \\
                    &= 1 + n \\
                    &= n + 1
\end{align*}

\item[Induction case 2]
Assume $\mean{\widehat{-n}}V = -n$ for $n \ge 0$.  Then
\begin{align*}
\mean{\widehat{-(n+1)}} V   &= \mean{(\Code{(-1)} + \widehat{-n})} V \\
                    &= \mean{\Code{(-1)}} V + \mean{\widehat{-n}} V \\
                    &= -\mean{\Code{1}} + (-n) \\
                    &= -1 + (-n) \\
                    &= -(n + 1)
\end{align*}

\end{description}

\subsubsection*{Problem 6(c)}

We use induction on the magnitude of $n$ to show that
\peqtn{$\widehat{n}$ + $\widehat{m}$}{$\widehat{n + m}$} for all
$m, n \in \integers$.

\begin{description}

\item[Base case] $n = 0$.  We must show that
\[
\peqtn{$\widehat{0}$ + $\widehat{m}$}{$\widehat{0 + m}$}.
\]

Since $\widehat{0}$ is \Code{0}, the arithmetic expression on the lefthand side
of the equation is actually \Code{(0 + $\widehat{m}$)}, and the righthand side 
is of course $\widehat{m}$.  So the equation is simply an instance of the
(identity for \Code{+}) axiom, and so is provable.

\item[Induction case $n \ge 0$]
We must show that
\[\peqtn{$\widehat{(n+1)}$ + $\widehat{m}$}{$\widehat{(n+1) + m}$}\]
and
\[\peqtn{$\widehat{-(n+1)}$ + $\widehat{m}$}{$\widehat{-(n+1) + m}$}.\]

We'll work on the second equation.

The lefthand side of the second equation is of the form \Code{(-1 +
$\widehat{-n}$) + $\widehat{m}$} because $\widehat{-(n+1)}$ is \Code{-1 +
$\widehat{-n}$} by definition.  In this form, we can see that the
lefthand side is provably equal to the expression \Code{$\widehat{-n}$ + (-1 +
$\widehat{m})$} by (commutativity), (associativity) and substitution (cf.,
Problem 3(a)).  The previous expression is in turn provably equal to
\Code{$\widehat{-n}$ + $\widehat{m-1}$} by {\bf Problem 6(b)} and substitution.
Now {\em by induction}, this expression is itself provably equal to
\Code{$\widehat{-n + (m-1)}$} which is of course the same as the righthand side
of the second equation.

The argument for the first equation is similar.

\end{description}

\subsubsection*{Problem 6(f)}

We use structural induction to show that \Code{\provable ($e$ =
$\widehat{\mean{e} V}$)} for all valuations~$V$ and all variable-fee arithmetic
expressions~$e$.

\begin{description}

\item[Base case 1] $e$ is \Code{0}.
We must show
\[\peqtn{0}{$\widehat{\mean{\Code{0}}V}$)}\]
for every valuation $V$.

By the definition of values of arithmetic expressions, $\mean{\Code{0}}V = 0$
for any $V$.  So the righthand side of the equation above is $\hat{0}$, which
is \Code{0} by definition of $\hat{}$.  Hence this equation is actually the axiom
\eqtn{0}{0}, and so is immediately provable.

\item[Base case 2] $e$ is \Code{1}.  Similarly.

\item[Induction case 1] $e$ is \Code{$e_{1}$ + $e_{2}$} for variable-free
$e_{1}, e_{2}$.

By induction, we have
\[
    \peqtn{$e_1$}{$\widehat{\mean{e_1} V}$}
\]
and
\[
    \peqtn{$e_2$}{$\widehat{\mean{e_2} V}$}.
\]
So by \Code{+}-congruence
\[
    \peqtn{$e_1$ + $e_2$}{$\widehat{\mean{e_1} V}$ + $\widehat{\mean{e_2} V}$}.
\]
Using Problem~6(c), the righthand side of this equation is provably equal to
\Code{$\widehat{\mean{e_1} V + \mean{e_2} V}$}.  So by transitivity,
\[
    \peqtn{$e_1$ + $e_2$}{$\widehat{\mean{e_1} V + \mean{e_2} V}$}.
\]

But the righthand side of this equation above is $\widehat{\mean{\Code{($e_1$ + $e_2$)}}V}$
by definition of \mean{\cdot}.  That is,
\[
    \peqtn{$e_1$ + $e_2$}{$\widehat{\mean{\Code{($e_1$ + $e_2$)}}V}$}
\]
as required for this case.

\item[Induction case 2 \& 3] $e$ is \Code{$e_{1}$ * $e_{2}$} or
\Code{-$e_{1}$}.  Similarly.

\end{description}

\subsubsection*{Problem 10(a)}

To show that $n \le m$ iff \Code{\ple ($\widehat{n}$ \cle\
$\widehat{m}$)}, we prove the two directions separately.

If \Code{\ple ($\widehat{n}$ \cle\ $\widehat{m}$)}, then $n \le m$: 

The proof system for inequalities is sound, so $\ple \Code{($\widehat{n}$ \cle\
$\widehat{m}$)}$ implies this inequality is valid .  That is, $\mean{\widehat{n}} V \le
\mean{\widehat{m}} V$ for any valuation~$V$.  From problem~5, we have that
$\mean{\widehat{n}} V = n$.  Therefore, $n \le m$.

\medskip

If $n \le m$, then \Code{\ple ($\widehat{n}$ \cle\ $\widehat{m}$)}:

We prove this by induction on~$m-n$.
\begin{description}

\item[Base case $m - n = 0$]
We must show that
\[\Code{\ple ($\widehat{n}$ \cle\ $\widehat{n}$)}
\]
But this follows immediately from (reflexivity) and ($\leq$-reflexivity).

\item[Induction case $m - n > 0$].
We first note that $\ple \leqtn{(-1 + $e$)}{$e$}$.  Here is a formal proof,
beginning with the \Code{+} identity and inverse axioms:
\[\begin{array}{l}
\eqtn{0 + (-0)}{-0}\\
\eqtn{0 + (-0)}{0}\\
\eqtn{-0}{0 + (-0)}\\
\eqtn{-0}{0}\\
\leqtn{-0}{0}\\
\leqtn{0}{1}\\
\leqtn{-1}{-0}\\
\leqtn{-1}{0}\\
\leqtn{-1 + e}{0 + e}\\
\eqtn{0 + e}{e}\\
\leqtn{0 + e}{e}\\
\leqtn{-1 + e}{e}
\end{array}\]

Now $\ple \leqtn{$\hat{n}$}{$\widehat{m - 1}$}$ by induction, and
\peqtn{$\widehat{m - 1}$}{-1 + $\hat{m}$} by 6(b), so $\ple \leqtn{$\hat{n}$}{-1 +
$\hat{m}$}$ by ($\leq$-reflexivity) and ($\leq$-transitivity).  But 
$\ple \leqtn{-1 + $\hat{m}$}{$\hat{m}$}$ by the formal proof above, so 
$\ple \leqtn{$\hat{n}$}{$\hat{m}$}$ by ($\leq$-transitivity).

\end{description}

\subsubsection*{Problem 10(b)}
We must show for all variable-free $e,f$, that if
$\models \leqtn{$e$}{$f$}$, then $\ple \leqtn{$e$}{$f$}$.

So assume $\models \leqtn{$e$}{$f$}$.  This means that $\mean{e} V \le
\mean{f} V$ for any valuation~$V$.  From~10(a), we have
\[\Code{\ple ($\widehat{\mean{e} V}$ \cle\ $\widehat{\mean{f} V}$)}.\]
From~6(f) we have
\[\peqtn{$e$}{$\widehat{\mean{e} V}$}\]
and \peqtn{$f$}{$\widehat{\mean{f} V}$}.  So by ($\leq$-reflexivity) and
($\leq$-transitivity), we conclude that $\ple \leqtn{$e$}{$f$}$.


\subsubsection*{Problem 11}  It was claimed in the Handout 3 that
\begin{theorem*}
Given any proof checking program for a sound proof system with arithmetic
inequalities as formal theorems, we can construct an inequality which is
valid over the integers but which has no proof in the system.
\end{theorem*}
But if the inequality has no proof, how can we possibly know it
is valid?

{\bf Answer}: Wait a minute!  Nobody said the inequality has no formal
proof at all.  In fact, as soon as you show me an inequality which can't
be proved in some {\em particular} formal proof system, I can show you
{\em another} formal proof system in which the inequality {\em can} be
proved---namely the original system augmented with the unprovable
inequality as an axiom!  So there is no such thing as an {\em inherently
unprovable} inequality.

OK, so given a sound formal proof system, how can we find an inequality
which is not provable in that particular system and at the same time be
sure that the inequality is valid?  We'll show how later in the course.
When we do so, we will also present an elegant short argument explaining
why the inequality is both unprovable and valid.  The argument will be
short because it begins with the powerful hypothesis that the given formal
proof system is {\em sound}, i.e., that all the inequalities formally
provable in the system are themselves valid.

So how we can know that a given proof system is sound?  That is a much
harder question in general, and it will bear further discussion later in
the course.

\end{document}
