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

[Harvey Friedman]

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