[FOM] Mathematical Certainty?
Harvey Friedman
friedman at math.ohio-state.edu
Fri Jun 20 02:32:30 EDT 2003
The recent postings of Taylor and Goodman remind me of a very
interesting foundational issue that is quite multidimensional.
This is the issue of mathematical certainty.
What is the nature of mathematical certainty in theory and in practice?
I wish to concentrate on: what is the nature of mathematical
certainty in practice.
In practice, I am never mathematically certain. For instance, if you
could define, and offer me, a clear bet to the effect that
1. If an inconsistency is found in some particular full formulation
of the exponential function arithmetic within the next 10 years, then
I must immediately undergo surgery, without an anesthetic, to remove
all parts of my body that a board of doctors deem I would live
without.
2. If not, then I get $10,000,000, backed by the full faith and
credit of a dozen U.S. banks plus the U.S. Govt.
then I would hesitate. But why? Isn't this essentially a sure thing?
But in practice, there can always be a mistake. E.g., maybe there is
an error in the axioms and rules of predicate calculus in that
particular full formulation.
###########################
So now let us consider a really complicated piece of mathematics,
like FLT. What kind of certainty is attached to FLT?
And what does certainty mean here? Are we talking about the certainty
that FLT is true, or are we talking about the certainty that the
present published proof of FLT is correct?
The former commits us to a certain level of realism. The latter is
quite ill defined. Under all of our mathematical treatments of what a
mathematical proof is, there are no published proofs in regular
mathematics Journals of any nontrivialities that are even close to
being correct proofs.
The Mizar project, and related automated proof checking projects, are
really the only game in town. They provide the closest examples of
the achievement of certainty through correct proofs that we have.
There is a man/machine interaction, where the man inputs enough
details of the proof in order to get the machine to fill in the
details and verify that everything is perfectly correct. There is a
considerable documented development. Run a search engine on Mizar.
But even here there are a number of intriguing problems.
What about the software behind Mizar? What about the software running
the computers that run Mizar? What about the hardware running the
computers that run Mizar? E.g., the logic and arithmetic circuits?
And do we have to worry about the physics involved?
If we wish to verify the software behind Mizar, then we need software
tools to check that the verification is correct. Don't these tools
need checking, maybe with further tools?
So my question is: can we break out of the loop? Maybe the tools for
the tools for the tools for the tools for the tools might just be
something that we can all stare at directly with great confidence?
A common method is to run programs on several different machines, and
also run programs built by different teams who don't talk to one
another.
What kind of confidence should that give us? Can we use statistics
for this? Is the statistic correct? How is the statistics verified?
In fact, maybe certainty is not even a reasonable notion to be using.
Should we be talking probabilities? If so, how do we compute them?
############################
An obvious retort is: do we care that much? After all, mathematics
like FLT never will command a huge investment from society like
weapons development and cures for major diseases.
That may be the case, but this is an intellectual matter for
interested subscribers of the FOM.
Also, this kind of issue is increasingly relevant in some practical
contexts such as so called critical systems.
And over the very long run, society will want to move towards bug
free infrastructure.
################################
So what is the most interesting question we can dig our teeth into here?
My favorite is that chain that goes back from something like Mizar to
something irreducibly elemental. Can this be set up in practice? This
could provide some serious practical notion of absolutely correct
proof for serious mathematics. Of course, I am thinking of factoring
out the physics of computers, here.
It might be that as one probes deeper back to the irreducibly
elemental, one is fooling oneself - one is actually increasing the
probability of errors, as one has to specify anything before one can
verify anything. So one has to be careful.
I think that this can be done "perfectly", but not without a lot of thought.
Harvey Friedman
More information about the FOM
mailing list