FOM: certainty

[Vladimir Sazonov]

Andreas Blass wrote:
>
> 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.

Being a permanent opponent of those who assert existence of 
absolute mathematical truth, I would say that axiom of union is 
certain essentially as much as it is certain that we have 
*intention* to build a set theory where this axiom will be 
postulated or proved. Analogously, the foundation (or 
regularity) axiom of ZFC is certain only until we decide that it 
also makes sense to work in "antifounded" set theory of Aczel. 
(One reason for such a decision may be found "on the Earth", in 
approaching to Web-like databases. Cf. my home page.) The third 
well-known example outside set theory is 5th postulate of Euclid 
geometry.

> (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,

Is "correctness" = "absolute truth" or = "plausibility from some 
intuitive point of view"?

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

Is it really certain the consistency of ZFC? To which degree?  
Is this certainty of the same degree than that when we see a 
correct formal proof in any formal system (even irrespective to 
its consistency)? Is not certainty of the latter much more 
reliable?  Why should we ever mix (inevitably non absolutely 
certain) intuitive meaningfulness or applicability in physics or 
the like of a formal system with the certainty of formal proofs 
in that system? Of course, provability and (informal) truth are 
closely related, but why absolutely? What about, say, heap paradox?

> [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.]

This feasible version of Con(ZFC) should be first formulated!  
To do this we need to introduce some way in ZFC a radically new 
concept of feasibility.

> (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.

I would say that ANY formal system which is believed to be 
contradiction-free (and desirably having some informal meaning) 
is appropriate for establishing of *corresponding* mathematical 
certainty. Again, what is ABSOLUTE 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.]

Really, can any technical proof-theoretic considerations 
drastically resolve any philosophical questions?

> (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.

As to me, I even don't know any models of ZFC or even PA, except 
some informal intuitions behind these theories. (I do not say 
about the technical notion of a model in the model theory.) Some 
intuitions behind formal systems are "better", some are "worse". 
But, what is most important, they are usually very helpful and 
only they make formalisms useful. Do we need anything more? 

> How about NFU, the
> version of NF that allows urelements and is known to have models?

In a technical sense, *relative* to ZFC?

> 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?

Who "WE"? Is this a question for sociology? Should we use voting 
here? It seems that the notion of formal system even understood 
informally (not in a framework of another formal metatheory like 
PA) is much more solid for taking it as the base for 
understanding mathematical certainty than the intuitive and 
therefore inevitably vague notion of cumulative hierarchy of 
sets.

> I suspect that Steve
> Cook had the latter view in mind, since he included the word
> "appropriate."

Why not use here the word "appropriate" in its general sense?  
"Appropriate formal system" is a system which is appropriate by 
*some* reasons, say, by having such and such intuitive or may be 
physical or some other meaning, or appropriate to formalise 
some specific problem. 

> 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).

I would replace in this and the following paragraph all 
occurrences of the word "mathematical" by "extramathematical" 
or, say, by "physical" or by some other word appropriate for the 
formal system considered and the intended "universe of 
discourse". [By the way, if we formally prove in a theory (which 
accurately describes the corresponding universe of discourse) 
that, say, some bridge is reliable, is it absolutely certain 
that it is indeed reliable?] Then, I think, the reason for the 
skepticism expressed in the next paragraph will disappear and 
the only source of *mathematical* certainty will be in formal 
proofs.

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

We cannot and need not make this precise. In particular I really ask:
"what is mathematical certainty *based* on these inherently unclear
concepts?" Why we ever need something more on mathematical certainty
than in formal proofs (based additionally on that or other intuition)?

> 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).

Here I completely agree.


Vladimir Sazonov
-- 			   | Tel. +7-08535-98945 (Inst.),
Computer Logic Lab.,	   | Tel. +7-08535-98953 (Inst.),
Program Systems Institute, | Tel. +7-08535-98365 (home),
Russian Acad. of Sci.	   | Fax. +7-08535-20566
Pereslavl-Zalessky,	   | e-mail: sazonov at logic.botik.ru
152140, RUSSIA		   | http://www.botik.ru/~logic/SAZONOV/