[FOM] New Umbrella?

[David Posner]

I think it's pretty obvious that this discussion is not really about which formal system can formalize what.  I think people are pretty clear about that.  Nor is the discussion about the practicality of the competing systems.  It's ridiculous to believe that the HoTT people have spent all this effort on a system that doesn't make their lives easier.  The discussion is about the religion of mathematics.  The HoTT people will naturally want to claim that HoTT provides a superior FOM.  Just as naturally, people invested in the set theoretic FOM are going to object to this claim.  Jobs are at stake!  Formerly respectable mathematicians might have to become programmers or something awful like that.  Professor Awodey you shouldn't be shocked when the discussion gets a little hot.  What's frustrating is that the proponents of HoTT are beating around the bush trying to reduce the fundamental question about God the Universe and everything to picayune technical
 issues.  So tell us HoTT people: why should mathematicians believe in the HoTT version of the mathematical universe.  In particular why should I want to live in a world without real models?

On Tuesday, October 28, 2014 11:56 AM, Monroe Eskew <meskew at math.uci.edu> wrote:
 




On Oct 27, 2014, at 6:23 AM, Urs Schreiber <urs.schreiber at googlemail.com> wrote:
>
>I started my replies to your question of what the point of HoTT is by
>saying clearly that the point is that some important high-level part
>of modern mathematics is formalized more naturally in HoTT in a way
>that makes it more practicable for actual formalization. You keep
>saying things that make it sound as if you were debating with somebody
>who claimed that HoTT had in-principle advantages over set theory. By
>established theorems however [1], this is not so. HoTT is modeled in
>ZFC+inaccesbibles and, conversely, (constructive) set theory may be
>found in HoTT, so by established theorems one may go back and forth,
>subject to some technical fine print.  There is nothing much to be
>debated here, it seems to me.
>

This point should ultimately eliminate any advantage in formalization that HoTT has over set theory.  If we want our mathematics to be completely formalized in the official language of set theory, with the ZFC axioms and some mild large cardinals, and the deduction rules of FOL, then we only need to complete one project in order to co-opt all the formal advantages of HoTT.  Just produce a formal proof that ZFC+inaccessibles (naturally) interprets HoTT, and then apply this result to any future deductions from HoTT.  Maybe this is actually worth doing!

_______________________________________________
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/20141028/1da20c73/attachment-0001.html>