[FOM] Challenge addressed by HoTT/UF that is not addressed by ZFC

[Dimitris Tsementzis]

Friedman wrote:

> On Mar 30, 2016, at 16:20, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> As I expected, I could not find a single example of any of the following:
> 
> (1) Some issue in f.o.m. that is not being addressed by the usual f.o.m.
> (2) Some issue in f.o.m. that is being addressed by type theoretic f.o.m.

Here is an example of such an issue, in my opinion extremely simple and fundamental, and worthy of discussion: 

ISSUE: Define a category SET of sets in f.o.m. whose objects are *all* sets. 

Concerning (1): ZFC does not satisfactorily address this issue. Several approaches (reflection principles, adding universes etc.) are known and have been studied extensively, the situation perhaps best summarized in Feferman’s Bernays Lectures [1]. But every such approach, as far as I can tell, on some level involves separating between some class of “small” and some class of “large” sets. And SET is then always defined as the category of all “small” sets. As such, in ZFC, SET cannot be defined so that it contains *all* sets.

Concerning (2): In HoTT/UF, this issue is addressed almost as a triviality. The type Set in a univalent universe U can be given the structure of a category and it contains *all* sets in U (defined as types of h-level 0, i.e. discrete homotopy types). The reason this works so well is because in HoTT/UF a given universe U is not comprised of sets. Sets are merely one of many structures one can impose on the objects of U. It thus becomes as natural to speak of *all* sets as it is in ZFC to speak of *all* sets of a given rank.

A few further reasons why this is a compelling example:

(a) The issue is clearly of practical significance for practicing mathematicians, who want to be able to manipulate a category of *all* sets. As such it is fair to call it an “issue in f.o.m.”. 

(b) Furthermore, it is an especially compelling example since it cannot be repeated in traditional (non-HoTT) MLTT. It depends essentially on having a notion of the h-level of a type and formalizing sets as types of a specific h-level.

(c) Interestingly, of course, one can say that the ISSUE is very well-addressed by NF. But the category of sets one obtains in NF is not very satisfactory, e.g. it is not cartesian-closed as shown by McLarty [2]. No such failures are known to occur in HoTT/UF.

Dimitris

[1] https://math.stanford.edu/~feferman/papers/BernaysLecture3.pdf <https://math.stanford.edu/~feferman/papers/BernaysLecture3.pdf>
[2] http://www.cwru.edu/artsci/phil/FCCinNF.pdf <http://www.cwru.edu/artsci/phil/FCCinNF.pdf>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160404/d1cef5de/attachment-0001.html>