FOM: Certainty and foundationalism in mathematics

[Vladimir Sazonov]

Harvey Friedman wrote:

> 1. Is there a meaningful concept of absolute certainty, beyond which one
> cannot go? And is this ever realized in mathematics? If it is sometimes
> realized in mathematics, then where in mathematics is it realized? Do you
> know of a candidate for a piece of mathematics that is not absolutely
> certain?

Mathematics is as certain as is the concept of rigorous (i.e.  
formal) proof. This certainty is well-known as extremely high, I 
would say, almost absolute. 

What is nevertheless not certain in usual mathematical proofs is 
that it is often not completely clear in which exactly formal 
system these proofs are written.  Say, we use a lot of 
abbreviations which are not *officially* included in usual 
formal systems of underlying predicate logic.  It is intuitively 
evident that all the necessary abbreviation rules participated 
in each concrete proof may be suitably formalized. But we 
usually do not pay sufficient attention to this (even in the 
framework of F.O.M.!). Is there a *complete* system of 
abbreviation rules which are sufficient to write absolutely 
formally all real proofs of contemporary mathematics?  What does 
this completeness mean? Can it be proved as it was proved 
Goedel completeness theorem? 

There are examples of formal(?) proofs of *non-feasible length* 
of shortly formulated theorems. Are they genuine proofs? Or we 
have only a genuine formal proof of a (meta)theorem in another 
formal (meta)theory on existence of an (imaginary) proof? I 
think we should be more careful in answering these questions 
because this may change the traditional (not sufficiently 
precise!) understanding of what is a formal proof, what is a 
consistent/inconsistent/meaningful/meaningless formal system and 
what is its (Tarski?) semantics? Traditional approaches to F.O.M 
completely ignore these, I believe, crucial questions or reduce 
them to also traditional "asymptotic" complexity theoretic 
considerations on estimating the length of proofs. 

Thus, it seems necessary to decide as faithfully as we can, what 
is a rigorous mathematical proof in a formal system (with fixed 
set of axioms and proof rules). 


If so, what is the oldest and/or most elementary example of a
> piece of mathematics that is not absolutely certain? E.g., is the "fact"
> that there is no one-one correspondence between {1,2,3} and {1,2,3,4}
> absolutely certain? And, e.g., is the "fact" that, for all positive
> integers n, there is no one-one correspondence between {1,...,n} and
> {1,...,n+1} absolutely certain?

Strictly speaking, I would not consider these statements as 
objective "facts" of a *mathematical* reality. I know no such a 
*unique* objective reality!  Of course, these statements have 
suitable formalized versions certainly proved in a formal system 
like PA. On the other hand there are corresponding evidently 
true and very certain *facts* for not very large n from our 
*physical* reality.

However, there is also somewhat alternative mathematical 
evidence. For example, there exists a consistent (even in the 
traditional sense!) and sufficiently plausible formal system 
where it is postulated that for some (non-standard) n there 
esists a bijection between "sets" of (1) binary strings of the 
length n, (2) binary strings of the length n+1, (3) all finite 
binary strings (4) all finite unary strings. Moreover, The 
bijection from (4) to (3) (but not vice versa) is polytime 
computable.  By the way, it follows that it is unprovable in a 
version of Bounded Arithmetic that any semideciding algorithm 
for SAT needs exponential time.  (SAT is the problem of 
satisfiability of propositional formulas which is well known to 
be NP-complete.)

Thus, I would assert certainty of axioms and proofs in a formal 
system rather than certainty of any mathematical "facts" as 
such. 

>
> 2. How does the level of certainty in mathematics compare with the level of
> certainty in other disciplines such as physics? E.g., is standard
> elementary school mathematics more certain than standard elementary school
> science?
>
> 3. Does the work in f.o.m. using formal systems and their relationships
> bear on issues of absolute certainty or relative certainty in mathematics?
> Is there any significance of formal systems such as ZFC for the philosophy
> of mathematics?

Yes! No doubts.

> 4. Does Hersh's writings convey any judgment on the value of formal systems
> and the extensive work on them in f.o.m.? If so, what judgment is conveyed
> to his readers? If the answer to 3 is yes, what guidance does Hersh give to
> this extensive literature? Is Hersh under any obligation to give such
> guidance?
>
> 5. What is foundationalism? To what extent is ZFC a formalization of
> mathematics? If one believes that ZFC is, in some appropriate sense, a
> formalization of mathematics, then is one a foundationalist? If one
> believes that ZFC is, in some appropriate sense, a formalization of
> mathematics, then is one an anti-humanist? If one believes that ZFC is, in
> some appropriate sense, a formalization of mathematics, then is one a
> fascist?
> ***********

I have no access to Hersh's book. Thus I cannot judge. It seems 
to me that foundationalism is any attempt to ground all 
mathematics (or whatever) on a *unique* basis. Of course this 
may be tempting and fruitful attempt or, better to say, 
experiment.  Just, it is interesting what happens. What I 
consider suspicious is considering such an attempt too 
seriously, more seriously that it deserves. Say, considering 
(even non explicitly) that everything *ought* to be grounded on 
this unique basis forever. 

As to ZFC, it is a brilliant formalization in the well-known 
sense of seemingly all the *contemporary* mathematics. But what 
about the *future* mathematics? 

The crucial question is "what is mathematics in general?" Let me 
repeat my attempt to define it from my posting to fom from 31 
Aug 1998:

Mathematics is investigating arbitrary MEANINGFUL FORMALISMS. 

(Cf. also my posting to fom from Jan 6.)

Note that both formal system and its informal background or 
meaning are *inseparable* parts. Note, that this in some 
dissonance with Hersh's definition of formalism:

> FORMALISM IN COMMON SPEECH SAYS THAT MATHEMATICS IS JUST FORMULAS
> AND CALCULATIONS.  MEANING IF ANY IS EXTRAMATHEMATICAL.

It is formal system which embody mathematical rigor and 
mathematics does not consider meaningless formalisms and does 
not consider formalisms without relation to their meaning. Also, 
no doubts, formalisms are *creations of peoples*, just specific 
*instruments* (like airplane or computer) helping to reach some 
goals (whatever they are).  Here are no restrictions on 
formalisms considered and no unique privileged formalism or an 
informal unique mathematical world is declared. We may 
temporarily pay more attention to some (imaginary and therefore 
not very certain) mathematical world (like a cumulative universe 
of sets) together with some its (very certain) formalization 
(like ZFC).  Then we may move to some other intuitive world with 
other formalism, etc. Wherefrom it follows that ZFC or some its 
extension is able to absorb any other mathematical 
world/formalism which could arise in a future? Asserting this 
means forbidding in advance any possibility for essentially 
different and possibly useful formalisms (instruments). 


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/