[FOM] foundations meeting/FOMUS/discussion

[Joe Shipman]

Let's make this extremely concrete. I am going to pick two very well-known theorems of different levels of difficulty. Can people who think HoTT is a useful "alternative foundation" for mathematics please say whether or not

(1) the Prime Number Theorem can be rigorously proved using foundations involving HoTT and no set theory without significantly more effort than the standard development  requires, counting effort "from the ground up"

(2) the Fundamental  Theorem of Algebra can be rigorously proved using foundations involving HoTT and no set theory without significantly more effort than the standard development  requires, counting effort "from the ground up"

-- JS


Sent from my iPhone

> On Mar 24, 2016, at 11:13 PM, Bruno Bentzen <b.bentzen at hotmail.com> wrote:
> 
> Harvey Friedman:
> > A FOUNDATION FOR MATHEMATICS
> > There is a standard classical meaning for this. Namely, to provide a
> > precise "workable" rule book for mathematical "activity", that
> > provides suitable criteria for "correctness" or "legitimacy".
> 
> If I am interpreting you correctly, a key aspect of a foundational theory's "philosophical coherence" would be the question - perhaps motivated by Wittgenstein’s famous slogan “meaning is use” - of whether or not it is compatible with the way mathematics is done in practice. In this sense, I think that the set-theoretical approach has some drawbacks.
> 
> It turns out that in practice mathematicians often identify two structures whenever they are isomorphic. This is clearly in conflict with set-theoretic foundational theories such as ZFC, since, for example, if A \cong B and \empty \in A then in general \empty \notin A. 
> 
> Harvey Friedman:
> > I favor the approach of carefully adding a lot of sugar to ZFC, rather
> > than bringing in foreign elements or replacing aspects of ZFC. 
> 
> I believe this issue is not a matter of adding more "sugar" to ZFC or other set theory, it is a limitation of the very set-theoretical framework, since equality, as given by the axiom of extensionality, is a much stronger requirement than isomorphism.
> 
> In contrast, this idea can be embodied within type theory. It is (roughly) the univalence axiom: two structures are equal if they are isomorphic.This is made possible by the fact that type theory, like category theory, has the nice property that every definable predicate of in the system is isomorphic-invariant. Therefore, HoTT admits a structuralist (and constuctivist) foundations of mathematics.
> 
> Harvey Friedman:
> >>> Among the obvious merits of ZFC as a foundation for mathematics, there
> >>> is one that I often see not sufficiently emphasized. That is, its
> >>> PHILOSOPHICAL COHERENCE.
> >>>
> >>> ../..
> >>>
> >>> But my impression is that the more radical proposals, particularly
> >>> HOTT, philosophical coherence is proudly thrown away.
> >
> > That is my understanding, which may or may not be correct. (However,
> > see below for a pointer to an internet manuscript ).This certainly
> > prima facie precludes HOTT as any kind of reasonable "foundation for
> > mathematics" in any standard sense.
> 
> In this respect, I cannot easily understand why HoTT would lack of "philosophical coherence" while ZFC would not.
> 
> I am learning a lot with this great discussion, however, I think we cannot objectively move forward with it since a better clarification of the word "philosophical coherence" is obviously required.
> 
> Bruno Bentzen
> _______________________________________________
> 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/20160325/354d10c9/attachment.html>