FOM: certainty

[Andreas Blass]

I feel I should respond to Steve Cook's statement (20 November 98)
that mathematical certainty means provability in an appropriate formal
system, such as ZFC.  The problem seems more difficult, because of
examples and questions like the following.

(1) Consider one of the axioms of ZFC, say the axiom of union.  I
regard it as mathematically certain, and of course it has a (feasible)
proof in ZFC.  But this one-line proof is not at all the reason for my
certainty.  Indeed, I had to be certain about the correctness of this
axiom before accepting ZFC as an appropriate formal system for
establishing facts with mathematical certainty.

(2) As soon as I see that ZFC is appropriate in this sense, i.e., that
I can be certain about the correctness of a statement once I have seen
it proved in ZFC, I also see that the consistency statement Con(ZFC)
is mathematically certain, even though it is not provable in ZFC.  In
other words, I would be foolish to take proofs in ZFC as establishing
mathematical certainty if I were uncertain about the consistency of
ZFC.  [If I were paying attention to feasibility issues, then I should
probably take Con(ZFC) to be the statement that no contradiction is
feasibly provable in ZFC.  Then the preceding comments remain
applicable, as far as I can see, since this feasible version of
Con(ZFC) is presumably not feasibly provable in ZFC.]

(3) In view of (2), the system obtained from ZFC by adding Con(ZFC) as
a new axiom (or by adding similar but stronger reflection principles)
should probably be regarded as also appropriate for establishing
mathematical certainty.  But this idea can be iterated --- add the
consistency statement for the enlarged system, etc.  So I find myself
considering Turing-Feferman-style progressions of theories.  How far
can I take this iteration and still have mathematical certainty for
all propositions proved in such a system?  Presumably I can go up to
any ordinal notations of whose well-foundedness I am mathematically
certain, but then the concepts of "mathematically certain" and
"appropriate formal system" are each explained in terms of the other.
[Trying to make this vicious circle into an induction, I find myself
certain about the well-foundedness of the proof-theoretic ordinal of
ZFC and some more ordinals "predicatively beyond it" --- perhaps the
proof-theorists can make precise what I'm trying to get at here.]

(4) Is Quine's New Foundations an appropriate system for establishing
facts with mathematical certainty?  Of course, once I see something
proved in NF, I am certain that it's true in all models of NF;
unfortunately, I don't know any models of NF.  How about NFU, the
version of NF that allows urelements and is known to have models?  A
proof there gives certainty of truth in all models of NFU, just as for
ZFC (or any other system).  Is this all that's meant by the assertion
that mathematical certainty means provability in an appropriate
system?  Is every (consistent) system appropriate, since certainty is
relative to its class of models?  Or is ZFC deemed appropriate because
it describes the cumulative hierarchy of sets, and this (not some NFU
model) is what we mean when we talk about sets?  I suspect that Steve
Cook had the latter view in mind, since he included the word
"appropriate."  But then, to attain mathematical certainty about a
proposition, we need not only a formal proof of it but also
mathematical certainty that the formal system used is an appropriate
one, i.e., that it accurately describes the cumulative hierarchy of
sets (or whatever other universe of discourse we intend to talk
about).

Because of problems like these, I am very skeptical about using formal
provability as an explanation of what mathematical certainty is.  I
recognize that, once we are certain that a formal system, like ZFC, is
correct, formal deductions in it are a powerful tool for expanding our
certainty to include propositions far less evident than the axioms.
But ultimately I think formal provability must remain a tool, not the
meaning of certainty.

Someone (perhaps everyone) will ask me: What then is the meaning of
mathematical certainty?  I don't know.  I expect that it involves
other concepts --- like "intended meaning" and "understanding" ---
that I also don't know how to make precise.  The only positive comment
I can make about the situation is that "understanding" seems, for many
mathematicians, to be the real objection to the proof of the
four-color theorem.  No matter how thoroughly we check the
calculations, we still haven't understood why the theorem has to be
true (in the way that we understand why the Hahn-Banach theorem has to
be true).

Andreas Blass
Professor of Mathematics 
University of Michigan