[FOM] New Umbrella?

[Joseph Shipman]

This is exactly the kind of metatheorem I talked about in my previous post. All that remains to be debated, then, is the empirical question of how much mathematics would be better formalized in HoTT "from the ground up" rather than in ZFC. I suspect the answer would be "a small fraction", as judged by number of published refereed papers, but I am very interested in any disagreement on this point, because without disagreement on this point there is really nothing left to argue about.

-- JS

Sent from my iPhone

> On Oct 28, 2014, at 3:13 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/dc315bfa/attachment-0001.html>