[FOM] Mathematical Certainty?

[Harvey Friedman]

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