\documentclass[11pt,twoside]{article}	
\usepackage{latex-macros/course}

\renewcommand{\coursecopyrightnames}{Prof.~Albert~R.~Meyer}
%\renewcommand{\coursecopyrightyear}{2002}

\newtheorem{method}{Method}
\newcommand{\posints}{\integers^+}

\begin{document}
\lecturenotes{1}{Proofs}

\section{What is a Proof?}

A proof is a method of ascertaining truth.  But what constitutes a proof
differs among fields.

\begin{description}

\item[Jury Trial] \emph{Legal} truth is ascertained by twelve people selected at
random.

\item[Word of God] \emph{Religious} truth is ascertained by communication with
God, perhaps via a third party.

\item[Word of Authority] \emph{Authoritative} truth is ascertained by a
trusted person or organization.

\item[Experiment] \emph{Scientific} truth is hypothesized, and the
hypothesis is confirmed or refuted by experiments.

\item[Sampling] \emph{Probable} truth is obtained from statistical
analysis of sample data.  For example, public opinion is ascertained by
polling a small random sample of people.

\item[Inner Conviction/Mysticism] \emph{Personal} truth may come from some
inexplicable belief.

\item[``I don't see why not...'']  Truth by \emph{benefit of doubt} comes
from claiming something is true and then shifting the burden of proof to
anyone who disagrees.

\item[``Cogito ergo sum''] \emph{Philosophical} proof often involves
reasoning about undefined terms.

This Latin quote translates as ``I think, therefore I am.'' It comes from
the beginning of a famous essay by the 17th century
Mathematician/Philospher, Ren\'e Descartes and is one of the most famous
quotes in the world: do a web search on the phrase and you will be flooded
with hits.

Deducing your existence from the fact that you're thinking about your
existence is a pretty cool starting axiom.  However, with just a few more
lines of proof in this vein, Descartes
\href{http://www.btinternet.com/~glynhughes/squashed/descartes.htm}{goes
on} to conclude that there is an infinitely beneficent God.  This ain't
Math.
\end{description}

Mathematics also has a specific notion of ``proof.''

\begin{definition*}
A \emph{formal proof} of a \emph{proposition} is a chain of \emph{logical
deductions} leading to the proposition from a base set of \emph{axioms}.
\end{definition*}

The three key ideas in this definition are highlighted: proposition,
logical deduction, and axiom.  Each of these terms is discussed in a
section below.

\iffalse The last section contains some examples of complete proofs.\fi

\section{Propositions}

\begin{definition*}
A {\em proposition} is a statement that is either true or false.
\end{definition*}

This definition sounds very general, but it does exclude sentences
such as, ``Wherefore art thou Romeo?'' and ``Give me an A!''.

But not all propositions are mathematical.  For example, ``Albert
R. Meyer's wife's name is `Irene' '' happens to be true, and could be
proved with legal documents and testimony of their children, but it's not
a mathematical statement.  That Albert deeply loves his wife is also true,
but neither Albert nor Irene are sure exactly what that means (though it's
important to them both they continue trying to prove it).  Of course this
ain't Math either.

Mathematically meaningful propositions must be about well-defined
mathematical objects like numbers, sets, functions, relations, \etc, and
they must be stated using mathematically meaningful terminology, like
`AND' and `FORALL'.  It's best to illustrate this with a few examples
about numbers and planar maps that are all mathematically meaningful.

\begin{proposition}
2 + 3 = 5.
\end{proposition}

This proposition is true.

\begin{proposition}
Let $p(n) \eqdef  n^2 + n + 41$.
\[
\forall n \in \naturals\; p(n) \text{ is a prime number}.
\]
\end{proposition}

The symbol $\forall$ is read ``for all''.  The symbol $\naturals$ stands for
the set of {\em natural numbers}, which are 0, 1, 2, 3, \dots (ask your
TA for the complete list).  A {\em prime} is a natural number greater than
one that is not divisible by any other natural number other than 1 and
itself, for example, 2, 3, 5, 7, 11, \dots.

Let's try some numerical experimentation to check this proposition:
$p(0) = 41$ which is prime.  $p(1) = 43$ which is prime.  $p(2) = 47$
which is prime.  $p(3)=53$ which is prime. \dots $p(20) = 461$ which is
prime.  Hmmm, starts to look like a plausible claim.  In fact we can keep
checking through $n=39$ and confirm that $p(39)=1601$ is prime.

But if $n = 40$, then $p(n) = 40^2 + 40 + 41 = 41 \cdot 41$, which is not
prime.  Since the expression is not prime {\em for all}\/ $n$, the
proposition is false!  In fact, it's not hard to show that \emph{no}
nonconstant polynomial can map all natural numbers into prime numbers.
The point is that in general you can't check a claim about an infinite set
by checking a finite set of its elements, no matter how large the finite
set.  Here are two even more extreme examples:

\begin{proposition}
$a^4 + b^4 + c^4 = d^4$ has no solution when $a, b, c, d$ are positive
integers.  In logical notation, letting $\posints$ denote the positive
integers, we have
\[
\forall a \in \posints\forall b \in \posints\forall c \in \posints\forall
d \in \posints\; a^4 + b^4 + c^4 \neq d^4.
\]
\end{proposition}

Strings of $\forall$'s like this are usually abbreviated for easier reading:
\[
\forall a, b, c, d \in \posints\; a^4 + b^4 + c^4 \neq d^4.
\]

Euler (pronounced ``oiler'') conjectured this 1769.  But the proposition
was proven false 218 years later by Noam Elkies at a liberal arts school
up Mass Ave.  He found the solution $a = 95800, b = 217519, c = 414560, d
= 422481$.

\begin{proposition}
$313 (x^3 + y^3) = z^3$ has no solution when $x, y, z\in\naturals$.
\end{proposition}

This proposition is also false, but the smallest counterexample has
more than 1000 digits!

\begin{proposition}
Every map can be colored with 4 colors so that adjacent\footnote{Two
regions are adjacent only when they share a boundary segment of positive
length.  They are not considered to be adjacent if their boundaries meet
only at a few points.} regions have different colors.
\end{proposition}

This proposition is true and is known as the ``four-color theorem''.
However, there have been many incorrect proofs, including one that stood
for 10 years in the late 19th century before the mistake was found.  An
extremely laborious proof was finally found in 1976 by mathematicians
Appel and Haken who used a complex computer program to categorize the
four-colorable maps; the program left a couple of thousand maps
uncategorized, and these were checked by hand by Haken and his
assistants---including his 15-year-old daughter.  There was a lot of
debate about whether this was a legitimate proof: the argument was too big
to be checked without a computer, and no one could guarantee that the
computer calculated correctly, nor did anyone have the energy to recheck
the four-colorings of thousands of maps that was done by hand.  Finally,
about five years ago, a humanly intelligible proof of the four color
theorem was found (see
\href{http://www.math.gatech.edu/~thomas/FC/fourcolor.html}
{http://www.math.gatech.edu/~thomas/FC/fourcolor.html}).
\footnote{The story of the four-color proof is told in a well-reviewed
recent popular (non-technical) book: ``Four Colors Suffice.  How the Map
Problem was Solved.'' \emph{Robin Wilson}.  Princeton Univ. Press, 2003,
276pp. ISBN 0-691-11533-8.}

\begin{proposition}[Goldbach]
Every even integer greater than 2 is the sum of two primes.
\end{proposition}

No one knows whether this proposition is true or false.  This is the
``Goldbach Conjecture,'' which dates back to 1742.


\begin{proposition}
The original Pentium chip divided properly.
\end{proposition}

Intel's ``proofs'' by authority and by sampling turned out to be
invalid.  The proposition is false.

The Intel Chip is a physical device, not a mathematical object, so this
last proposition is not really a mathematical one.  But because we know
how to define the circuit elements and connections, and have a precise
mathematical model of circuit behavior, we can make propositions about the
chip mathematically meaningful.  But the circuit model is a mathematical
abstraction of physical behavior, and is never \emph{exactly} right, so a
proposition about the mathematical model of the chip may be true, but turn
out not to predict chip behavior very well.  This would be a failure of
the modelling, not the Math.  It is actually amazing how well our
mathematical models of chips and other electrical phenomena predict real
physical behavior.

For a Computer Scientist, some of the most important questions are about
program and system ``correctness'' -- whether a program or system does
what it's supposed to.  Programs are notoriously buggy, and there's a
growing community of researchers and practitioners trying to find ways to
prove program correctness.  These efforts have been successful enough in
the case of CPU chips that they are now routinely used by leading chip
manufacturers to prove chip correctness and avoid mistakes like the Intel
division bug.

There has been less success in developing ways to prove program
correctness, in part because programs are usually written in languages
like C++ that are huge, complicated, messy, and hard to model
mathematically in a manageable way.  Computer operating systems are even
larger and messier, and so are even less amenable to comprehensive
mathematical analysis.  Even so, it has in many cases been useful to
formulate simplified models of programs and systems and then prove
correctness their using these models.  Developing such mathematical
methods to verify programs and systems is an active research area.  We'll
consider some of these methods later in the course.


\iffalse

THE NEXT TWO SECTIONS 'Axioms' & ' Logical Deductions' SHOULD BE REPLACED
BY A DISCUSSION OF ``formal proof systems'' consisting of axioms and
rules.  Skip the discussion of the consistency of nonstandard axioms.
Emphasize he ste-by-step checkability of formal proof

\fi

\section{Axioms}


\begin{definition*}
An {\em axiom} is a proposition that is assumed to be true.
\end{definition*}

There is no proof that an axiom is true; you just assume it is true
because you believe it is reasonable.  Here are some examples:

\begin{axiom}
If $a = b$ and $b = c$, then $a = c$.
\end{axiom}

This seems very reasonable!  But sometimes the right choice of axiom
is not clear.

\begin{axiom}[Euclidean geometry]
Given a line $l$ and a point $p$ not on $l$, there is exactly one line
through $p$ parallel to $l$.
\end{axiom}

\begin{axiom}[Spherical geometry]
Given a line $l$ and a point $p$ not on $l$, there is {\em no} line
through $p$ parallel to $l$.
\end{axiom}

\begin{axiom}[Hyperbolic geometry]
Given a line $l$ and a point $p$ not on $l$, there are {\em infinitely
many} lines through $p$ parallel to $l$.
\end{axiom}

No one of the three preceding axioms is better than the others; all
yield equally good proofs.  Of course, a different choice of axioms
makes different propositions true.  Still, a set of axioms should not
be chosen arbitrarily.  In particular, there are two basic properties
that one would want in any set of axioms; it should be consistent and
complete.

\begin{definition*}
A set of axioms is \emph{consistent} if no proposition can be proven to be
both true and false.
\end{definition*}

This is an absolute must.  One would not want to spend years proving a
proposition true only to have it proven false the next day!  Proofs
would become meaningless if axioms were inconsistent.

\begin{definition*}
A set of axioms is {\em complete} if it can be used to prove or
disprove every proposition.
\end{definition*}

Completeness is an attractive property; we would like to believe that
any proposition could be proven or disproven with sufficient work and
insight.

Surprisingly, making a complete, consistent set of axioms is not easy.
Bertrand Russell and Alfred Whitehead tried during their entire
careers to find such axioms for basic arithmetic and failed.  Then
Kurt G\"{o}del proved that no set of axioms can be both consistent and
complete!  This means that any set of consistent axioms (an absolute
must) can not be complete; there will be true statements that can not
be proven.  For example, it might be that Goldbach's conjecture is
true, but there is no proof!

In 6.042 we will not worry about the precise set of axioms underpinning
our proofs.  The requirements are only that you be upfront about what you
are assuming, that the background knowledge of Math that you assume is
self-consistent, and that you do not try to avoid homework and exam
problems by declaring everything an axiom!

\section{Logical Deductions }

Logical deductions or \emph{inference rules} are used to combine axioms
and true propositions to construct more true propositions.

A fundamental inference rule is \emph{modus ponens}.  This rule says that
if $p$ is true and $p \implies q$ is true, then $q$ is true.  The
expression $p \implies q$ is read ``$p$ implies $q$'' or ``if $p$, then
$q$.''  A truth table for $\implies$ is shown below:

\[
\begin{array}{c|c|c}
p & q & p \rightarrow q \\ \hline
T & T & T \\
T & F & F \\
F & T & T \\
F & F & T 
\end{array}
\]

\iffalse
In this table, $T$ stands for ``true'' and $F$ stands for ``false''.
Note that if $p$ is false, then $p \Rightarrow q$ is always true.  For
example, any statement beginning, ``If pigs fly, then ...'' is
true!
\fi

Inference rules are sometimes written in a funny notation.  For example,
\emph{modus ponens} is written:
\begin{rul*}
\Rule{p, \quad p \implies q}{q}
\end{rul*}

When the statements above the line, called the \emph{antecedents}, are
true, then we can infer that the statement below the line, called the
\emph{conclusion} or the \emph{consequent}, is also true.  There are many
other natural inference rules, for example:
\begin{rul*}
\Rule{p \implies q, \quad q \implies r}{p \implies r}
\end{rul*}

\begin{rul*}
\Rule{p \implies q, \quad \neg q}{\neg p}
\end{rul*}

Rosen describes additional standardized inference rules useful in proofs.
As with axioms, we will not be too formal about the set of legal inference
rules.  Each step in a proof should be clear and ``logical''; in
particular, you should state what previously proved facts are used to
derive each new conclusion.

\iffalse

\section{Examples of Proofs}

The first two examples are simple; the last two are more tricky.

\subsection{Direct Proofs}

\begin{theorem}[DeMorgan's Law]
For any sets $A$ and $B$, $\overline{A \cup B} = \overline{A} \cap
\overline{B}$.
\end{theorem}

The usual way to prove that two sets are equal is to show that each is
a subset of the other.  This means that the proof will have two parts.

\begin{method}
To prove $R = S$, show $R \subseteq S$ and $S \subseteq R$.
\end{method}

\begin{proof}
First, we will show $\overline{A \cup B} \subseteq \overline{A} \cap
\overline{B}$.  We do this by showing that any element of the left
side set is also in the right side set.

Let $x$ be any element of $\overline{A \cup B}$.  This implies that
$x$ is not an element of the complementary set, $A \cup B$.
Therefore, $x$ is contained in neither $A$ nor $B$.  Since $x$ is not
contained in $A$, it must be contained in the complementary set,
$\overline{A}$.  Similarly, since $x$ is not contained in $B$, it must
be contained in $\overline{B}$.  We now know $x \in \overline{A}$ and
$x \in \overline{B}$.  These facts imply that $x$ is contained in the
intersection $\overline{A} \cap \overline{B}$.  We have shown that any
element of the left side set is also in the right side set.  This
proves that $\overline{A \cup B} \subseteq \overline{A} \cap
\overline{B}$.

Second, we will show $\overline{A} \cap \overline{B} \subseteq
\overline{A \cup B}$.  We will use the same style of argument for the second
part of the proof; in fact, we will argue in reverse.

Let $x$ be any element of $\overline{A} \cap \overline{B}$.  This
implies that $x$ is an element of $\overline{A}$ and an element of
$\overline{B}$.  Since $x$ is an element of $\overline{A}$, it can not
be an element of the complementary set $A$.  Similarly, since $x$ is
an element of $\overline{B}$, it can not be an element of $B$.  We now
know that $x \notin A$ and $x \notin B$.  These facts imply that $x$
is not contained in the union $A \cup B$.  This implies that $x$ is
contained in the complementary set $\overline{A \cup B}$.  Again, we
have shown that any element of the left side set is contained in the
right side set.  This proves that $\overline{A} \cap \overline{B}
\subseteq \overline{A \cup B}$.

Since each of the two sets is contained in the other, the two sets
must be equal.
\end{proof}
This is tedious!  But this is the way to prove statements like this
directly from the definitions of the ``Boolean'' set-theoretic
operators union ($\cup$), intersection ($\cap$), and complement.

Actually, there is another way to prove such propositions about sets under
the set-theoretic operations.  We can
translate the set-theoretic equality into a Boolean formula involving
truth-valued variables under the corresponding Boolean operations $\land$,
$\lor$, and $\neg$ and then use truth-tables to check that the Boolean
formula is valid.  So the set-theoretic DeMorgan's law can be reduced to a
truth-table verification of the truth-value version of DeMorgan's Law:

\begin{theorem}[De Morgan]
For any Boolean variables $x$ and $y$,
\[
\neg(x \lor y) \equiv (\neg x \land \neg y).
\]
\end
{theorem}



A Boolean variable is one that is true/false or, equivalently, 0/1.  The
symbol $\equiv$ is read ``if and only if'' and is sometimes also written
``iff'' or $\Leftrightarrow$.  A statement of the form $S \Leftrightarrow R$ holds
provided $S$ is true exactly when $R$ is true.  A common mistake when
writing proofs with iff statements is to forget the only if part and to
only go one way, for example, to show only $S \implies R$.

\begin{method}[truth table method]
To prove a statement about a small number of Boolean variables, make a
truth table and check all the possible cases.
\end{method}

\begin{proof}\text{EDIT FOR DEMORGAN}
\[
\begin{array}{c|c|c|c}
x & y & x \rightarrow y & \neg y \Rightarrow \neg x \\ \hline
T & T & T & T \\
T & F & F & F \\
F & T & T & T \\
F & F & T & T
\end{array}
\]

\end{proof}

\subsection{Proofs by Contradiction}

The two preceding examples are {\em direct proofs}.  In a direct
proof, axioms and previously proved theorems are combined until a new
proof is done.  Sometimes an {\em indirect proof} is easier.  This is
also known as a {\em proof by contradiction}.  The idea is to assume
the opposite of what we are trying to prove and try to derive a
falsehood or contradiction.  Then we can conclude that the assumption
was false.  More formally, we have the following method.

\begin{method}[Proof by Contradiction]
To prove that $p$ is true, we prove that $\neg p \Rightarrow False$.
\end{method}

We can verify the validity of this technique by the truth table
method:

\[
\begin{array}{c|c|c}
p & \neg p & \neg p \Rightarrow False \\ \hline
T & F & T \\
F & T & F \\
\end{array}
\]

The table shows that $p$ is true iff $\neg p \Rightarrow False$.

A good example of proof by contradiction is the proof that $\sqrt{2}$ is
irrational (given in Lecture 1 Slides, and also in Rosen).
\fi



\section{Good Proofs and Bad Proofs}

\iffalse
THE ISSUE HERE IS ``real'' mathematical proofs that appear in texts or are
used by professional mathematicians versus formal proof.  NEEDS TO BE MADE
CLEARER.
\fi

Even the best scholarly Math journals sometimes publish papers containing
serious errors,
\iffalse An estimated 1/3 of all mathematical papers contain errors.\fi
and some of the world's most famous mathematicians have botched up their proofs.
Here are some famous examples:

\begin{itemize}

\item Gauss's 1799 Ph.D. thesis is usually referred to as being the
first rigorous proof of the Fundamental Theorem of Algebra (every
polynomial has a zero over the complex numbers).  But it contains
quotes like
\begin{quote}
  "If a branch of an algebraic curve enters a bounded region, it must
   necessarily leave it again. ... Nobody, to my knowledge, has ever
   doubted [this fact].  But if anybody desires it, then on another
   occasion I intend to give a demonstration which will leave no
   doubt."
\end{quote}
Fields Medalist Steve Smale writes about this, calling it an "immense
gap" in the proof that was not filled in until 1920, more than a
hundred years later.

\item In 1900 Poincare carelessly claimed a certain very simple
topological characterization of the 3-dimensional sphere.  Later
realizing it was not so obvious, he demoted the claim to the status of
a "conjecture" in 1904.  The Poincare Conjecture is now one of the
biggest open questions in mathematics (two Fields Medals have been
given out for partial progress on it).

\item In the 1990's, Andrew Wiles recently announced a proof of Fermat's
Last Theorem.  It was several hundred pages long.  It took mathematicians
months of hard work to discover it had a fatal flaw. Then Wiles ans some
coolaborators produced another proof of several hundred pages which has
finally convinced the experts.

\end{itemize}


Here are some of the characteristics of a good proof:

\iffalse MORE SIGNIFICANT POINT to be made here is that real proofs are
not formal.  What a real proof is depends on the prior knowledge of
audience, so it evolves, \eg proofs that would be considered thorough &
convincing by the end of the term wouldn't be accepted at the beginning of
the term.  So in this course we won't try to say exactly what a good proof
is, but will explain by showing lots of examples of good, and bad, proofs.
\fi


\begin{itemize}

\item It is clear and \emph{correct}!

\iffalse
%If only :-)   -- ARM

\item It is elegant; surprisingly short or clever.  Like a ``nice
hack'' in code.

\fi

\item It has a nice structure, like a good program.  It is broken up
into separate parts
\iffalse
\footnote{The correct plural of ``lemma'' is
undeniably ``lemmata'', but users of the latter term often die young
from mysterious... accidents.}
\fi
that define and prove key intermediate properties.
This makes it easy to understand the reason the whole thing works.  It
also makes it more likely that pieces can be reused.

\item The pieces are general and abstract.  This avoids the clutter of
unnecessary hypotheses, useless restrictions, \etc.  Again, the analogy to
programming holds: a subroutine is more valuable if it is generally enough
to be useful in other applications.

Of course the original proofs of historically important theorems have
typically been long and messy, like those of Appel \& Haken and of Wiles,
but no less important for that weakness.  Sometimes it's taken centuries
for the abstractions to be formulated that lead to simple proofs; the Law
of Large Numbers in probability theory is an example of this that we'll
see in detail towards the end of the term.

\item Important conclusions are not ``justified'' by being ``left to the
reader,'' nor by intimidating phrases like ``it is obvious that\dots'' or
``any moron can see that\dots.''  These phrases save the writer's time,
but consume the reader's time.  Mistakes in proofs are typically found in
these parts ``left to the reader.''

\item Like a scientific experiment, someone else must be able to
``replicate'' (i.e. understand) your proof.

\end{itemize}

Proofs are important.  They permit you to convince yourself and others
that your reasoning is correct.  The insights gained can help you
understand why something is true and whether it will stay true when other
things change.  In Computer Science and Electrical Engineering, proofs
have the potential to save time, money, and lives.  The problem is that
they are often hard to find.  In this course, we'll introduce you to some
of the ways that proofs can be found.

\iffalse
Bugs have proven costly for Intel, AT\&T, and Airbus.  A good proof is
strong evidence that no bugs exist.
\fi

\end{document}
