[FOM] alternative foundations?

[John Baldwin]

I add one to Joe's questions, prompted by one Martin's observations.

Does the HTT foundation provide a hierarchy of systems? If so, how does it
compare with extensions of ZFC?

John T. Baldwin
Professor Emeritus
Department of Mathematics, Statistics,
and Computer Science M/C 249
jbaldwin at uic.edu
851 S. Morgan
Chicago IL
60607


On Sat, Mar 22, 2014 at 7:25 PM, Joseph Shipman <joeshipman at aol.com> wrote:

> I asked some focused questions to try and channel the discussion
> productively, but they were ignored, so I will try again, because I think
> these questions will prevent talking at cross-purposes.
>
> To the people who had been proposing Homotopy Type theory as an
> alternative foundation:
>
> What percent of mathematical research, in your opinion, could be more
> easily formalized in a system with HTT foundations than in ZFC?
>
> What's a well-known theorem for which HTT foundations makes the result
> much easier to find or prove than ZFC does?
>
> To advocates of ZFC:
>
> What do you think of my analogy between the thesis that all rigorous math
> can be formalized in ZFC and the Church-Turing thesis that all effective
> algorithms can be programmed in Turing Machine language? How does the
> amount of formal detail math authors ought to provide compare with how much
> program code ought to be provided by computer science researchers?
>
> -- JS
>
> Sent from my iPhone
>
> On Mar 22, 2014, at 7:50 PM, Martin Davis <martin at eipye.com> wrote:
>
> 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
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140323/63f50193/attachment.html>