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

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

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

\section{What is a Proof?}
A \hyperdef{proofs}{what}{proof} is a method of establishing truth.  What
constitutes a proof differs among fields.

\begin{itemize}

\item \emph{Legal} truth is ascertained by a jury based on
allowable evidence presented at trial.

\item \emph{Authoritative} truth is ascertained by a trusted person or
organization.

\item \emph{Scientific} truth\footnote{Actually, only scientific
\emph{falsehood} can be demonstrated by an experiment, when the experiment
fails to behave as predicted.  But no amount of experiment can confirm
that the \emph{next} experiment won't fail.  For this reason, scientists
rarely speak of truth, but rather of \emph{theories} that accurately
predict past, and anticipated future, experiments.} is ascertained by
experiment.

\item \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 \emph{Philosophical} proof involves careful exposition and persuasion
based on consistency and plausibility.  The best example is ``Cogito ergo
sum,'' a Latin sentence that translates as ``I think, therefore I am.''  It
comes from the beginning of a 17th century essay by the
Mathematician/Philospher, Ren\'e Descartes, and it 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 and persuasive-sounding first 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{itemize}

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.  In the next sections, we'll discuss these
three ideas along with some basic ways of organizing proofs.

\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'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.

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$.
\hyperdef{proofs}{eqdef}{
\footnote{The symbol $\eqdef$ means
 ``equal by definition.''  It's always ok to simply write ``='' instead of
 $\eqdef$, but reminding the reader that an equality holds by definition
 can be helpful.}}
\[
\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).  The period after the $\naturals$ is just a
separator between phrases.

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}
{\texttt{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.

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 notorious Intel
division bug in the 1990's.

Developing mathematical methods to verify programs and systems remains an
active research area.  We'll consider some of these methods later in the
course.



\section{The Axiomatic Method}

The standard procedure for establishing truth in mathematics was
invented by Euclid, a mathematician working in Alexadria, Egypt around
300 BC.  His idea was to begin with five \textit{assumptions} about
geometry, which seemed undeniable based on direct experience.  (For
example, ``There is a straight line segment between every pair of
points.)  Propositions like these that are simply accepted as true are
called \term{axioms}.

Starting from these axioms, Euclid established the truth of many
additional propositions by providing ``proofs''.  A \term{proof} is a
sequence of logical deductions from axioms and previously-proved
statements that concludes with the proposition in question.  You
probably wrote many proofs in high school geometry class, and you'll
see a lot more in this course.

There are several common terms for a proposition that has been proved.
The different terms hint at the role of the proposition within a
larger body of work.
%
\begin{itemize}
\item Important propositions are called \term{theorems}.
\item A \term{lemma} is a preliminary proposition useful for proving
later propositions.
\item A \term{corollary} is an afterthought, a proposition that follows
in just a few logical steps from a theorem.
\end{itemize}
%
The definitions are not precise.  In fact, sometimes a good lemma
turns out to be far more important than the theorem it was originally
used to prove.

Euclid's axiom-and-proof approach, now called the \term{axiomatic method},
is the foundation for mathematics today.  In fact, there are just a handful
of axioms, called ZFC, which, together with a few logical deduction rules,
appear to be sufficient to derive essentially all of mathematics.

\floatingtextbox{
\textboxtitle{The ZFC Axioms}

For the record, we list the axioms of Zermelo-Frankel Set Theory.
Essentially all of mathematics can be derived from these axioms together
with a few logical deduction rules.
%
\begin{description}

\item[Extensionality.] Two sets are equal if they have the same members.
In formal logical notation, this would be stated as:
\[
(\forall z.\; (z \in x \iff z \in y)) \implies x = y.
\]

\item[Pairing.] For any two sets $x$ and $y$, there is a set,
     $\set{x,y}$, with $x$ and $y$ as its only elements.

\item[Union.] The union of a collection, $z$, of sets is also a set.
%
\[
\exists u \forall x.\; (\exists y.\; x \in y \wedge y \in z) \iff x \in u.
\]

\item[Infinity.]  There is an infinite set; specifically, a nonempty set,
  $x$, such that for any set $y \in x$, the set $\set{y}$ is also a member
  of $x$

\item[Subset.] Given any set, $x$, and any proposition $P(y)$, there is a
  set containing precisely those elements $y \in x$ for which $P(y)$ holds.

\item[Power Set.]  All the subsets of a set form another set.

\item[Replacement.]  The image of a set under a function is a set.
\iffalse
%
\[
\forall w \exists y \forall z (\phi(w,z) \implies z = y)
        \implies \exists y \forall z (
            z \in y \iff \exists w (w \in x \wedge \phi(w,z)))
\]
\fi

\item[Foundation.]  For every non-empty set, $x$, there is a set $y \in x$
such that $x$ and $y$ are disjoint.  (This most technical of the axioms
aims to capture the idea that sets are built up successively from simpler
sets.  In particular, this axiom prevents a set from being a member of
itself.)

\item[Choice.]  We can choose one element from each set in a collection of
  nonempty sets.  More precisely, if $x$ is a set, and every element
  of $x$ is itself a set that is nonempty, then there is a ``choice''
  function, $g$, such that $g(y) \in y$ for every $y \in x$.

\iffalse
 %
\[
\exists y \forall z \forall w (
    (z \in w \wedge w \in x) \implies
    \exists v \exists u (\exists t ((u \in w \wedge w \in t) \wedge
                                       (u \in t \wedge t \in y))
    \iff u = v))
\]
\fi

\end{description}
%
We're \textit{not} going to be working with the ZFC axioms in this
course.  We just thought you might like to see them.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Our Axioms}

The ZFC axioms are important in studying and justifying the foundations of
Mathematics.  But for practical purposes, they are much too
primitive--- by one reckoning, proving that $2 + 2 = 4$ requires more than
20,000 steps!  So instead of starting with ZFC, we're going to take a
\textit{huge} set of axioms as our foundation: we'll accept all familiar
facts from high school math!

This will give us a quick launch, but you \textit{will} find this
imprecise specification of the axioms troubling at times.  For
example, in the midst of a proof, you may find yourself wondering,
``Must I prove this little fact or can I take it as an axiom?''  Feel
free to ask for guidance, but really there is no absolute answer.
Just be upfront about what you're assuming, and don't try to evade
homework and exam problems by declaring everything an axiom!

\subsection{Proofs in Practice}

In principle, a proof can be \textit{any} sequence of logical
deductions from axioms and previously-proved statements that concludes
with the proposition in question.  This freedom in constructing a
proof can seem overwhelming at first.  How do you even \textit{start}
a proof?

Here's the good news: many proofs follow one of a handful of standard
templates.  Proofs all differ in the details, of course, but these
templates at least provide you with an outline to fill in.  We'll go
through several of these standard patterns, pointing out the basic
idea and common pitfalls and giving some examples.  Many of these
templates fit together; one may give you a top-level outline while
others help you at the next level of detail.  And we'll show you
other, more sophisticated proof techniques later on.

The recipes below are very specific at times, telling you exactly
which words to write down on your piece of paper.  You're certainly
free to say things your own way instead; we're just giving you
something you \textit{could} say so that you're never at a complete
loss.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Proving an Implication}
\label{sec:prove_implies}

An enormous number of mathematical claims have the form ``If $P$, then
$Q$'' or, equivalently, ``$P$ implies $Q$''.  Here are some examples:
%
\begin{itemize}

\item (Quadratic Formula) If $a x^2 + b x + c = 0$ and $a \neq 0$,
then $x = \paren{- b \pm \sqrt{b^2 - 4 a c}} / 2a$.

\item (Goldbach's Conjecture) If $n$ is an even integer greater than
$2$, then $n$ is a sum of two primes.

\item If $0 \leq x \leq 2$, then $-x^3 + 4x + 1 > 0$.

\end{itemize}
%
There are a couple standard methods for proving an implication.

\subsection{Method \#1}

In order to prove that $P$ implies $Q$:
%
\begin{enumerate}
\item Write, ``Assume $P$.''
\item Show that $Q$ logically follows.
\end{enumerate}

\subsection*{Example}

\begin{theorem}
If $0 \leq x \leq 2$, then $-x^3 + 4x + 1 > 0$.
\end{theorem}

Before we write a proof of this theorem, we have to do some
scratchwork to figure out why it is true.

The inequality certainly holds for $x = 0$; then the left side is
equal to 1 and $1 > 0$.  As $x$ grows, the $4x$ term (which is
positive) initially seems to have greater magnitude than $-x^3$ (which
is negative).  For example, when $x = 1$, we have $4x = 4$, but $-x^3
= -1$ only.  In fact, it looks like $-x^3$ doesn't begin to dominate
until $x > 2$.  So it seems the $-x^3 + 4x$ part should be nonnegative
for all $x$ between 0 and 2, which would imply that $-x^3 + 4x + 1$ is
positive.

So far, so good.  But we still have to replace all those ``seems
like'' phrases with solid, logical arguments.  We can get a better
handle on the critical $-x^3 + 4x$ part by factoring it, which is not
too hard:
%
\[
-x^3 + 4x^2 = x (2 - x)(2 + x)
\]
%
Aha!  For $x$ between 0 and 2, all of the terms on the right side are
nonnegative.  And a product of nonnegative terms is also nonnegative.
Let's organize this blizzard of observations into a clean proof.

\begin{proof}
Assume $0 \leq x \leq 2$.  Then $x$, $2 - x$, and $2 + x$ are all
nonnegative.  Therefore, the product of these terms is also
nonnegative.  Adding 1 to this product gives a positive number, so:
%
\[
x (2 - x)(2 + x) + 1 > 0
\]
%
Multiplying out on the left side proves that
%
\[
-x^3 + 4x + 1 > 0
\]
%
as claimed.
\end{proof}

There are a couple points here that apply to all proofs:
%
\begin{itemize}

\item You'll often need to do some scratchwork while you're trying to
figure out the logical steps of a proof.  Your scratchwork can be as
disorganized as you like--- full of dead-ends, strange diagrams,
obscene words, whatever.  But keep your scratchwork separate from your
final proof, which should be clear and concise.

\item Proofs typically begin with the word ``Proof'' and end with some
sort of doohickey like $\Box$ or ``q.e.d''.  The only purpose for
these conventions is to clarify where proofs begin and end.

\end{itemize}

\subsection{Method \#2 - Prove the Contrapositive}

An implication (``$P$ implies $Q$'') is logically
equivalent to its \emph{contrapositive} ``not $Q$ implies not $P$'';
proving one is as good as proving the other.  And often proving the
contrapositive is easier than proving the original statement.  If so,
then you can proceed as follows:
%
\begin{enumerate}
\item Write, ``We prove the contrapositive:'' and then state the
contrapositive.
\item Proceed as in Method \#1.
\end{enumerate}

\subsection*{Example}

\begin{theorem}
If $r$ is irrational, then $\sqrt{r}$ is also irrational.
\end{theorem}

Recall that rational numbers are equal to a ratio of integers and
irrational numbers are not.  So we must show that if $r$ is
\textit{not} a ratio of integers, then $\sqrt{r}$ is also \textit{not}
a ratio of integers.  That's pretty convoluted!  We can eliminate both
``not'''s and make the proof straightforward by considering the
contrapositive instead.

\begin{proof}
We prove the contrapositive: if $\sqrt{r}$ is rational, then $r$ is
rational.

Assume that $\sqrt{r}$ is rational.  Then there exists integers $a$
and $b$ such that:
%
\[
\sqrt{r} = \frac{a}{b}
\]
%
Squaring both sides gives:
%
\[
r  = \frac{a^2}{b^2}
\]
%
Since $a^2$ and $b^2$ are integers, $r$ is also rational.
\end{proof}


\section{Proving an ``If and Only If''}
\label{sec:prove_iff}

Many mathematical theorems assert that two statements are logically
equivalent; that is, one holds if and only if the other does.  Here
are some examples:

\begin{itemize}

\item An integer is a multiple of 3 if and only if the sum of its
digits is a multiple of 3.

\item Two triangles have the same side lengths if and only if two
sidelengths an an angle are the same.

\item A positive integer $p \geq 2$ is prime if and only if $1 + (p -
1) \cdot (p - 2) \cdots 3 \cdot 2 \cdot 1$ is a multiple of $p$.

\end{itemize}

\subsection{Method \#1:  Prove Each Statement Implies the Other}

The statement ``$P$ if and only if $Q$'' is equivalent to the two
statements ``$P$ implies $Q$'' and ``$Q$ implies $P$''.  So you can
prove an ``if and only if'' by proving \textit{two} implications:
%
\begin{enumerate}
\item Write, ``We prove $P$ implies $Q$ and vice-versa.''
\item Write, ``First, we show $P$ implies $Q$.'' Do this by one
of the methods in Section~\ref{sec:prove_implies}.
\item Write, ``Now, we show $Q$ implies $P$.''  Again, do this by
one of the methods in Section~\ref{sec:prove_implies}.
\end{enumerate}

\subsection*{Example}

Two sets are defined to be equal if they contain the same elements;
that is, $X = Y$ means $z \in X$ if and only if $z \in Y$.  (This is
actually the first of the ZFC axioms.)  So set equality theorems can be
stated and proved as ``if and only if'' theorems.

\begin{theorem}[Distributive Law for Sets]
Let $A$, $B$, and $C$ be sets.  Then:
%
\[
A \cap (B \cup C) = (A \cap B) \cup (A \cap C)
\]
\end{theorem}

\begin{proof}
We show $z \in A \cap (B \cup C)$ implies $z \in (A \cap B) \cup (A
\cap C)$ and vice-versa.

First, we show $z \in A \cap (B \cup C)$ implies $z \in (A \cap B)
\cup (A \cap C)$.  Assume $z \in A \cap (B \cup C)$.  Then $z$ is in
$A$ and $z$ is also in $B$ or $C$.  Thus, $z$ is in either $A \cap B$
or $A \cap C$, which implies $z \in (A \cap B) \cup (A \cap C)$.

Second, we show $z \in (A \cap B) \cup (A \cap C)$ implies $z \in A \cap
(B \cup C)$.  Assume $z \in (A \cap B) \cup (A \cap C)$.  Then $z$ is
in both $A$ and $B$ or else $z$ is in both $A$ and $C$.  Thus, $z$ is
in $A$ and $z$ is also in $B$ or $C$.  This implies $z \in A \cap (B
\cup C)$.
\end{proof}

\subsection{Method \#2:  Construct a Chain of Iffs}

In order to prove that $P$ is true if and only if $Q$ is true:
%
\begin{enumerate}
\item Write, ``We construct a chain of if-and-only-if implications.''
\item Prove $P$ is equivalent to a second statement which is
equivalent to a third staement and so forth until you reach $Q$.
\end{enumerate}
%
This method is generally more difficult than the first, but the result
can be a short, elegant proof.

\subsection*{Example}

The \textit{standard deviation} of a sequence of values $x_1, x_2,
\dots, x_n$ is defined to be:
%
\[
\sqrt{(x_1 - \mu)^2 + (x_2 - \mu)^2 + \cdots + (x_n - \mu)^2}
\]
%
where $\mu$ is the average of the values:
%
\[
\mu = \frac{x_1 + x_2 + \cdots + x_n}{n}
\]

\begin{theorem}
The standard deviation of a sequence of values $x_1, \dots, x_n$ is
zero if and only if all the values are equal to the mean.
\end{theorem}

For example, the standard deviation of test scores is zero if and only
if everyone scored exactly the class average.

\begin{proof}
We construct a chain of ``if and only if'' implications.  The standard
deviation of $x_1, \dots, x_n$ is zero if and only if:
%
\[
\sqrt{(x_1 - \mu)^2 + (x_2 - \mu)^2 + \cdots + (x_n - \mu)^2} = 0
\]
%
where $\mu$ is the average of $x_1, \dots, x_n$.  This equation holds
if and only if
%
\[
(x_1 - \mu)^2 + (x_2 - \mu)^2 + \cdots + (x_n - \mu)^2 = 0
\]
%
since zero is the only number whose square root is zero.  Every term
in this equation is nonnegative, so this equation holds if and only if
every term is actually 0.  But this is true if and only if every value
$x_i$ is equal to the mean $\mu$.
\end{proof}

\begin{notesproblem}
Reformulate the proof Distributive Law for Sets as a chain of if-and-only-if
implications.
\end{notesproblem}


\section{How to Write \textit{Good} Proofs}

One purpose of a proof is to establish the truth of an assertion with
absolute certainty.  Mechanically checkable proofs of enormous length or
complexity can accomplish this.  But the most desirable proofs are humanly
intelligible ones that help the reader understand the subject matter.  The
teachers of 6.042 share the view held nearly universally among
Mathematicians that important Mathematical results can't be fully
understood until their proofs are understood, and that is why proofs are
an important part of the 6.042 curriculum.

To be understandable and helpful, more is required of a proof than just
logical correctness: a good proof must also be clear.  Correctness and
clarity are usually complementary; a well-written proof is more likely to
be a correct proof, since mistakes are harder to hide.

In practice, the notion of proof is a moving target.  Proofs in a
professional research journal are generally unintelligible to all but a
few experts who know all the terminology and prior results used, often
without explicit mention, in the proof.  Conversely, proofs in the first
weeks of a beginning course like 6.042 would be regarded as tediously
long-winded by a professional mathematician.  In fact, what we accept as a
good proof later in the term will be different from what we consider good
proofs in the first couple of weeks of 6.042.  But even so, we can offer
some general tips on writing good proofs:

\begin{description}

\item[State your game plan.]  A good proof begins by explaining the
general line of reasoning, e.g. ``We use case analysis'' or ``We argue
by contradiction''.  This creates a rough mental picture into which
the reader can fit the subsequent details.

\item[Keep a linear flow.] We sometimes see proofs that are like
mathematical mosaics, with juicy tidbits of reasoning sprinkled across
the page.  This is not good.  The steps of your argument should follow
one another in a sequential order.

\item[A proof is an essay, not a calculation.]  Many students
initially write proofs the way they compute integrals.  The result is
a long sequence of expressions without explantion.  This is bad.  A
good proof usually looks like an essay with some equations thrown in.
Use complete sentences.

\item[Avoid excessive symbolism.]  Your reader is probably good at
understanding words, but much less skilled at reading arcane
mathematical symbols.  So use words where you reasonably can.

\item[Revise and simplify.]  Your readers will be grateful.

\item[Introduce notation thoughtfully.]  Sometimes an argument can be
greatly simplified by introducing a variable, devising a special
notation, or defining a new term.  But do this sparingly since you're
requiring the reader to remember all that new stuff.  And remember to
actually \textit{define} the meanings of new variables, terms, or
notations; don't just start using them!

\item[Structure long proofs.]  Long programs are usually broken into a
heirarchy of smaller procedures.  Long proofs are much the same.
Facts needed in your proof that are easily stated, but not readily
proved are best pulled out and proved in preliminary lemmas.  Also, if
you are repeating essentially the same argument over and over, try to
capture that argument in a general lemma, which you can cite
repeatedly instead.

\item[Be wary of the ``obvious''.]  When familiar or truly obvious facts
are needed in a proof, it's OK to label them as such and to not prove
them.  But remember that what's obvious to you, may not (and typically is
not) obvious to your reader.

Most especially, don't use phrases like ``clearly'' or ``obviously'' in an
attempt to bully the reader into accepting something which you're having
trouble proving.  Also, go on the alert whenever you see one of these
phrases in someone else's proof.

\item[Finish.]  At some point in a proof, you'll have established all the
essential facts you need.  Resist the temptation to quit and leave the
reader to draw the ``obvious'' conclusion.  Instead, tie everything
together yourself and explain why the original claim follows.

\end{description}

The analogy between good proofs and good programs extends beyond
structure.  The same rigorous thinking needed for proofs is essential
in the design of critical computer systems.  When algorithms and
protocols only ``mostly work'' due to reliance on hand-waving
arguments, the results can range from problematic to catastrophic.  An
early example was the Therac 25, a machine that provided radiation
therapy to cancer victims, but occasionally killed them with massive
overdoses due to a software race condition.  More recently, in August
2004, a single faulty command to a computer system used by United and
American Airlines grounded the entire fleet of both companies--- and
all their passengers!

It is a certainty that we'll all one day be at the mercy of critical
computer systems designed by you and your classmates.  So we really
hope that you'll develop the ability to formulate rock-solid logical
arguments that a system actually does what you think it does!

\section{Propositional Formulas}
It's really sort of
\hyperdef{propform}{english}{amazing}
that people manage to communicate in the English language.  Here are
some typical sentences:
%
\begin{enumerate}
\item ``You may have cake or you may have ice cream.''
\item ``If pigs can fly, then you can understand the Chernoff bound.''
\item ``If you can solve any problem we come up with, then you get an
A for the course.''
\item ``Every American has a dream.''
\end{enumerate}
%
What \textit{precisely} do these sentences mean?  Can you have both
cake and ice cream or must you choose just one dessert?  If the second
sentence is true, then is the Chernoff bound incomprehensible?  If you
can solve some problems we come up with but not all, then do you get
an A for the course?  And can you still get an A even if you can't
solve any of the problems?  Does the last sentence imply that all
Americans have the same dream or might they each have a different
dream?

Some uncertainty is tolerable in normal conversation.  But when we
need to formulate ideas precisely--- as in mathematics--- the
ambiguities inherent in everyday language become a real problem.  We
can't hope to make an exact argument if we're not sure exactly what
the individual words mean.  (And, not to alarm you, but it is
\textit{possible} that we'll be making an \textit{awful lot} of
exacting mathematical arguments in the weeks ahead.)  So before we
start into mathematics, we need to investigate the problem of how to
talk about mathematics.

To get around the ambiguity of English, mathematicians have devised a
special mini-language for talking about logical relationships.  This
language mostly uses ordinary English words and phrases such as
``or'', ``implies'', and ``for all''.  But mathematicians endow these
words with definitions more precise than those found in an ordinary
dictionary.  Without knowing these definitions, you could sort of read
this language, but you would miss all the subtleties and sometimes
have trouble following along.

Surprisingly, in the midst of learning the language of logic, we'll
come across the most important open problem in computer science--- a
problem whose solution could change the world.

\subsection{Combining Propositions}

In English, we can modify, combine, and relate propositions with words
such as ``not'', ``and'', ``or'', ``implies'', and ``if-then''.
For example, we can combine three propositions into one like this:
%
\begin{center}
\textbf{If} all humans are mortal \textbf{and} all Greeks are human,
\textbf{then} all Greeks are mortal.
\end{center}

For the next while, we won't be much concerned with the internals of
propositions--- whether they involve mathematics or Greek mortality---
but rather with how propositions are combined and related.  So we'll
frequently use variables such as $P$ and $Q$ in place of specific
propositions such as ``All humans are mortal'' and ``$2 + 3 = 5$''.
The understanding is that these variables, like propositions, can take
on only the values \true (true) and \false (false).  Such true/false variables
are sometimes called \term{Boolean variables} after their inventor,
George--- you guessed it--- Boole.

\subsubsection{``Not'', ``And'' and ``Or''}

We can precisely define these special words using \term{truth tables}.
For example, if $P$ denotes an arbitrary proposition, then the
truth of the proposition ``not $P$'' is defined by the following
truth table:
%
\[
\begin{array}{c|c}
P & \text{not $P$} \\ \hline
\true & \false \\
\false & \true \\
\end{array}
\]
%
The first row of the table indicates that when proposition $P$ is true,
the proposition ``not $P$'' is false (F).  The second line indicates that
when $P$ is false, ``not $P$'' is true.  This is probably what you would
expect.

In general, a truth table indicates the true/false value of a
proposition for each possible setting of the variables.  For example,
the truth table for the proposition ``$P$ and $Q$'' has four lines,
since the two variables can be set in four different ways:
%
\[
\begin{array}{cc|c}
P & Q & \text{$P$ and $Q$} \\ \hline
\true & \true & \true \\
\true & \false & \false \\
\false & \true & \false \\
\false & \false & \false
\end{array}
\]
%
According to this table, the proposition ``$P$ and $Q$'' is true only
when $P$ and $Q$ are both true.  This is probably reflects the way you
think about the word ``and''.

There is a subtlety in the truth table for ``$P$ or $Q$'':
%
\[
\begin{array}{cc|c}
P & Q & \text{$P$ or $Q$} \\ \hline
\true & \true & \true \\
\true & \false & \true \\
\false & \true & \true \\
\false & \false & \false
\end{array}
\]
%
This says that ``$P$ or $Q$'' is true when $P$ is true, $Q$ is true,
or \textit{both} are true.  This isn't always the intended meaning of
``or'' in everyday speech, but this is the standard definition in
mathematical writing.  So if a mathematician says, ``You may have cake
or you may have ice cream'', then you \textit{could} have both.

\subsubsection{``Implies''}

The least intuitive connecting word is ``implies''.  Mathematicians
regard the propositions ``$P$ implies $Q$'' and ``if $P$ then $Q$'' as
synonymous, so both have the same truth table.  (The lines are
numbered so we can refer to the them later.)
%
\[
\begin{array}{rcc|c}
   & P & Q & \parbox[b]{13ex}{$P$ implies $Q$, \\ if $P$ then $Q$} \\ \hline
1. & \true & \true & \true \\
2. & \true & \false & \false \\
3. & \false & \true & \true \\
4. & \false & \false & \true
\end{array}
\]

Let's experiment with this definition.  For example, is the following
proposition true or false?
%
\begin{center}
``If Goldbach's Conjecture is true, then $x^2 \geq 0$ for every real
number $x$.''
\end{center}
%
Now, we told you before that no one knows whether Goldbach's
Conjecture is true or false.  But that doesn't prevent you from
answering the question!  This proposition has the form $P \implies Q$
where $P$ is ``Goldbach's Conjecture is true'' and $Q$ is ``$x^2 \geq
0$ for every real number $x$''.  Since $Q$ is definitely true, we're
on either line 1 or line 3 of the truth table.  Either way, the
proposition as a whole is \textit{true}!

One of our original examples demonstrates an even stranger side of
implications.
%
\begin{center}
``If pigs fly, then you can understand the Chernoff bound.''
\end{center}
%
Don't take this as an insult; we just need to figure out whether this
proposition is true or false.  Curiously, the answer has
\textit{nothing} to do with whether or not you can understand the
Chernoff bound.  Pigs do not fly, so we're on either line 3 or line 4
of the truth table.  In both cases, the proposition is \textit{true}!

In contrast, here's an example of a false implication:
%
\begin{center}
``If the moon shines white, then the moon is made of white cheddar.''
\end{center}
%
Yes, the moon shines white.  But, no, the moon is not made of white
cheddar cheese.  So we're on line 2 of the truth table, and the
proposition is false.

The truth table for implications can be summarized in words as
follows:
%
\begin{center}
\textit{An implication is true when the if-part is false or the
then-part is true.}
\end{center}
%
This sentence is worth remembering; a large fraction of all
mathematical statements are of the if-then form!

\subsubsection{``If and Only If''}

Mathematicians commonly join propositions in one additional way that
doesn't arise in ordinary speech.  The proposition ``$P$ if and only
if $Q$'' asserts that $P$ and $Q$ are logically equivalent; that is,
either both are true or both are false.
%
\[
\begin{array}{cc|c}
P & Q & P \text{ if and only if } Q \\ \hline
\true & \true & \true \\
\true & \false & \false \\
\false & \true & \false \\
\false & \false & \true
\end{array}
\]
%
The following if-and-only-if statement is true for every real number
$x$:
%
\begin{center}
``$x^2 - 4 \geq 0$ if and only if $|x| \geq 2$''
\end{center}
%
For some values of $x$, \textit{both} inequalities are true.  For
other values of $x$, \textit{neither} inequality is true .  In every
case, however, the proposition as a whole is true.

The phrase ``if and only if'' comes up so often that it is often
abbreviated ``iff''.

\subsection{Propositional Logic in Computer Programs}

Propositions and logical connectives arise all the time in computer
programs.  For example, consider the following snippet, which could be
either C, C++, or Java:
%
\begin{tabbing}
\hspace{1in} \= \quad\quad \= \quad\quad \= \quad\quad \= \kill
\> \texttt{if ( x > 0 || (x <= 0 \&\& y > 100) )} \\
\> \> \vdots\\
\> \> \textit{(further instructions)}
\end{tabbing}
%
The symbol \texttt{||} denotes ``or'', and the symbol \texttt{\&\&}
denotes ``and''.  The \textit{further instructions} are carried out
only if the proposition following the word \texttt{if} is true.  On
closer inspection, this big expression is built from two simpler
propositions.  Let $A$ be the proposition that \texttt{x > 0}, and let
$B$ be the proposition that \texttt{y > 100}.  Then we can rewrite the
condition this way:
%
\hyperdef{AAB}{snippet}{
\[
A \text{ or } ((\text{not } A) \text{ and } B)
\]}
%
A truth table reveals that this complicated expression is logically
equivalent to ``$A \text{ or } B$''.
%
\[
\begin{array}{cc|c|c}
A & B &
    A \text{ or } ((\text{not } A) \text{ and } B) &
    A \text{ or } B \\ \hline
\true & \true & \true & \true \\
\true & \false & \true & \true \\
\false & \true & \true & \true \\
\false & \false & \false & \false
\end{array}
\]
%
This means that we can simplify the code snippet without changing the
program's behavior:
%
\begin{tabbing}
\hspace{1in} \= \quad\quad \= \quad\quad \= \quad\quad \= \kill
\> \texttt{if ( x > 0 || y > 100 )} \\
\> \> \textit{(further instructions)}
\end{tabbing}

Rewriting a logical expression involving many variables in the
simplest form is both difficult and important.  Simplifying
expressions in software might slightly increase the speed of your
program.  But, more significantly, chip designers face essentially the
same challenge.  However, instead of minimizing \texttt{\&\&} and
\texttt{||} symbols in a program, their job is to minimize the number
of analogous physical devices on a chip.  The payoff is potentially
enormous: a chip with fewer devices is smaller, consumes less power,
has a lower defect rate, and is cheaper to manufacture.

\subsection{A Cryptic Notation}

Programming languages use symbols like $\&\&$ and $!$ in place of
words like ``and'' and ``not''.  Mathematicians have devised their own
cryptic symbols to represent these words, which are summarized in the
table below.
%
\begin{center}
\begin{tabular}{ll}
\textbf{English} & \textbf{Cryptic Notation} \\[1ex]
``not $P$'' & $\neg P$ \quad (alternatively, $\overline{P}$) \\
``$P$ and $Q$'' & $P \wedge Q$ \\
``$P$ or $Q$'' & $P \vee Q$ \\
``$P$ implies $Q$'' or ``if $P$ then $Q$'' & $P \implies Q$ \\
``$P$ if and only if $Q$'' & $P \iff Q$
\end{tabular}
\end{center}
%
For example, using this notation, ``If $P$ and not $Q$, then $R$''
would be written:
%
\[
(P \wedge \neg Q) \implies R
\]

This symbolic language is helpful for writing complicated logical
expressions compactly.  But in most contexts ordinary words such as
``or'' and ``implies'' are much easier to understand than symbols such
as $\vee$ and $\implies$.  So we'll use this symbolic language
sparingly, and we advise you to do the same.

\subsection{Logically Equivalent Implications}

Are these two sentences saying the same thing?
%
\begin{center}
If I am hungry, then I am grumpy. \\
If I am not grumpy, then I am not hungry.
\end{center}
%
We can settle the issue by recasting both sentences in terms of
propositional logic.  Let $P$ be the proposition ``I am hungry'', and
let $Q$ be ``I am grumpy''.  The first sentence says ``$P$ implies
$Q$'' and the second says ``(not $Q$) implies (not $P$)''.  We can
compare these two statements in a truth table:
%
\[
\begin{array}{c|c|c|c}
P & Q &
    \text{$P$ implies $Q$} &
    \text{(not $Q$) implies (not $P$)} \\ \hline
\true & \true & \true & \true \\
\true & \false & \false & \false \\
\false & \true & \true & \true \\
\false & \false & \true & \true
\end{array}
\]
%
Sure enough, the two statements are precisely equivalent.  In general,
``(not $Q$) implies (not $P$)'' is called the \term{contrapositive} of
``$P$ implies $Q$''.  And, as we've just shown, the two are just
different ways of saying the same thing.  This equivalence is mildly
useful in programming, mathematical arguments, and even everyday
speech, because you can always pick whichever of the two is easier to
say or write.

In contrast, the \term{converse} of ``$P$ implies $Q$'' is the
statement ``$Q$ implies $P$''.  In terms of our example, the converse
is:
%
\begin{center}
If I am grumpy, then I am hungry.
\end{center}
%
This sounds like a rather different contention, and a truth table
confirms this suspicion:
%
\[
\begin{array}{c|c|c|c}
P & Q &
    \text{$P$ implies $Q$} &
    \text{$Q$ implies $P$} \\ \hline
\true & \true & \true & \true \\
\true & \false & \false & \true \\
\false & \true & \true & \false \\
\false & \false & \true & \true
\end{array}
\]
%
Thus, an implication \textit{is} logically equivalent to its
contrapositive, but is \textit{not} equivalent to its converse.

One final relationship: an implication and its converse together are
equivalent to an if and only if statement, specifically, to these two
statements together.  For example,
%
\begin{center}
If I am grumpy, then I am hungry. \\
If I am hungry, then I am grumpy.
\end{center}
%
are equivalent to the single statement:
%
\begin{center}
I am grumpy if and only if I am hungry.
\end{center}
%
Once again, we can verify this with a truth table:
%
\[
\begin{array}{c|c|c|c}
P & Q &
    \text{($P$ implies $Q$) and ($Q$ implies $P$)} &
    \text{$Q$ if and only if $P$} \\ \hline
\true & \true & \true & \true \\
\true & \false & \false & \false \\
\false & \true & \false & \false \\
\false & \false & \true & \true
\end{array}
\]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\floatingtextbox{
\textboxtitle{SAT}

A proposition is \textbf{satisfiable} if some setting of the variables
makes the proposition true.  For example, $P \wedge \neg Q$ is
satisfiable because the expression is true when $P$ is true and $Q$ is
false.  On the other hand, $P \wedge \neg P$ is not satisfiable
because the expression as a whole is false for both settings of $P$.
But determining whether or not a more complicated proposition is
satisfiable is not so easy.  How about this one?
%
\[
(P \vee Q \vee R) \wedge (\neg P \vee \neg Q)
                  \wedge (\neg P \vee \neg R)
                  \wedge (\neg R \vee \neg Q)
\]

The general problem of deciding whether a proposition is satisfiable
is called \term{SAT}.  One approach to SAT is to construct a truth
table and check whether or not a $\true$ ever appears.  But this
approach is not very efficient; a proposition with $n$ variables has a
truth table with $2^n$ lines.  For a proposition with just 30
variables, that's already over a billion!

Is there an \textit{efficient} solution to SAT?  Is there some
ingenious procedure that \textit{quickly} determines whether any given
proposition is satifiable or not?  No one knows.  And an awful lot
hangs on the answer.  An efficient solution to SAT would immediately
imply efficient solutions to many, many other important problems
involving packing, scheduling, routing, and circuit verification.
This sounds fantastic, but there would also be worldwide chaos.
Decrypting coded messages would also become an easy task (for most
codes).  Online financial transactions would be insecure and secret
communications could be read by everyone.

At present, though, researchers are completely stuck.  No one has a
good idea how to either solve SAT more efficiently or to prove that no
efficient solution exists.  This is the outstanding unanswered
question in computer science.}

\section{Logical Deductions }

Logical deductions or \emph{inference rules} are used to prove new
propositions using previously proved ones.

A fundamental inference rule is \emph{modus ponens}.  This rule says that
a proof of $P$ together with a proof of $P \implies Q$ is a proof of
$Q$.

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
proved, then we can consider the statement below the line, called the
\emph{conclusion} or \emph{consequent}, to also be proved.

A key requirement of an inference rule is that it must be \emph{sound}: any
assignment of truth values that makes all the antecedents true must also
make the consequent true.  So it we start off with true axioms and apply
sound inference rules, everything we prove will also be true.

There are many other natural, sound inference rules, for example:
\begin{rul*}
\Rule{P \implies Q, \quad Q \implies R}{P \implies R}
\end{rul*}

\begin{rul*}
\Rule{\neg{P} \implies Q, \quad \neg{Q}}{P}
\end{rul*}

\begin{rul*}
\Rule{\neg{P} \implies \neg{Q}}{Q \implies P}
\end{rul*}

On the other hand,
\begin{rul*}
\Rule{\neg{P} \implies \neg{Q}}{P \implies Q}
\end{rul*}
is not sound: if $P$ is assigned $\true$ and $Q$ is assigned $\false$, then
the antecedent is true and the consequent is not.

\begin{notesproblem}
Prove that a propositional inference rule is sound iff the conjunction
(AND) of all its antecedents implies its consequent.
\end{notesproblem}

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.

\end{document}
