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

Fri Apr 8 19:47:19 EDT 2016

> On Apr 5, 2016, at 21:11, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> On Tue, Apr 5, 2016 at 7:19 PM, Dimitris Tsementzis
> <dtsement at princeton.edu> wrote:
>> 
>> I’m not sure exactly what you mean by a “universal object” though I can see that in some sense SET is one. Is it fair to ask for an explanation?
> 
> I shouldn't of used universal object" as that means something
> important in category theory.
> 
> I see the following approaches to the kind of thing I think you are
> talking about, within the usual f.o.m. framework.
> 
> 1. The most well known. Use the set class distinction, and form the
> natural class of all sets.
> 
> 2. You can have sets and supersets. The standard model is the two
> sorted (V(lambda),V(kappa),epsilon). The sets are the elements of
> V(kappa). The supersets are the elements of V(lambda). Both V(lambda)
> and V(kappa) are to satisfy ZFC. When axiomatizing this, you can have
> the separation axiom for V(kappa) to use the full language.
> 
> 3. You can have the set V of all sets, but only have what I call
> positive comprehension. The problem is that the natural way to have
> the cumulative hierarchy here will involve some negative
> comprehension. Fixing this in the most obvious way will start to look
> like the set/class distinction, throwing us into a variant of 1.

I never doubted that there are such work-arounds. My contention is that they are not as satisfactory as what you can do in HoTT (with respect to this issue). All of the methods above involve “large” and “small” sets in one form or another. So there will be sets that you are leaving out when defining SET. In HoTT this doesn’t happen. This is to be expected, because in HoTT not all its basic objects are sets. The basic objects are homotopy types. This allows you to easily talk about all sets, since not all homotopy types are sets.

There is absolutely nothing complicated going on here other than the natural evolution of ideas. Set theory gave a foundation to mathematics. Mathematics also advanced because of set theory. Sets thus became objects of study of actual day-to-day mathematics, rather than just ways to formalize mathematics. So now we need natural foundations which can talk of *all* sets as if they were just one more among many (non-primitive) mathematical structures. HoTT provides one such way. 

> I will grant that there should be a way of doing this better in
> standard f.o.m. I will remain skeptical that it can be done better in
> another framework of the same logical strength as ZFC on very simple
> grounds. Until alternative f.o.m. is presented in a philosophically
> coherent way, then in a sense nothing that it does of this general
> conceptual nature is done well.
> 
> OK, let's take it granted, for argument's sake, that you have spotted
> something of some importance that you think alternative f.o.m. does
> better than standard f.o.m.
> 
> The natural question from the point of view of general purpose
> foundations for mathematics, is just where in the Undergrad Math
> Courses at Princeton,
> https://www.math.princeton.edu/undergraduate/courses one should or
> could naturally take advantage of this feature?

Very few, of course. But I don’t see how that’s relevant. After all, both HoTT and ZFC will coincide for all practical purposes for the vast majority of these courses. As you have emphasized time and time again (and I agree): with respect to concrete mathematics (e.g. the kind taught in most of these courses) all that matters is bi-interpretability of foundations. In all other respects it is a virtue for foundations to remain invisible, to stay in the background.

As such, foundations (whether HoTT or ZFC) will remain invisible for the vast majority of these courses, and that’s the way it should be. In some of these courses (e.g. Algebraic Geometry) foundations become visible when you have to consider, say, large categories. Instructors will usually say something like “We assume here that we are given a universe of small sets, there are several ways to do this etc.” and then carry on as usual. With HoTT, foundations would not need to become visible even in such cases, since we would rest assured that sets are merely one of many structures on our basic objects, and there is no reason to worry about “size". Thus, with respect to this ISSUE, HoTT provides an incremental improvement: increased invisibility.

Dimitris

> On Apr 5, 2016, at 21:11, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> On Tue, Apr 5, 2016 at 7:19 PM, Dimitris Tsementzis
> <dtsement at princeton.edu> wrote:
>> 
>> I’m not sure exactly what you mean by a “universal object” though I can see that in some sense SET is one. Is it fair to ask for an explanation?
> 
> I shouldn't of used universal object" as that means something
> important in category theory.
> 
> I see the following approaches to the kind of thing I think you are
> talking about, within the usual f.o.m. framework.
> 
> 1. The most well known. Use the set class distinction, and form the
> natural class of all sets.
> 
> 2. You can have sets and supersets. The standard model is the two
> sorted (V(lambda),V(kappa),epsilon). The sets are the elements of
> V(kappa). The supersets are the elements of V(lambda). Both V(lambda)
> and V(kappa) are to satisfy ZFC. When axiomatizing this, you can have
> the separation axiom for V(kappa) to use the full language.
> 
> 3. You can have the set V of all sets, but only have what I call
> positive comprehension. The problem is that the natural way to have
> the cumulative hierarchy here will involve some negative
> comprehension. Fixing this in the most obvious way will start to look
> like the set/class distinction, throwing us into a variant of 1.
> 
> 4. Untyped lambda calculus. Here the operators act on everything. But
> again how to get the cumulative hierarchy?
> 
>> Also, of course, the ISSUE I raised was not meant to be a definitive reason to switch foundations, but an illustration of the kind of thing that “alternative f.o.m.” allows you to do well, that you can also do in standard f.o.m. > but not so well.
> 
> I will grant that there should be a way of doing this better in
> standard f.o.m. I will remain skeptical that it can be done better in
> another framework of the same logical strength as ZFC on very simple
> grounds. Until alternative f.o.m. is presented in a philosophically
> coherent way, then in a sense nothing that it does of this general
> conceptual nature is done well.
> 
> OK, let's take it granted, for argument's sake, that you have spotted
> something of some importance that you think alternative f.o.m. does
> better than standard f.o.m.
> 
> The natural question from the point of view of general purpose
> foundations for mathematics, is just where in the Undergrad Math
> Courses at Princeton,
> https://www.math.princeton.edu/undergraduate/courses one should or
> could naturally take advantage of this feature?
> 
> Precalculus/Prestatistics
> Calculus 1
> Calculus II
> Number, Shape and Symmetry
> The Magic of Numbers
> An Integrated Introduction to Engineering, Mathematics, Physics
> An Integrated Introduction to Engineering, Mathematics, Physics (more)
> Useful Fictions: How and why mathematics is developed and then changes the world
> Math Alive
> Calculus III (Multivariable Calculus)
> Introduction to Linear Algebra
> Advanced Multivariable Calculus
> Advanced Linear Algebra with Applications
> Numbers, Equations, and Proofs
> Honors Analysis in a Single Variable
> Accelerated Honors Analysis I
> Honors Linear Algebra
> Accelerated Honors Analysis II
> Mathematics in Engineering 1
> Mathematics in Engineering II
> Introduction to Real Analysis
> Numerical Methods
> Introduction to Differential Equations
> Topics in Mathematical Modeling - Mathematical Neuroscience
> Analysis I: Fourier Series and Partial Differential Equations
> Complex Analysis with Applications
> Analysis II: Complex Analysis
> Applied Algebra
> Algebra I
> Algebra II
> Fundamentals of multivariable analysis and calculus on manifolds
> Introduction to Differential Geometry
> Topology
> Introduction to Graph Theory
> Combinatorial Mathematics
> Theory of Games
> Probability Theory
> Analytic Number Theory
> Topics in Number Theory: Algebraic Number Theory
> Analysis III: Integration Theory and Hilbert Spaces
> Ordinary Differential Equations
> Advanced Topics in Analysis
> Cryptography
> Commutative Algebra
> Topics in Algebra: Representation Theory
> Advanced Topics in Geometry - Lie Theory
> Algebraic Geometry
> Advanced Topology
> Random Processes
> Functional Analysis
> Introduction to Partial Differential Equations
> Advanced Analysis
> Riemann Surfaces
> 
> Harvey Friedman