\documentclass[11pt]{handout}
\usepackage{6044}
%\documentclass[11pt]{article}
%\usepackage{6001}
\usepackage{time,fullpage}
\usepackage{amsmath}
\usepackage{prooftree}

\textheight 8in

\oddsidemargin 11pt
\evensidemargin \oddsidemargin
\marginparwidth 0.5in

\advance\textwidth by -2\oddsidemargin

\newdimen\tablewidth
\tablewidth=\textwidth
\advance \tablewidth by -11pt

\parindent 0.0in
\parskip \medskipamount

\let\to\rightarrow
\let\union\cup
\let\cross\times

\def\SI{\mbox{Scheme-Integer}}
\def\SNI{\mbox{Scheme-Nonneg-Integer}}
\def\SN{\mbox{Sch-\-Num}}
\def\SB{\mbox{Sch-Bool}}
\def\Empty{\mbox{Empty}}
\def\SI{\mbox{Sch-Int}}
\def\SNI{\mbox{Sch-Nonneg-Int}}


\makeatletter

\def\DefineBNFAbbrev#1#2{%
    \expandafter\newcommand\expandafter{\csname#1\endcsname}{\@bnfabbrev{#2}}%
}

\def\@bnfabbrev#1{%
    \@ifnextchar _{\@subabbrev{#1}}{\@plainabbrev{#1}}%
}

\def\@subabbrev#1_#2{\hbox{\normalfont$\langle\mbox{#1}_{#2}\rangle$}}

\def\@plainabbrev#1{\hbox{\normalfont$\langle\mbox{#1}\rangle$}}

% \def\exp{\hbox{$\bnf <expression>$}}

\DefineBNFAbbrev{idfr}{identifier}
\DefineBNFAbbrev{expr}{expression}
\DefineBNFAbbrev{define}{define}
\DefineBNFAbbrev{defines}{defines}
\DefineBNFAbbrev{vrbl}{variable}
\DefineBNFAbbrev{bod}{body}
\DefineBNFAbbrev{init}{init}
\DefineBNFAbbrev{val}{value}
\DefineBNFAbbrev{pval}{primitive\ value}
\DefineBNFAbbrev{ival}{immediate\ value}
\DefineBNFAbbrev{test}{test}
\DefineBNFAbbrev{orsf}{or}
\DefineBNFAbbrev{andsf}{and}
%\DefineBNFAbbrev{beginsf}{begin}

\makeatletter


\def\fbox#1{%
  \vtop{\vbox{\hrule%
     \hbox{\vrule\kern3pt%
 \vtop{\vbox{\kern3pt#1}\kern3pt}%
 \kern3pt\vrule}}%
 \hrule}}

\let\to\rightarrow
\let\union\cup
\let\cross\times

\def\z3{\fortext{\integers_{3}}}
\def\ltecom{\fortext{\sqsubseteq}}
\newcommand{\lcm}{\mathop{\rm lcm}\nolimits}
\newcommand{\subst}[3]{#1[#2 := #3]}
\let\union\cup

\newcommand{\aeval}[2]{{\it val}(#1,#2)}
\newcommand{\provable}{\fortext{\vdash\,}}
\newcommand{\notprovable}{\fortext{\not\vdash\,}}
\newcommand{\can}[1]{\mbox{canon}(#1)}

\newcommand{\notmodels}{\fortext{\not\models}}

\newcommand{\integers}{\ensuremath{\mathbb{Z}}}
\newcommand{\reals}{\ensuremath{\mathbb{R}}}
\newcommand{\complex}{\ensuremath{\mathbb{C}}}

\begin{document}

\handout{aeq-notes}{Notes on Proving Arithmetic Equations}{September 6,
1996; corrected Sept. 10}

\section{Expressions and Values}

In these notes we describe a formal system for proving arithmetic
equations.  Our objective is to explain what it means to have a completely
formal, automatically verifiable proof system, and to clarify the basic
properties of such proof systems.  Our objective is {\em not} to clarify
the basic properties of numbers---we need to know these beforehand in
order to understand and justify the proof system.  For example, it will
take some effort in our system to prove that $e \times 0 = 0$; the formal
proof certainly does not make this equation any more or less obvious.

\begin{definition}
{\em Arithmetic expressions} (ae's) are defined inductively as follows:
\begin{itemize}
\item
The numerals {\tt 0}, {\tt 1} are ae's.

\item
Any variable, $x$, is an ae.

\item
If $e$ is an ae, then so is {\tt (-$e$)}.

\item
If $e$, $f$ are ae's, then so are {\tt ($e$ + $f$)} and {\tt ($e$ * $f$)}.

\item
That's all.
\end{itemize}
\end{definition}

We use the symbol $\integers$ for the set of all integers $\{0,1,-1,2,-2,\dots\}$.

\begin{definition}
A {\em valuation}, $V,$ is a mapping from the set, {\em Var}, of variable
symbols which may appear in ae's, into $\integers$.  The {\em value},
$\aeval{e}{V},$ of an ae, $e$, at a valuation, $V$, is defined by
structural induction on ae's as follows:
\begin{itemize}

\item
$\aeval{{\tt 0}}{V} = 0$ and $\aeval{{\tt 1}}{V} = 1$.

\item
$\aeval{x}{V}= V(x)$ for any variable, $x$.

\item
$\aeval{\Code{(-$e$)}}{V} = -\aeval{e}{V}$.

\item
$\aeval{\Code{($e$ + $f$)}}{V} = \aeval{e}{V} + \aeval{f}{V}$, and

\item $\aeval{\Code{($e$ * $f$)}}{V} = \aeval{e}{V} \times \aeval{f}{V}$.

\end{itemize}
The {\em meaning}, $\mean{e}$, of an ae, $e$, is the function from
valuations to $\integers$ defined by:
\[
\mean{e}(V) = \aeval{e}{V}.
\]
It is conventional to omit parentheses around the arguments of meaning
functions, writing ``$\mean{e}V$'' instead of ``$\mean{e}(V)$.''

\end{definition}

\begin{definition}

An {\em arithmetic equation\/} (aeq) is an expression of the form \Code{($e$
= $f$)} where $e$, $f$ are ae's.  The aeq is {\em true} at
valuation $V$, written
\[
V \models \Code{($e$ = $f$)},
\]
iff $\mean{e}V = \mean{f}V$.  The equation is {\em valid}, written
\[
\models \Code{($e$ = $f$)}
\]
iff it is true at all valuations, that is, iff $\mean{e} = \mean{f}$.
\end{definition}


\begin{example}
Let $e_{0},f_{0}$ be the ae's
\begin{eqnarray*}
e_{0} &::=& \Code{((1 + (1 + 1)) * (x + y))},\\
f_{0} &::=& \Code{((y * (x * y)) + (-((1 + 1) + 1)))}.
\end{eqnarray*}
Let $V_{1}$ be a valuation such that $V_1(\Code{x}) = 2$, and
$V_1(\Code{y}) = 3$.  Then $\aeval{e_0}{V_1} = 15$ and $\aeval{f_0}{V_1} =
15$, so $V_1 \models \Code{($e_{0}$ = $f_{0}$)}$.  Let $V_2$ be the
valuation such that $V_{2}(v) = 0$ for all variables $v$.  Then
$\aeval{e_{0}}{V_2} = 0 \neq -3 = \aeval{f_{0}}{V_2}$, so $V_{2}\:
\notmodels\: \Code{($e_{0}$ = $f_{0}$)}$.  Thus, \Code{($e_{0}$ = $f_{0}$)}
is {\em not} valid.
\end{example}

As another example, note that equations of the following form are valid:

\begin{lemma}\label{dist-lem}
\[
\models \Code{( ($e$ * ($f$ + $g$)) = (($e$ * $f$) + ($e$ * $g$)) )}
\]
for all ae's $e,f,g$.
\end{lemma}

\begin{proof}
Let $V$ be any valuation and $l,m,n$ be the values of $e,f,g$ at $V$.  Then
\[
\mean{\Code{($e$ * ($f$ + $g$))}}V = l(m+n)
\]
by definition of the meaning of ae's.  Likewise,
\[
\mean{\Code{(($e$ * $f$) + ($e$ * $g$))}}V = lm + ln.
\]
But $l(m+n) = lm+ln$ by the distributive law of arithmetic, so
\[
\mean{\Code{($e$ * ($f$ + $g$))}}V = \mean{\Code{(($e$ * $f$) + ($e$ *
$g$))}}V.
\]
But $V$ was arbitrary, so this equation must hold for all $V$, i.e., the
equation is valid.
\end{proof}

\section{Equational Proofs}

We've been careful so far to use a special ``teletype'' font for the {\em
actual} symbols ``\Code{)}, \Code{*},''\ldots occurring in ae's, to
distinguish them from the italic font mathematical symbols ``{\it )}, $x$,
$e$, $f$'' used to {\em describe} ae's.  To keep our notation uncluttered,
from now on we stop being so careful when there is no danger of ambiguity.
In particular, we often will omit parentheses and just use mathematical
font throughout expressions.  For example, the valid equations of
Lemma~\ref{dist-lem} above will now be written as

\[e * (f + g) = (e * f) + (e * g).\]

\begin{definition}

An aeq, $C$, is said to {\em follow by the transitivity rule\/} from the
pair of aeq's $A_1$ and $A_2$ iff $A_1$ is of the form $e = f$, $A_2$ is
of the form $f = g$, and $C$ is of the form $e = g$.

We use the notation
\begingroup
\[
\prooftree
     e = f, \quad f = g
\justifies
    e = g
\endprooftree
\]
\endgroup
as a shorthand description of this rule.  The aeq's above the
horizontal line are called the {\em antecedents\/} of the rule, and
the aeq below the line is called its {\em consequent}.
\end{definition}

Along with transitivity, the {\em reflexivity, symmetry}, and {\em
congruence rules\/} together are called the {\em standard equational
inference rules}.  They are described in Table~\ref{steqrules}.  Note that
the reflexive rule has no antecedents.  Such rules without antecedents are
usually called {\em axioms} and are just written as equations, omitting
the horizontal line.

\begin{table}[h]
\caption{Standard Equational Inference Rules. \label{steqrules}}\small
\[\begin{array}{|c|} \hline
\\
\prooftree
\justifies
    e = e
\using
    \mbox{(reflexivity)}
\endprooftree
\qquad\quad
\prooftree
    e = f
\justifies
    f = e
\using
    \mbox{(symmetry)}
\endprooftree
\qquad\quad
\prooftree
     e = f, \quad f = g
\justifies
    e = g
\using
    \mbox{(transitivity)}
\endprooftree\\
\\
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 + f_1 = e_2 + f_2
\using
    \mbox{($+$-congruence)}
\endprooftree
\quad
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 * f_1 = e_2 * f_2
\using
    \mbox{($*$-congruence)}
\endprooftree
\quad
\prooftree
    e = f
\justifies
   -e = -f
\using
    \mbox{($-$-congruence)}
\endprooftree\\
\\ \hline
\end{array}\]
\end{table}

To capture the properties of arithmetic, we will need some additional
axioms.  These {\em equational axioms for arithmetic} are all the aeq's of
the forms given in Table~\ref{eqaxarith}.

\begin{table}[h]
\caption{Equational Axioms for Arithmetic\label{eqaxarith}}
\[\begin{array}{|rcll|}
\hline
(e + f) + g &=& e + (f + g) & \mbox{(associativity of $+$)}\\
(e * f) * g &=& e * (f * g) & \mbox{(associativity of $*$)}\\
e + f &=& f + e & \mbox{(commutativity of $+$)}\\
e * f &=& f * e & \mbox{(commutativity of $*$)}\\
0 + e &=& e  & \mbox{(identity for $+$)}\\
1 * e &=& e  & \mbox{(identity for $*$)}\\
e + (-e) &=& 0  & \mbox{(inverse for $+$)}\\
e * (f + g) &=& (e * f) + (e * g) & \mbox{(distributivity)}\\
\hline
\end{array}\]
\end{table}

\begin{definition}
An {\em arithmetic equational proof} is a finite sequence of aeq's such
that every aeq in the sequence follows from aeq's earlier in the sequence
by one of the standard equational inference rules or axioms of arithmetic.
An aeq, $e = f$, is {\em equationally provable}, written
\[
\provable e = f,
\]
iff it is the last equation of some proof.
\end{definition}

A crucial property of formal proofs is that they can be checked
automatically, i.e., by a program, without any need for ``understanding''
of the subject matter by the checker.  Adding comments to an equational
proof can make proof checking easier, but it is not strictly necessary,
since it is not hard to program a checker for uncommented proofs.

Figure~\ref{fgg} contains a formal proof of the equation $(f + g) + -g =
f$.  For the reader's convenience, the names of the rules from which each
equation follows have been included as a comment after the equation.

\begin{figure}[h]
\caption{An arithmetic equational proof. \label{fgg}}\small
\[
\begin{array}{|rcll|}
\hline
g + -g &=& 0 & \mbox{(inverse for $+$)}\\
f &=& f & \mbox{(reflexivity)}\\
f + (g + -g) &=& f + 0 & \mbox{(congruence)}\\
(f + g) + -g &=& f + (g + -g) & \mbox{(associativity of $+$)}\\
(f + g) + -g &=& f + 0 & \mbox{(transitivity)}\\
f + 0 &=& 0 + f & \mbox{(symmetry)}\\
(f + g) + -g &=& 0 + f & \mbox{(transitivity)}\\
0 + f &=& f & \mbox{(identity for $+$)}\\
(f + g) + -g &=& f & \mbox{(transitivity)}\\
\hline
\end{array}
\]
\end{figure}

Using this formal proof, we can show:

\begin{lemma}
For all ae's $e$,
\[\provable 0 =  0 * e.\]
\end{lemma}

\begin{proof}
Figure~\ref{0e=0} exhibits a formal proof with rule names as comments.
\end{proof}
\begin{figure}[h]
\caption{A proof of $0 = e*0$. \label{0e=0}}\small
\[
\begin{array}{|rcll|}
\hline
0 + 1 &=& 1 & \mbox{(identity for $+$)}\\
e &=& e & \mbox{(reflexivity)}\\
e * (0 + 1) &=& e * 1 & \mbox{(congruence)}\\
e * 1 &=& e * (0 + 1) & \mbox{(symmetry)}\\
e * (0 + 1) &=& (e * 0) + (e * 1) & \mbox{(distributivity)}\\
e * 1 &=& (e * 0) + (e * 1) & \mbox{(transitivity)}\\
-(e * 1) &=& -(e * 1) & \mbox{(reflexivity)}\\
(e * 1) + -(e * 1) &=& ((e * 0) + (e * 1)) + -(e * 1) & \mbox{(congruence)}\\
\vdots\\
\mbox{(Insert proof from} & \mbox{Fig.\,\ref{fgg}} & \mbox{with $f,g$
replaced by $e*0, e*1$, respectively).}\\
\vdots\\
(e * 1) + -(e * 1) &=& e * 0 & \mbox{(transitivity)}\\
(e * 1) + -(e * 1) &=& 0 & \mbox{(inverse for $+$)}\\
0 &=& (e * 1) + -(e * 1) & \mbox{(symmetry)}\\
0 & = & e*0 & \mbox{(transitivity)}\\
\hline
\end{array}
\]
\end{figure}

The axioms of Table~\ref{eqaxarith} are so fundamental that they have a
special mathematical name: {\em the commutative ring axioms}.  Any set of
elements with $+, *, -$ operations satisfying these axioms is called a
{\em commutative ring}.  In addition to \integers, other examples of
commutative rings are the real numbers, $\reals$, the complex numbers,
$\complex$, and the integers modulo $n$ (for $n > 1$).

\problem\label{e1e}

\subproblem
Show that $\provable -e = -1 * e$.

\subproblem
Show that  $\provable\ 1 =  -1 * -1$.

\problem\label{athm} Define the set of {\em Arithmetic Equational Theorems} (aet's)
inductively as follows:
\begin{itemize}
\item every equational axiom of arithmetic is an aet.
\item if all the antecedents of a standard equational inference rule are
aet's,  then so is the consequent.
\end{itemize}
Prove that the set of equationally provable aeq's equals the set of aet's.

\problem
%
For arithmetic expressions $e,f$ and variable $x$, the {\em substitution},
$\subst{e}{x}{f}$, of $f$ for $x$ in $e$ is defined by induction on $e$:
\newcommand{\op}{{\it op}}
\begin{eqnarray*}
\subst{x}{x}{f} &=& f,\\
\subst{c}{x}{f} &=& c \quad \mbox{for any constant or variable, $c$, distinct from } x,\\
\subst{(-e_{0})}{x}{f} &=&  -(\subst{e_{0}}{x}{f}),\\
\subst{(e_{0}\ \op\ e_{1})}{x}{f} &=&  \subst{e_{0}}{x}{f}\ \op\ \subst{e_{1}}{x}{f},
\quad \mbox{where \op\ $\in\{+,*\}$}\ .
\end{eqnarray*}

\subproblem Prove that
\[
\provable f = g \mbox{  implies  } \provable\ \subst{e}{x}{f} =
\subst{e}{x}{g}.
\]

\subproblem
Prove that
\[
\provable e = g \mbox{  implies  } \provable\ \subst{e}{x}{f} =
\subst{g}{x}{f}.
\]



\problem
Repeat Problem~\ref{e1e}, using the results of the previous two problems
to simplify the argument.

\smallskip

The validity of the distributivity axiom---Lemma~\ref{dist-lem}---followed
directly from the distributivity of the integers and definition of the
value of an ae.  It is equally easy to see that all the other equational
axioms of arithmetic of Table~\ref{eqaxarith} are valid as well.

A rule of inference is {\em validity-preserving} if the consequent of the
rule is valid whenever all its antecedents are valid.  For example, it
follows directly from the symmetry of mathematical equality, that the
(symmetry) inference rule of our formal equational proof system is
validity-preserving.  Clearly all the standard equational inference rules
of Table~\ref{steqrules} are also validity-preserving.  As a consequence,
we have:

\begin{theorem}
({\em Soundness})
\[
\provable e = f \quad \mbox{implies} \quad \models e = f.
\]
\end{theorem}

\begin{proof}
Immediate by induction on the definition of arithmetic equational
theorems given in Problem~\ref{athm}, using the fact that the
inference rules are validity-preserving.
\end{proof}


\section{Canonical Forms}  The only numerals defined to occur in
aeq's are {\tt 0} and {\tt 1}---not {\tt 2}, {\tt 3}, \ldots.  We don't
need these other numerals since there are expressions for them, e.g.,
\Code{(1 + 1)} is an expression whose meaning is the integer two.  It {\em
is} useful to have a standard expression, or {\em canonical form}, for
every integer:
\begin{definition}
For integers $n \geq 0$ define ae's $\hat{n}$ and $\widehat{-n}$ inductively:
\begin{itemize}
\item $\hat{0} = {\tt 0}$,
\item $\widehat{n+1} = \Code{(1 + $\hat{n}$)}$,
\item $\widehat{-(n+1)} = \Code{((-1) + $\widehat{-n}$)}$
\end{itemize}
\end{definition}

For example, 
\begin{eqnarray*}
\hat{3} & \mbox{ is } & \Code{(1 + (1 + (1 + 0)))},\\
\widehat{-2} & \mbox{is} & \Code{((-1) + ((-1) + 0))}.
\end{eqnarray*}


\problem Prove that $\mean{\hat{n}}{V} = n$ for all $n \in \integers$ and
valuations $V$.

\problem

\subproblem Show that $\provable \Code{(1 + $\hat{n}$)} = \widehat{n+1}$ for all $n
\in \integers$.
\subproblem Show that $\provable \Code{((-1) + $\hat{n}$)} = \widehat{n-1}$ for all $n
\in \integers$.
\subproblem Show that $\provable \Code{($\hat{n}$ + $\hat{m}$)} = \widehat{n + m}$ for all $m,n
\in \integers$. (hint: Induction on magnitude of $n$.)
\subproblem Show that $\provable \Code{($\hat{n}$ * $\hat{m}$)} = \widehat{n \times m}$ for all $m,n
\in \integers$.
\subproblem Show that $\provable \Code{(-$\hat{n}$)} = \widehat{-n}$ for all $n.
\in \integers$.
\subproblem\label{ecanon}  Let $e$ be an arbitrary ae in which there are no occurrences of
variables.  Conclude that for all
valuations $V$,
\[
\provable e = \widehat{\mean{e}{V}}.
\]
(hint: Structural induction on $e$.)



\begin{lemma}
(Completeness for Constant Expressions) Let $e,f$ be ae's in
which there are no occurrences of variables.  Then
\[
\models e = f \quad \mbox{implies} \quad \provable e = f.
\]
\end{lemma}

\begin{proof}
Choose some fixed valuation $V$.  From $\models e = f$, we have
$\mean{e}{V} = \mean{f}{V} = n$ for some $n \in \integers$.
By~\ref{ecanon}, part~(f), $\provable e = \hat{n}$ and $\provable f =
\hat{n}$, so $\provable e = f$ by symmetry and transitivity.
\end{proof}

The usual canonical form for a polynomial in $x$ is
\[c_{n}x^{n} + c_{n-1}x^{n-1} + \ldots + c_{0}\]
where the leading coefficient $c_{n}$ is nonzero.  We use instead the
``sparse'' canonical form
\[c_{n_{1}}x^{n_{1}} + c_{n_{2}}x^{n_{2}} + \ldots + c_{n_{k}}x^{n_{k}}\]
where $n_{1} > n_{2} > \ldots$ and {\em all} coefficients are nonzero.  We
generalize to more than one variable by treating, for example, a polynomial
in variables $y$ and $x$ as a polynomial in $y$ with coefficients which
are polynomials in $x$.  Here is the precise definition:

\begin{definition}
For any ae $e$ and integer $n \geq 1$, let $e^{1} ::= e$ and $e^{n+1} ::=
\Code{($e$ * $e^{n}$)}$.

Let $L$ be a sequence of distinct variables.  An {\em $L$-canonical arithmetic
expression of degree $d\geq 0$} is defined by induction on the length of
$L$:
\begin{itemize}
\item if $L$ is empty, then the $L$-canonical ae's of degree 0 are
precisely the ae's of the form $\hat{n}$ for $n \in \integers$.  In this
case, there are no $L$-canonical ae's of positive degree.

\item if $L$ begins with the variable $x$ and $L'$ is the rest of $L$,
then the $L$-canonical ae's of degree $d$ are defined by induction on $d$:

\begin{itemize}
\item the $L$-canonical ae's of degree 0 are the $L'$-canonical ae's (no
matter what their degrees).

\item The $L$-canonical ae's of degree $d+1$ are those ae's of the form
\[
\Code{(($a$ * $x^{d+1}$) + $c$)}
\]
where $a \neq {\tt 0}$ is an $L'$-canonical form (of any degree) and $c$
is an $L$-canonical form of degree $\leq d$.
\end{itemize}
\end{itemize}
\end{definition}



\problem
Describe an $x,y,z$-canonical form with the same meaning as $((x +
(\widehat{-3} * y^{2})) + z^{3})^{2}$.



\begin{theorem}\label{Lcanon}
Let $e$ be an arithmetic expression and $L$ a sequence of distinct
variables including all the variables occurring in $e$.  Then there is
an $L$-canonical form $c$ such that $\provable e = c$.
\end{theorem}

\begin{proof}
(Sketch) First prove by induction on $d$ that the sum of an $L$-canonical
form of degree $d$ and any $L$-canonical form is provably equal to an
$L$-canonical form.  Use this to prove that a product of two $L$-canonical
forms, as well as the negative of an $L$-canonical form, is provably equal
to an $L$-canonical form.  Then proceed by structural induction on $e$.
\end{proof}

\begin{lemma}\label{cneqd}
If $c$ and $d$ are syntactically distinct $L$-canonical forms for some
$L$, then $\mean{c} \neq \mean{d}$.
\end{lemma}

\begin{proof}
(Sketch) By induction on the length of $L$.  The induction step uses the
fact that if $p,q$ are polynomials in the same variable, $x$, with real
number coefficients, then if the degree of $p$ is greater than that of
$q$, or they have the same degree and the absolute value of the leading
coefficient of $p$ is greater than that of $q$, then the absolute value of
$p$ is greater that the absolute value of $q$ for all large enough values
of $x$.
\end{proof}

\begin{theorem}
(Completeness)  For all ae's $e,f$,
\[
\models e = f \quad \mbox{implies} \quad \provable e = f.
\]
\end{theorem}

\begin{proof}
Let $L$ be a sequence of distinct variables including all the variables
occurring in either of $e$ or $f$.  By Theorem~\ref{Lcanon}, $\provable e
= c$ and $\provable f = d$ for some $L$-canonical forms $c,d$.  By
Soundness, we have $\mean{e} = \mean{c}$ and $\mean{f} = \mean{d}$.  Now
if $\models e = f$, then $\mean{e} = \mean{f}$, so $\mean{c} = \mean{d}$.
Then by Lemma~\ref{cneqd}, $c$ and $d$ must be syntactically identical, so
we really have $\provable e = c$ and $\provable f = c$, from which
$\provable e = f$ follows by symmetry and transitivity.
\end{proof}



\problem
Let $e$ be an ae and $L$ a sequence of distinct variables including all
the variables in $e$.  Show that there is a {\em unique} $L$-canonical
form $c$ such that $\provable e = c$.


The development above extends easily to arithmetic
expressions over the {\em real numbers} simply by allowing valuations in
which the values of variables may be real numbers.  (For uniformity, we
keep the syntax unaltered, so the only numbers definable by variable-free
ae's are still the integers.)  We say an aeq $e = f$ is {\em valid over
the reals},
\[
\models_{\reals} e = f,
\]
iff it holds for all real-valued valuations.  Since we are now considering
two notions of validity---over the reals and over the integers---we'll use
the notation $\models_{\integers}$ for $\models$ when it is helpful to
emphasize our original notion of validity.


\problem\label{real=}
Prove that
\[
\models_{\reals} e = f \quad \mbox{iff} \quad \models_{\integers} e = f.
\]


\section{Arithmetic Inequalities}

We can extend our formal proof system to include arithmetic {\em in}equalities.

\begin{definition}
An {\em arithmetic inequality\/} (aineq) is an expression of the form \Code{($e$
<= $f$)} where $e$, $f$ are ae's.  The aineq is {\em true} at
valuation $V$, written
\[
V \models \Code{($e$ <= $f$)}
\]
iff $\mean{e}V \leq \mean{e}V$.  The equation is {\em valid}, written
\[
\models \Code{($e$ <= $f$)}
\]
iff it is true at all valuations, that is, iff $\mean{e} \leq \mean{f}$.
\end{definition}

As we did with equations, we will stop using teletype font for formal
symbols like {\tt <=} which appear in aineq's, writing them instead as
ordinary mathematical symbols, e.g., ``$\leq$.''  Some additional formal
inference rules for proving inequalities are given in Table~\ref{ineq}.

\begin{table}[h]
\caption{Inference Rules for Inequalities. \label{ineq}}\small
\[\begin{array}{|c|} \hline
\\
\prooftree
    e = f
\justifies
    e \leq f
\using
    \mbox{($\leq$-reflexivity)}
\endprooftree
\quad
\prooftree
    e \leq f, \quad f \leq e
\justifies
    f = e
\using
    \mbox{($\leq$-antisymmetry)}
\endprooftree
\quad
\prooftree
     e \leq f, \quad f \leq g
\justifies
    e \leq g
\using
    \mbox{($\leq$-transitivity)}
\endprooftree\\
\\
\prooftree
    e \leq f
\justifies
    e + g \leq f + g
\using
    \mbox{($+$-$\leq$-congruence)}
\endprooftree
\quad
\prooftree
    e \leq f, \quad 0 \leq g
\justifies
    e * g \leq f * g
\using
    \mbox{($*$-$\leq$-congruence)}
\endprooftree
\quad
\prooftree
    e \leq f
\justifies
    -f \leq -e
\using
    \mbox{($-$-$\leq$-congruence)}
\endprooftree\\
\\
0 \leq 1 \quad\mbox{($01$-axiom)}\\
\\ \hline
\end{array}\]
\end{table}

We now have two proof systems, the original one for equality with the
rules in Tables~\ref{steqrules} and~\ref{eqaxarith}, and the extension of
this system by the rules for inequalities in Table~\ref{ineq}.  We'll use
the notations $\provable_{=}$ and $\provable_{\leq}$ when it's useful to
emphasize the relevant proof system.



\problem Completeness for constant inequalities. \label{ineqcomp}

\subproblem Show that $n \leq m$ iff $\provable_\leq\ \Code{($\hat{n}$ <= $\hat{m}$)}$.

\subproblem Conclude that if 
$e,f$ are ae's with no occurrences of variables, then
\[
\models e \leq f \quad \mbox{implies} \quad \provable_\leq\ e \leq f.
\]



By Problem~\ref{ineqcomp}, we know that $\provable_{\leq}$ is complete for
inequalities between aeq's without variables.  Given our success in
finding a complete proof system for arithmetic equalities over the
integers even if variables do occur, we might hope to achieve the same
thing for inequalities.

However, there are some notable contrasts between equations and
inequations.  For example, Problem~\ref{real=} reveals that the same
equations are valid whether we consider meanings over the integers,
$\integers$, or the real numbers, $\reals$.  In fact, exactly the same
equations are valid over the complex numbers, $\complex$.  Not so for
inequations.  For example, let $\reals^{+}$ denote the positive real
numbers.  The complex numbers can be partially ordered by the relation,
$\ltecom$, where $c \ltecom d$ iff $d - c \in \reals^{+}\union \{0\}$.  If
we interpret the symbol $\leq$ to mean the relation \ltecom, then we have:
\begin{eqnarray*}
\models_{\integers} 0 & \leq & e * e,\\
\models_{\reals} 0 & \leq & e * e, \mbox{   but}\\
\notmodels_{\complex}\ 0 & \leq & e * e.
\end{eqnarray*}

This remark implies a limitation of the proof rules for
$\provable_{\leq}$, namely:

\begin{lemma}(Incompleteness for $\provable_\leq$)
There is an arithmetic inequality which is valid over the integers but not
$\provable_\leq$-provable, namely,
\begin{eqnarray*}
\models_{\integers} 0 & \leq & x * x,\\
\notprovable_{\leq}\ 0 & \leq & x * x.
\end{eqnarray*}
\end{lemma}

\begin{proof}
All the rules of $\provable_\leq$ are validity-preserving over the complex
numbers with $\leq$ interpreted as \ltecom, so an inequality which is not
valid over the complexes cannot be provable.
\end{proof}

This particular discrepancy between validity and provability can be
regarded an oversight in the design of our proof system.  We could repair
it simply by adding the ``missing'' inequality as an axiom.  That is, if
we define $\provable_2$ to have the rules of $\provable_{\leq}$ along with
the axiom $0 \leq e * e$, then the resulting proof system remains sound
over the integers (though not any more over the complexes partially
ordered by \ltecom).  Now, of course, the formerly missing inequality is
immediately $\provable_2$-provable.

But $\provable_2$ is also incomplete over the integers.
\begin{lemma}(Incompleteness for $\provable_2$)
There is an arithmetic inequality which is valid over the integers but not
$\provable_2$ provable, namely,
\begin{eqnarray*}
\models_{\integers} e & \leq & e * e,\\
\notprovable_2\ x & \leq &  x * x.
\end{eqnarray*}
\end{lemma}

\begin{proof}
All the rules of $\provable_2$ are validity-preserving over the
real numbers, so the inequality $x \leq  x * x$, which is not valid
over the reals, cannot be provable.
\end{proof}

Now we might similarly define $\provable_3$ to have the rules of
$\provable_2$ along with the further rule $e \leq e * e$.  At this point,
it is no longer so easy to show incompleteness for $\provable_3$.  On the
other hand, neither is there an apparent reason to expect $\provable_3$ to
be complete for integer inequalities.

Nevertheless, we can be sure that $\provable_3$ is {\em not} complete.
One of the great mathematical results of the Twentieth Century implies
that {\bf there is {\em no} sound, complete proof system for arithmetic
inequalities over the integers}.  In fact, given a proof checking program
for any sound proof system for integer inequalities, it is possible to
construct, from the text of the checking program, a valid inequality which
has no proof recognizable by the checker!  This is one of the consequences
of G\"odel's Incompleteness Theorem and Matiyasevich's negative solution
to Hilbert's Tenth Problem\footnote{cf. {\em Hilbert's Tenth Problem},
Yuri V. Matiyasevich, MIT Press, c. 1993, 264 pp.}, topics which we take
up later.

\problem For discussion: We have explained that, given any proof checking
program for a sound proof system for arithmetic inequalities over the
integers, we can construct a valid inequality which has no proof in the
system.  But if the inequality has no proof, how can we possibly know it
is valid?

\end{document}
