[FOM] What are foundations for?

[Martin Davis]

This a list devoted to Foundations of Mathematics. But looking at the
proliferating ongoing discussion of various foundations as moderator, I
have the sense that much of it is at cross purposes.  I would like to make
some distinctions that I hope may be helpful.

1. To begin with one seeks a foundation simply to avoid an infinite
regress. Mathematicians establish their results by providing a proof that
reasons from known propositions. So a foundation provides a basis from
which all the rest follows. This is what first Frege and then
Whitehead-Russell were attempting. The modern concept came to the fore of a
foundation consisting of basic propositions and purely combinatorial rules
of inference.

2. Now it became possible to use mathematical methods to study foundations
in the sense of 1. Post and Hilbert initiated this kind of work. It led to
a new outlook in which the limits of what a given fixed foundation could
reach became apparent. This was already seen in Skolem's discovery that
countable models can't be eliminated even when within the formalism one can
prove things about  non-countable structures. Then Gödel's work on
incompleteness and the on the consistency of the continuum hypothesis
opened up a huge field of study. Already there can be a clash between
foundations with the utter simplicity that is most desirable from the point
of view of such study and those that in the interest of intuitive clarity
avoid artificial constructions. (Of course equivalence proofs are readily
available.)

3. With the development of modern computers, a foundation can be made to
serve the practical purpose of providing a tool for verifying the
correctness of proofs (or even of searching for proofs). This field has
advanced enormously over the very early work that I with Hilary Putnam, Don
Loveland, and George Logemann did so long ago. Designing such a system must
be approached as a problem is software engineering. Questions to be decided
include:  What hardware will it run on? Will it be designed to verify any
proofs from any part of mathematics, or will it be more specific? Will it
be designed to verify only constructive proofs? There is no reason why any
such system should be best in all situations. Arguing about whether types
should be built in, about whether natural numbers should be defined in
terms of sets or simply be a given type, are implementational matters that
are not to be settled on theoretical grounds. And there is no reason why
any one such implementation will be best for all mathematical uses.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160411/de409ef5/attachment-0001.html>