[FOM] Friedman/Campion/getting Hot

[Harvey Friedman]

More from https://plus.google.com/110536551627130071099/posts/6TiKLxjSCnu

FRIEDMAN:

I think that there is a very satisfying theory that does the
following. You start with a very nice relation of 2 or more variables
on a tiny finite set. You then take the "completion" of this tiny
thingie and get many of the usual iconic mathematical structures we
all know and love. This completion process is more radically general
than the ones normally discussed (but of course I am new to this kind
of game).

I am thinking that three points are enuf to generate the real line
with and without endpoints, and four points are enuf to generate the
circle. For the plane and for the usual sphere, more points, maybe 8
or so.

I see the possibility of delicious foundational theorems like you need
a certain number of points and a certain arity for the "seed" to
generate these various iconic spaces.

Thus there is going to be a theory of generation from tiny seeds. Seed
Generation Theory.

CONJECTURE. All of the usual iconic math structures fit well into this
theory, all generated by a  general totally clear completion process,
starting with tiny finite structures as seeds. The same iconic
structure may be generated by quite different tiny seeds.

John Baez - if this works out well enuf, thanks for your red meat. 

Also the entire set theoretic universe V under membership should be
generated from a tiny seed, maybe a five element thingie. Only here I
think that the completion process has to be a bit more radical. Then
the problem will be to unify this message with my previous message so
that the iconic math structures sit alongside (V,epsilon) in a common
trivial to understand theory. Although the underlying proofs of the
results may be highly nontrivial.

The ambitious idea will be that all of the information we really care
about in mathematics can be conveniently packaged into 2,3,4-ary
relations on sets of sizes 1,2,3,4,5,6,6,7,8, or so. And the packages
are readily understandable, far far clearer than any kind of random
table.

So, I am going to TRY to do this standard f.o.m. stuff:

1. General theory of how you complete nice tiny finite structures. If
the tiny finite structures, or seeds, obey a crucial condition, then
all goes well with the completion process, and you get something nice
and well defined and nice and "smooth" or infinite discrete.

2. Show how you can get a very large number of iconic mathematical
structures by picking the seeds carefully. The seeds are always tiny
pieces of the structure you wish to generate. It may be the case that
any sufficiently rich piece of the structure you wish to generate can
be used as a seed to generate the same structure.

3. Show that any really good structure has the property that it is so
generated by some tiny seed inside itself.

4. Present this in a lecture series. The first lecture will have the
following property: everybody understands every word. I might offer
$100 to anybody who can document that they didn't understand something
I said.

This is the standard f.o.m. investigation that is my real time
reaction to John Baez's red meat. What does this have to do with what
you guys and gals want to do?

TIM CAMPION:

I hope people will correct me whereever I go wrong in what follows,
but I see a fantastic teaching moment lurking in this exchange:

+John Baez  said:

“But the key is that we're taking a very relaxed attitude toward how
you can tweak a space while considering it the same.”

to which +Harvey Friedman  replied:

“We do this in standard f.o.m. by using the idea of an equivalence
relation, as you well know.”

Professor Friedman may be surprised to learn that although it’s true
that homotopy theory is about studying spaces (better: pointed spaces)
up to homotopy equivalence (better: weak homotopy equivalence),
nevertheless it’s false that homotopy theory is about studying the
equivalence relation of homotopy equivalence on the class of
topological spaces (even if you take into account pointedness or weak
homotopy equivalence). This equivalence relation simply throws out far
too much information. I’ll also point out (though Friedman didn’t
claim this) that it’s even more false that homotopy theory is about
studying the equivalence classes of spaces under the relation of
homotopy equivalence.

This can already be seen in much simpler cases. In enumerative
combinatorics, field theory, or really most mathematical subjects, we
are interested in finite sets, fields, or whatever objects we’re
interested in only up to isomorphism. But it’s important to keep track
of which isomorphisms are used — e.g. bijective proofs are preferable
to non-bijective ones; the study of automorphisms via Galois theory is
absolutely central to understanding fields; and really automorphisms
are important in just about any mathematical subject. Probably some
descriptive set theorist somewhere has considered the set of all field
structures on some set of sets and studied the equivalence relation of
isomorphism on it, but that is not what most mathematicians study when
they study field theory. (And if we pass to equivalence classes of
finite sets, we are no longer doing enumerative combinatorics at all,
but rather number theory).

In homotopy theory, it’s even worse in that we’re interested in spaces
not up to isomorphism, but up to weak homotopy equivalence. In order
to understand weak homotopy equivalences as the isomorphisms of some
category, we need to formally invert them and pass to the homotopy
category, which is very ill-behaved and difficult to work with. And
even that’s not enough, because passing to the homotopy category still
forgets too much information — in particular it doesn’t allow you to
talk about homotopy coherence of diagrams. To handle this, one can
either continue working directly with specific models of homotopy
theory like topological spaces, showing directly that all one’s
constructions are homotopy-invariant, or else move to a framework like
∞-categories.

I just referred topological spaces as a “model” of homotopy theory
because the notion of “sameness” given by homotopy equivalence is
sufficiently loose that we can actually model “topological spaces up
to homotopy equivalence” in many different ways. For example,
simplicial sets “model” exactly the same homotopy theory as
topological spaces. The sense in which this is true is technical
(there is a so-called “Quillen equivalence” between these two “model
categories” — and in particular this use of the word “model” has
nothing to do with, say, first-order model theory). It can be made
clearer using the language of ∞-categories, at the expense of
introducing more technical machinery.

The details of the last two paragraphs are not that important except
to communicate that in order to reason correctly about the sense in
which two homotopy equivalent spaces are “the same” in homotopy
theory, or at one level higher the sense in which topological spaces
and simplicial sets model the same homotopy theory, one either needs
to express things rather indirectly (using tools like Quillen model
categories) or else introduce more technical machinery (like
∞-categories). Part of what makes HoTT exciting is that it gives a
direct way of reasoning about these things that’s simply not available
in such a direct form in standard foundations. Namely, the objects of
study are simply types, and "homotopy equivalent" types are actually
equal, but in these foundations this fact does not lead to the loss of
information that passing to equivalence classes does in standard fom.

The takeaway is:

1. In standard fom, it is not the case that homotopy theorists study
the equivalence relation of homotopy equivalence on topological
spaces. What they study is related to this equivalence relation, but
it is much more complicated to express in standard fom.

2. In HoTT, this subject matter becomes simple and straightforward to express.
Harvey Friedman
8:44 PM

FRIEDMAN:

+Tim Campion  I leave it for now for others, such as Mario, to address
your specific specialized points, specifically in their responses.

In standard f.o.m., there are all kinds of additional fundamental
equivalence relations than just isomorphism. E.g., homomorphism. Often
we put additional structure in the structures so that isomorphism then
preserves much more than before. And standard f.o.m. also studies
automorphism groups like the automorphism group of free groups, and
the automorphism group of that automorphism group, etcetera. I also
alluded to various back and forth relations. We also readily deal with
things like whether two isomorphisms are themselves isomorphic.

So if you want to preserve some more fundamental stuff about your
favorite objects, standard f.o.m. is likely to be able to accommodate
this in satisfying ways with an army of ready make techniques designed
to make your head spin with their power.

For example, there are some very rich things going on that I largely
initiated in connection with the iconic equivalence relations coming
out of elementary mathematics, in terms of their structure and various
kinds of embeddings between them, in the area of descriptive set
theory. Some of this is rather close to ergodic theory. Descriptive
set theorists definitely develop some nontrivial frameworks for what
they do, which have a sort of foundational flavor. BUT THEY wouldn't
even consider offering it up as  general purpose foundations for
mathematics. THEY let it sit on top of ZFC, without any question. And
if descriptive set theorists can refrain from being tempted to say
that they are doing some seriously alternative general purpose
foundations for mathematics, then "you" should consider refraining
also.

Similar remarks apply to the model theorists, whose also definitely
set up various frameworks of a foundational nature. They would not
even consider themselves offering up any alternative general purpose
foundations for mathematics. And these modern model theorists are
fairly close to algebraic geometers, analytic geometers, algebraic
number theorists, universal algebraists.

So I do not believe for a moment that you are doing anything that
can't be done better with standard f.o.m. If you can give me some
simple universally understandable red meat like John Baez gave me,
then I can hope to show you how there is a standard f.o.m. subject
surrounding it that does something even more hopefully fundamental
than what you might have had in mind.

At the moment, given the billions of users of mathematics worldwide,
including professionals doing various specialized topics of all kinds,
almost none of them care about subtle homotopy type stuff. Of course,
almost none of them care about any specialized topic in any
specialized branch of math, so this is not a complaint about homotopy
type stuff at all (no offense).

It's just that the standards for something to be called general
purpose foundations for mathematics are very very high. And they
should be.

So put your stuff on top of ZFC and nobody has any issues. Probably a
few pages at most of key definitions would allow you to never ever
ever ever ever  have to refer to the extensional concept of set that
underlies ZFC, unless you want to.

Once you start to claim that it is more intellectually fundamental, -
or as intellectually fundamental - then you have taken on a very very
serious burden. This burden seems to me to be totally unnecessary.

Maybe you can meet that burden. But I believe that in order to do
this, you are going to look at mathematical thinking generally, and
not tailor a general purpose foundation to specialized esoteric
matters.

I just don't see what intellectually tangible advantage you have in
taking on this burden. The really overwhelmingly important
foundational issues that can substantially affect our relationship
with mathematical reality do not depend at all on the precise choice
of general purpose foundations for mathematics. This is because of the
accepted standard of mutual interpretability.

If you look at a piece of finite math, like FLT, it is generally
accepted that there is no wiggle room about needing some subtle setup
to understand what it means. Prima facie, there was a real
foundational issue. The first proof quoted Grothendieck Universes,
going just beyond ZFC. Actually ZFC is for almost all mathematical
situations of any concrete nature, is normally about 2^2^100000000
tines more powerful than what is actually used. Many feel that FLT can
be proved in a purely finitary way - i.e., can be proved in finite set
theory = ZFC with infinity replaced by not(infinity). This has not
been established in any convincing way, although believed.

John Baez's circle challenge is fine. There is a clear mental picture
of the circle held in the minds of billions of people around the
world. Clear mental pictures are basically tiny finite systems, hence
the need for Tiny Seed Theory. But fundamental issues like this should
be first analyzed in standard f.o.m. terms before one even thinks of
getting into anything like the subtleties you are referring to.

Maybe you have a very simple beautiful piece of red meat for me, like
Baez, that billions of people can immediately relate to already, and I
can try to chew on it.

I would be surprised if you had any chance at all in the wider
community of general intellectuals where pure abstract mathematics
itself is not a major thrust.

Harvey Friedman