[FOM] alternative foundations?

[Martin Davis]

My impression of this thread is that much of the discussion has been at
cross purposes. Those posting write about "foundations" without first
specifying what a foundation is supposed to be for. Many of the posts have
been concerned with formalisms most suitable for use in computer systems to
which a user can conveniently input a purported mathematical proof that can
then be automatically checked for correctness. Developing such systems is
certainly very worthwhile. (In fact it's a project to which I myself have
contributed long ago.) But it is a project that is quite disjoint from the
tradition in which foundational issues were raised and is quite irrelevant
to either the fascinating achievements stemming from that tradition or to
the compelling problems that remain.

In a talk he gave in 1933 Gödel said:
"... we are confronted by a strange situation. We set out to find a formal
system [of axioms] for mathematics and instead of that found an infinity of
systems, and whichever system you choose ..., there is one ... whose axioms
are stronger. ... ...But ... this character of our systems ... is in perfect
accord with certain facts which can be established quite independently ...
For any formal system you can construct a proposition-in fact a proposition
of the arithmetic of integers-which is certainly true if the given system
is free from contradictions but cannot be proved in the given system. Now
if the system under consideration (call it S) is based on the theory of
types, it turns out that ... this proposition becomes a provable theorem if
you add to S the next higher type and the axioms concerning it. ... the
construction of higher and higher types ... is necessary for proving theorems
even of a relatively simple structure."

It is this vision of formal systems of increasing strength in which more
and more propositions become provable as one ascends the hierarchy that has
provided a remarkably fruitful framework for foundational research. The
program of reverse mathematics has been worked out along some of the bottom
rungs of the ladder. The topic of determinacy takes one very far up the
ladder. For Borel sets Zermelo set theory (that is, without replacement) is
insufficient. To obtain determinacy for all projective sets, one assumes
the existence of sets too large for  their existence to be provable in full
ZFC (so-called "large cardinals") . The program of using projective
determinacy to solve problems in descriptive set theory left open before
such methods were available is a well-known success story.

In addition,the development of formalisms incorporating certain
much-discussed  proposed restrictions of proof methods to those thought
more reliable (constructivity, predicativity) made it possible to
study these ideas in a scientific manner where previously polemical
discussions had dominated the scene.

It was to encourage the discussion and dissemination of  this foundational
tradition that FOM was founded.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140322/e8a56b5e/attachment.html>