FOM: mathematical certainty

[Stephen Cook]

Here is a reply to Andreas Blass's comments on my working definition
of mathematical certainty as provability in an appropriate formal
system such as ZFC.

It seems to me that any attempt at a formal definition of mathematical
certainty is subject to the kind of attack made by Andreas.  My 
intention was to give a simple operational definition that seems to
apply to current mathematical practice.   For example, when a
mathematician finds a "mistake" in someone's proof, he is pointing
out that the proof exposition cannot be translated into a formal
ZFC proof in any obvious way.  Conversely, all theorems which are
currently considered as "established" by the mathematical community
have proofs that can be formalized in ZFC.

Of course if ZFC is found to be inconsistent, then this definition 
of mathematical certainty would have to be revised.

Steve Cook