\documentstyle[11pt,twoside,prooftree]{article}

\input{macros-course}

\newcommand{\aeval}[2]{{\it val}(#1,#2)}
\newcommand{\mean}[1]{\llbracket#1\rrbracket}
\newcommand{\provable}{\vdash}

\newtheorem{definition}[theorem]{Definition}

\begin{document}

\handout{aeq-notes}{Notes on Proving Arithmetic Equations}{February 22,
1996}

\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}


\begin{definition}
A {\em valuation}, $V,$ is a mapping from the set, {\em Var}, of variable
symbols which may appear in ae's, into the integers, $\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{e}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{xample}
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 \Code{($e_{0}$ =
$f_{0}$)} is {\em not} valid.
\end{xample}

Here is an example of a set of valid equations:

\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 a 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.
\]
\end{proof}

\section{Equational Proofs}

We've been careful so far to distinguish the actual symbols ``\Code{)},
\Code{*},''\ldots in ae's from the mathematical symbols ``{\it )}, $x$,
$e$, $f$'' used to describe ae's.  To keep our notation uncluttered, from
now on we will use less formal descriptions when there is no danger of
ambiguity---in particular, we often will omit parentheses and use one 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
\using
    \mbox{(transitivity)}
\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}

The {\em symmetry rule\/} is similarly described by:
\begingroup
\[
\prooftree
    e = f
\justifies
    f =  e
\using
    \mbox{(symmetry)}
\endprooftree
\]
\endgroup

The {\em congruence rule\/} has one case for each arithmetic operator:
\[
\prooftree
    e = f
\justifies
    -e = -f
\endprooftree
\qquad\qquad
\prooftree
    e_1 = f_1, \quad e_2 = f_2
\justifies
    e_1 + e_2 = f_1 + f_2
\endprooftree
\qquad\qquad
\prooftree
    e_1 = f_1, \quad e_2 = f_2
\justifies
    e_1 * e_2 = f_1 * f_2
\using
    \mbox{\quad(congruence)}
\endprooftree
\]

The {\em reflexive\/} rule is
\[
\prooftree
\justifies
    e = e
\using
    \mbox{(reflexivity)}
\endprooftree
\]

The rules above are called the {\em standard equational inference rules}.

Note that the reflexive rule has no antecedents.  Such rules without
antecedents are usually called {\em axioms} and are simply written as
equations, omitting the horizontal line.

To capture the properties of arithmetic expressions, 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 along with rule name 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} & \mbox{from} & \mbox{Figure~\ref{fgg} with $e*0, e*1$ for $f,g$).}\\
\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}

\begin{problems}
\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
\bparts

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

\ppart
Show that  $\provable 1 =  -1 * -1$.
\eparts
\end{problems}

In Lemma~\ref{dist-lem}, we saw that the validity of the distributivity
axiom followed directly from the distributivity of the integers and
definition of the value of an ae.  It is easy to see that all the other
equational axioms of arithmetic 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.  It is equally easy to see that all the standard
equational inference rules above are validity-preserving.  Thus,


\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~\ref{athm}, using the fact that the
inference rules are validity-preserving.
\end{proof}

\section{Canonical Forms}

\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*}

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

\problem
\bparts
\ppart Show that $\provable \Code{(1 + $\hat{n}$)} = \widehat{n+1}$ for all $n
\in \integers$.
\ppart Show that $\provable \Code{((-1) + $\hat{n}$)} = \widehat{n-1}$ for all $n
\in \integers$.
\ppart Show that $\provable \Code{($\hat{n}$ + $\hat{m}$)} = \widehat{n + m}$ for all $m,n
\in \integers$. (hint: induction on magnitude of $n$.)
\ppart Show that $\provable \Code{($\hat{n}$ * $\hat{m}$)} = \widehat{n \times m}$ for all $m,n
\in \integers$.
\ppart Show that $\provable \Code{(-$\hat{n}$)} = \widehat{-n}$ for all $n.
\in \integers$.
\ppart\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$.)
\eparts
\end{problems}

\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}

\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}

\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}


\begin{problems}

\problem
\bparts
\ppart

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$.

\ppart

Describe the $x,y,z$-canonical form of $((x + (\widehat{-3} * y^{2})) +
z^{3})^{2}$.

\eparts

\problem\label{real=} 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.  Prove that
\[
\models_{\reals} e = f \quad \mbox{iff} \quad \models e = f.
\]
\end{problems}

\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}

We add some additional inference rules for inequalities:
\begingroup
\[
\prooftree
    e = f
\justifies
    e \leq f
\using
    \mbox{($\leq$-reflexivity)}
\endprooftree
\]
\endgroup

\begingroup
\[
\prooftree
    e \leq f, \quad f \leq e
\justifies
    f = e
\using
    \mbox{($\leq$-antisymmetry)}
\endprooftree
\]
\endgroup

\begingroup
\[
\prooftree
     e \leq f, \quad f \leq g
\justifies
    e \leq g
\using
    \mbox{($\leq$-transitivity)}
\endprooftree
\]
\endgroup

\[
\qquad\qquad
\prooftree
    e \leq f
\justifies
    e + g \leq f + g
\endprooftree
\qquad\qquad
\prooftree
    e \leq f, \quad 0 \leq g
\justifies
    e * g \leq f * g
\endprooftree
\qquad\qquad
\prooftree
    e \leq f
\justifies
    -f \leq -e
\using
    \mbox{\quad($\leq$-congruence)}
\endprooftree
\]

\iffalse

\[
\prooftree
    e * g \leq f * g, \quad 1 \leq g
\justifies
    e \leq f
\using
    \mbox{($\leq$-cancellation)}
\endprooftree
\]
\fi

\[0 \leq 1 \quad\mbox{($01$-axiom)}
\]

\begin{problems}

\problem (Completeness for constant inequalities) 
\bparts
\ppart Show that $n \leq m$ iff $\provable \Code{($\hat{n}$ <= $\hat{m}$)}$.

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

\eparts

\end{problems}

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.
We also have two proof systems, the original one for just equality and the
system extended with the rules for inequalities.  We'll use the notations
$\provable_{=}$ and $\provable_{\leq}$ when it's useful to emphasize the
relevant proof system.

In contrast to the situation for equalities, cf.~\ref{real=}, validity of
inequalities over the integers does not agree with validity over the
reals.
For example,
\begin{eqnarray*}
\models_{\integers} 0 & \leq & x * (x + -1),\\
\not\models_{\reals} 0 & \leq & x * (x + -1).
\end{eqnarray*}

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

\begin{proof}
All the rules in our proof system are validity-preserving over the reals,
so an inequality which is not valid over the reals 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 try to
repair it simply by adding the ``missing'' inequality as an axiom.  That
is, if we define $\provable_{xx-1}$ to have the rules of
$\provable_{\leq}$ along with the axiom $0 \leq x * (x + -1)$, then the
resulting proof system remains sound over the integers (though not over
the reals any more).  Now, of course, the formerly missing inequality is
immediately $\provable_{xx-1}$ provable.  This is an {\em ad hoc} repair,
and it would not be surprising if $\provable_{xx-1}$ was itself still
incomplete over the integers.

\iffalse
This time it is possible to show that

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

However, given our success in finding a complete proof system for
arithmetic equalities over the integers, we might hope to achieve the same
thing for inequalities.  One of the great mathematical results of the
Twentieth Century is 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 a consequence of the Undecidability of the Halting
Problem for programs and Matijasevich's negative solution to Hilbert's
Tenth Problem, topics which are taken up in more advanced courses in
Theory of Computation such as 6.044 or 6.045.

\begin{problems}

\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{problems}

\end{document}
