[FOM] What are foundations for?

[katzmik at macs.biu.ac.il]

I very much support the kind of pluralism advocated by Martin, and would go
even further and propose the following idea.  An axiom system for set theory
should be treated similarly to an axiom system for group theory.

For various purposes it is useful to vary the list of axioms a group is
supposed to satisfy.  One might decide whether commutativity is a desirable
axiom depending on the purpose one has in mind.  One might wish to enrich the
basic language by the introduction of an order, and speak of ordered groups,
thereby necessitating the introduction of additional axioms.

Mathematicians would generally find it odd if a philosopher came along and
declared that there is one true collection of group axioms, or one true
background model thereof, the others being hypothetical chimeras.

Similarly a case can be made for a variety of axiomatic set theories is a
virtue, and should be used depending on the applications envisioned. Hamkins'
multiverse proposal certainly goes in this direction, resolving in particular
the much-ado-about-nothing over the ontological status of CH (the mathematical
issues involved are of course tremendous).

Harvey Friedman made a proposal a while ago in this direction related to
nonstandard integers.

Edward Nelson proposed a set theory endowed with a richer language for
accomodating procedures usual in mathematical analysis.  This involves the
introduction of a one-place predicate "st", where st(x) reads "x is standard"
(I would have preferred "x is assignable" to follow Leibniz's terminology). 
the resulting axiomatisation of the \in-st-language involves three additional
axioms.  The resulting theory IST is conservative with respect to ZFC.

As far as constructions are concerned, IST has a certain shortcoming that not
every model of ZFC can be built up into a model of IST.  This was overcome by
Hrbacek and Kanovei and found expression in a new theory called BST (B for
"bounded").  The theory BST has the advantage that every model of ZFC can be
built up into a model of IST.

MK

On Mon, April 11, 2016 23:21, Martin Davis wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>