[FOM] alternative foundations?

[Joseph Shipman]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140322/18930a13/attachment.html>