Re: What is a proof, exactly?

From: Ryan Reich (ryanr_at_uchicago.edu)
Date: 11/22/04 

Date: Mon, 22 Nov 2004 10:40:23 -0600

Jasper Stein wrote:
> Dear mathematicians,
>
> For my Ph.D. work in automated reasoning I am investigating formalised
> linear algebra. In automated reasoning one tries to capture mathematical
> definitions, theorems as well as mathematical reasoning in (computerised)
> formal systems, notably type theories.
>
> However, due to several technical difficulties formalising linear algebra I
> have begun wondering what exactly it means to have a proof of a theorem. I
> hope to have answers to this question from a number of mathematicians
> unspoilt by the automated reasoning community. Could you please comment on
> this main question ("what is a proof?")?

Disclaimer: I'm still a student, albeit a student in a logic class. Thus the
below constitutes somewhat more of my own opinion than the typical answer to
this question might be expected to.

Strictly speaking, a proof is a sequence of logical formulas proceeding
according the the rule of deduction: if A -> B and A both appear, then we can
write B; else we cannot, unless B is one of two special kinds of formulas,
either a logical axiom or an axiom of our model. The logical axioms are just a
bunch of statements which are "tautologically true" or "valid", in a sense that
you would be better served by a textbook than by myself to clarify; their exact
composition is sort of arbitrary but they tend to be chosen to capture our
intuition about what should consist in a deduction. And the axioms of the model
are just a collection of formulas which we are allowing to be "true", where this
word really just means we can put them in deductions for free.

No one actually writes these, obviously. It's very painful. In mathematical
logic one encounters "metatheorems" which say when you can conclude that a
deduction _could_ be given, if you so desired, so that you can avoid having to
write down the entire thing, but only logicians use those either. General
mathematicians tend to write "convincing arguments" which fill in the really
important logic with something resembling the metatheorems and otherwise present
credible evidence that another mathematician familiar with the material and with
logic would be able to use to convince himself (or herself) that a proof exists.
  (Those readers who believe otherwise are invited to try to understand some of
the proofs in Hartshorne's _Algebraic Geometry_, which although an excellent
book only maintains its slim figure through a regimen of extreme exercise of the
reader's brain.) A real proof is explicitly defined to require no intelligence
on the part of the reader at all: everything is either obviously a logical
axiom, obviously an axiom of our model, or obviously follows from two previous
statements by deduction.

> There are a number of related questions that may be worth taking into
> account as well, such as:
>
> - What did Wiles do when he proved Fermat's theorem? What do we mean by
> saying "The Riemann Hypothesis is proved."? What do we need to do to make
> it so?

I don't know anything about Wiles' proof other than that he didn't prove
Fermat's Last Theorem literally. He instead proved a conjecture which had in
turn been shown already to imply Fermat's Last Theorem, which by deduction is of
course just as good. I likewise have no idea whether his proof approaches the
logical ideal more closely than just being "convincing"; I would imagine it does
given the monumental amount of peer review it is supposed to have endured.

I don't know about you, but many of us mean "no" when we say "The Riemann
Hypothesis is proved". Jokes aside, it probably means much the same thing that
Wiles' proof does: a proof of some other theorem which logically implies the RH.

> - What does it mean to say that Euler (was it?) proved $e^{i\pi} = -1$? How
> is (in this case) proof different from computation?

This is an interesting case, actually, since he probably proved it using power
series manipulations which were totally unjustifiable at the time. That is, he
plugged "ix" into the argument of the exponential function, wrote out the
series, separated out the even and odd terms, and observed that he had trig
functions. There is no guarantee that such a trick works without first proving
something about convergent power series of complex numbers, and complex analysis
wasn't really initiated for another century. So in this case the proof really
was a computation. This is not to say that computations do not constitute valid
proofs; if the theorem is something like "The Euler characteristic of the sphere
is 2", then assuming you have proven that your definition of the Euler
characteristic is equivalent to the one Euler used with vertices, edges, and
faces of polyhedra, then the proof is quite easy and consists of literally
writing down the numbers. Of course, it does rest on that other proof, unless
of course you are using Euler's definition.

> - Why could I not prove -say- that the set of natural numbers is as large
> as the set of reals? How does the falseness of this come into play? Why
> couldn't I prove -say- the generalised continuum hypothesis either, even
> though it isn't false in any sense? (or is it? why?)

Well, the short answer is that you cannot prove it because it is false, and that
implication is given by the soundness theorem of first-order logic. Only true
things are provable, where "true" means true in a given logical system. The
definition of that is a little hazy; in the class I'm taking, it is defined to
mean something like "A logical statement is true if when you translate it into
English, it's true of any model of that system", which for obvious reasons I
never liked. One way to look at it is that the soundness theorem (and its
converse, Godel's completeness theorem) show that logical proof completely
captures our idea of logical truth and therefore we don't have to worry about
the "intuitive" truth of a statement because if it's there, we can prove it
somehow. Another thing, of course, to be careful of is that our axioms for set
theory might be inconsistent (which Godel's incompleteness theorem says we can't
know) and in that case we _would_ be able to prove that the natural numbers and
the real numbers have the same cardinality...and everything else, as well.

> - Does the extremely simple theorem "5=5" need a proof? Why (not)?

Yes and no. "x = x" is an axiom and any generalization of an axiom (obtained by
inserting universal quantifiers in front) is an axiom, so it is but a short
proof to get "5 = 5" literally. No one would write it. We don't even really
think of "x = x" as being fundamentally different from "5 = 5", in the sense
that neither x nor 5 is given a distinguished role in the context of these
sentences so that they are interchangeable. On the other hand, even the logical
axioms "need" proofs, which are one line long.

> - How is a proof different from just an explanation? Is there a difference
> at all?

Well, I had that paragraph above which touches on this. A teacher explaining a
subject to students is not proving anything, but rather developing their
intutions about math so that, when the time comes to give proofs, the
symbol-shuffling which constitutes a real logical proof can be avoided and a
"convincing argument" can be given in its place. On the other hand, the
convincing argument is itself an explanation of why the author thinks a proof
exists; if you read it enough you come to understand it as well as the author
did, and then you can skip the proof as well.

> - What is the status of "=" (equality) with respect to proofs? Is there a
> difference between "meaning of" and "definition of"? Is "=" defined or does
> it only have a (logical) meaning? Can we equate any two mathematical
> objects?

Well, first-order logic does give a preferential status to that symbol over the
other relational symbols, in that it appears in the axioms and is not up for
interpretation. I would say that in the context of logic both definition and
meaning are subjective and appropriate only to the metatheory which resides in
the head of the reader; as far as proofs are concerned things are what they look
like, and are to be interpreted only insofar as the interpretations follow
logically from the axioms or deduction. There is another way to insert
interpretations into logic, which is as a "model" of a set of logical
statements, namely a set in which each logical symbol corresponds to a function
or relation or element of the set, so that a logical sentence is translated into
a composition of these things concatenated with logical connectives like -> or
"for all", and this sentence is either true or false (or totally undecidable, of
course)...but again, this judgement is made by a person. Mathematical logic is
strictly a formal system which tries to capture this subjective quality.

> - What does it mean to say that we have two different proofs of theorem T?

It means there are two different deductions, that's all.

> - How is a mathematical proof different from a mathematical object? Are the
> derivations from -say- predicate logic (where one talks about e.g.
> "&-introduction" or "quantifier elimination") or from sequent calculus the
> same things as 'normal' proofs? Or are they, rather, mathematical objects
> themselves? Or are they somewhere in between?

I'll have to bow out of this one, since I am not experienced enough to talk
about these ideas.

> - Suppose we defined an object X. Then we state a theorem Thm. about X,
> which we subsequently prove by a proof prf. According to the main school(s)
> of mathematics, what is the ontological status of X, Thm, and prf? Does Thm
> 'exist' in the same sense as X 'exists'? Does prf 'exist' in the same sense
> as Thm?

I would say that prf exists just as much as X does, namely as a set of formulas
just as X is a set of somethings. Thm is likewise a formula. If you want to
know what a formula is, well, you will eventually hit a dead end when you need
to define symbols and sequences and the like, but then, you need to know what a
set is to define X. The basics are all equally real, which is to say as real as
our imagination allows us to believe that some primitive notion of a set is real.

> - Once we defined X as above, we can make additional definitions Y, Z, ...
> depending on X. Can we also make definitions depending on Thm? On prf? Can
> you comment on the definition of the reciprocal ($x \to \frac{1}{x}$),
> which seems to depend not only on $x$ but also on a 'theorem' stating that
> $x \neq 0$? Does it also depend on a proof of such a theorem? How?

In what way does the definition of X allow us to make additional definitions?
In the sense that the existence of X is a logical statement with logical
consequences, this is perhaps true (of course, that's not a first-order
concept). Another way to look at it is that Y and Z depend on certain logical
non-axioms in addition to the axioms, and if X satisfies those axioms then,
having convinced ourselves that X is our universe of the day, we will accept Y
and Z as well. That is a first order statement, and it really just says that
the any model of Y's axioms is also a model of X's. Since Thm is just a
formula, one can easily make a definition based on it by taking any other
formula which includes Thm as a part such that the truth of the other is
dependent on the truth of Thm. Prf is another matter; formulas do not have
independent truth or falsity; our logical axioms were just preferences. It
would not be a first-order statement to discuss the existence of Prf (it would
probably be a second-order statement, but then you would have proofs of proofs
and you haven't really answered the question. And probably never will).
However, the actual nature of Prf is irrelevant, since its existence is the
verification that Thm is provable, and conversely the provability of Thm is (by
definition) the existence of Prf. And we can deal with Thm.

> - The proof of the four colour theorem is controversial, since it depends
> on a piece of computer code. What is the problem with that?

It's not convincing, of course. It's very hard to say whether a big (= hundreds
of pages) of code is logically correct, or whether a typo really has it proving
something other than it claims to.

> - This code calculated and checked a few thousands of 'configurations'. If
> these calculations and the checking were done by mathematicians, would the
> proof be still as controversial? Why (not)?

Probably not, but then, they would have to write all that out, which was the
point of using the program. It is a step up in the hierarchy of "convincing
argument" which has yet to be fully integrated into our methods. If they wrote
it all out then humans would have confidence that humans could reproduce the
proof, and since as I've indicated that I belive, proofs are eventually based on
human ideas about how to determine truth.

> - Suppose aliens gave us a pack of paper, full of english text and
> mathematical symbols, ending in "... and hence the Riemann Hypothesis is
> proved. QED." Suppose also that this text was so intricate and so involved
> and so convoluted that no one would be able to understand it in full. Does
> this pack of paper constitute a proof?

If a tree falls in a forest, and no one witnesses it in any way, did it fall? I
would say yes. But theorems aren't trees; if a logical statement is consistent
with the axioms then (by the completeness theorem) there exists a proof, and the
production of that proof does not change its logical status. All it does is
change our knowledge of it, and it's the part where we believe that the RH is
true not because we'd like to, but because it has been shown to be the case by
methods we also believe to be the perfect embodiment of our intuition, that is
important to us. If aliens give us an incomprehensible proof it's no good; and
if the four-color theorem's proof is incomprehensible, that's no good either.
Even if it's true. Of course, if I understand it and you don't, I can feel free
to use it (provided my understanding indicates it's true, of course), whereas
you would warily agree that my manipulation of the logical symbols is correct,
there is one spot in my proofs that needs further verification.

> I suppose that's enough questions for the time being. Feel free to include
> any pertinent thoughts and additional questions.

Let the tearing down of my amateurish responses begin! 

-- 
Ryan Reich
ryanr@uchicago.edu

Relevant Pages
Loading