[FOM] Friedman/Baez/getting HOT

[Harvey Friedman]

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

BAEZ:

+R. Rowan wrote: "I thought it telling that [Mario] said "the objects
of HoTT are complicated, but that's exactly what makes the field
interesting"."

I wouldn't have said that myself.   I never think things are
interesting just because they're complicated.  I like taking
complicated things and making them simple.

A type in HoTT is - as I said earlier - just a kind of space.  But the
key is that we're taking a very relaxed attitude toward how you can
tweak a space while considering it the same.  For example, a doughnut
is the same as a coffee cup is the same as a circle is the same as an
annulus is the same as the plane with a point removed.

Now, spaces can be complicated - that's true.  But what's great about
HoTT is that we can get our hands on spaces much more simply than in
traditional mathematics.  Traditionally, before I can discuss a circle
I need to define the real numbers, etc.  In HoTT we can get it very
quickly.

Also, in HoTT we see that any proposition can also be seen as a space:
the points of this space are just its proofs.

So we're unifying topology and logic, while dramatically simplifying the former.

To me, THIS is what makes the field interesting.

The unification of topology and logic has been underway for a long
time now; it didn't start with HoTT.  But HoTT does it in a nice way.

MICHAEL SHULMAN:

"My favorite metaphor for foundations of mathematics is that they are
like programming languages.  When you invent a new programming
language, call it say X, you have to write a compiler for it.  You
probably start out by writing a compiler in some other language, say
Y, since you want to be able to compile your compiler and a compiler
for X doesn't doesn't exist yet.  But that doesn't mean that language
Y is logically or philosophically "more fundamental" than language X,
only that it came first as a matter of historical accident.  After
language X becomes established, you could just as well write a
compiler for language Y in language X."

BAEZ:

I don't think that's quite right.  If I write a compiler for a new
language, X, and write the compiler in a different language, Y, that
already exists, many factors other than mere existence will affect my
choice of Y.   I'll try to pick a Y I think is good for writing
compilers; and if X becomes established, it may not be that I could
just as well write a compiler for Y in X.  X might not be as good for
writing compilers, or Y might be a harder language to write a compiler
for.

(I also don't think that very much of the order in which programming
languages appeared is quite historical accident.)

A different analogy I think may be useful is about what the compiler
for X outputs.  One approach I used and seen used to good effect is
for it to output C (and then run the C compiler on the result).   C
has properties that make it especially good for that role, and it can
be considered in a sense "more fundamental".

FRIEDMAN (all of the stuff below written by me):

+John Baez

BEFORE READING THIS,

1. HIDE THE CHILDREN.
2. REALIZE THAT I KNOW THAT I MAY BE WRONG. SHOW ME.

Rowan:

"I thought it telling that [Mario] said "the objects of HoTT are
complicated, but that's exactly what makes the field interesting"."

Baez:

I wouldn't have said that myself.   I never think things are
interesting just because they're complicated.  I like taking
complicated things and making them simple.

Friedman:

BRAVO!!! Now you are talking my language. You're my hero!

Baez:

A type in HoTT is - as I said earlier - just a kind of space.

Friedman:

Very standard f.o.m. friendly idea.

Baez:

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

Friedman:

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

Baez:

For example, a doughnut is the same as a coffee cup is the same as a
circle is the same as an annulus is the same as the plane with a point
removed.

Friedman:

IMMEDIATE REACTION. Depends on what equivalence class you are talking
about. My plane with my point removed in my mind is not the same as my
circle. And I don't want it to be the same - unless you tell me what
purpose you are serving by my thinking that they are the same. I do
know that they are the same with no structure. I.e., they are
isomorphic under just equality.

Homeomorphism, and all kinds of variations of homeomorphism done for
various geometric like purposes. It is also standard f.o.m. to do this
for all kinds of non geometric based ideas, too. Like "satisfying the
same first order sentences", "satisfying the same second order
sentences", and some even much stronger things that are not as well
known or as well worked out, that probably should be. In fact, there
is an important language called L-infinity-omega with a beautiful
theorem characterizing "satisfying the same L-infinity-omega
sentences" in terms of what are called back and forth relations. In
fact, now that I recall, there is a whole hierarchy of so called back
and forth relations, which are purely combinatorial, and do not
mention languages in any way, but which are equivalent to the obvious
language theoretic equivalence relations.

These are all viewed as a hierarchy of approximations to being
isomorphic. They are generally not the same as being isomorphic.
Except, there is one very stunning case and that is of countable
structures. Here there is a fundamentally important result due to or
essentially due to Scott. In nice informal terms, given any two
countable structures, there is a uniform "process" of successively
stronger comparisons, creating a hierarchy of equivalence relations
between the domains of the two structures, that are much weaker than
being an isomorphism, and which, in the limit, provides a kind of
canonical isomorphism, if they are isomorphic. This process is
necessarily countably transfinite.

Thus there is a measure of the degree to which any two countable
isomorphic structures are isomorphic, and the measure is a countable
ordinal.

By the way, there are other fundamental contexts in which countable
ordinals come up in surprising ways.

THEOREM (friedman). For any two countable sets of rational (or real)
numbers, there is a one-one pointwise continuous map from the first to
the second or from the second to the first.

THEOREM (friedman). In various senses, both from descriptive set
theory (branch of standard f.o.m.) and proof theory (branch of
standard f.o.m.), all countable ordinals are involved in the preceding
Theorem.

HOWEVER: I have never seen this point of view of successive
approximations to isomorphism and isomorphisms between countable
structures investigated systematically for CONTINUOUS structures!

Obviously, the kind of continuous structures that come up in
mathematics in seriously intense ways, are VERY SPECIAL from a
combinatorial point of view, and MUST SURELY lend themselves to a very
nice extension of the above classical stuff from standard f.o.m. that
works so well for countable structures.

People know that this sort of thing for arbitrary countable structures
turns rather ugly for arbitrary structures of cardinality the
continuum. But mathematics only really focuses on very well behaved
structures of cardinality the continuum, and so the whole matter of
isomorphic, isomorphisms, and approximations to these, needs to be
systematically revisited with normal mathematical thinking in mind.

In fact, probably the transfinite is not needed, as it is necessarily
so (we know this) in the case of arbitrary countable models. It would
be most dramatic to have the process of successive approximations to
isomorphisms be demonstrably of finite length in fairly general
fundamental environments.

Baez:

Now, spaces can be complicated - that's true.  But what's great about
HoTT is that we can get our hands on spaces much more simply than in
traditional mathematics.  Traditionally, before I can discuss a circle
I need to define the real numbers, etc.  In HoTT we can get it very
quickly.

Friedman:

You have FINALLY given me real piece of RED MEAT, and I am hungry.

Of course, there are probably 17 interesting ways of quickly getting
to "a circle" in standard f.o.m. So I desperately need to know what
you have in mind for "discussing a circle" that is different than -
and better than - the 17 interesting ways of doing this in standard
f.o.m.

I have had a foundational program in the back burner for some time
called "logical characterizations of fundamental mathematical
structures", where I study how simple I can make sentences in various
languages that characterize important structures up to isomorphism,
and possibly up to weaker equivalence relations. The circle is on my
list of structures.

Of course, there are various ways you can construe the circle as a
mental picture. All of those basic ways lend themselves to interesting
standard f.o.m. investigations. There is also the overriding question
of "what does a fundamental construing of something like a circle
consist of" and "characterize all of the fundamental construings of
things like the circle".

All of this is RED MEAT standard f.o.m.

As I have repeatedly said many times.

CONJECTURE. anything "you" can do I can do better with standard f.o.m.

This does not mean that one can use simply a limited kind of
reasonably astute understanding of basic standard f.o.m. and a high
IQ. That will not be enough. But say 10,000 hours of thinking deeply
about standard f.o.m. should be enough. 100,000 hours will be more
than enough.

Baez:

Also, in HoTT we see that any proposition can also be seen as a space:
the points of this space are just its proofs.

Friedman:

This is the kind of prima facie nonsense that is VASTLY PREMATURE.
Long before you do violence to sacred notions like "proposition" and
"proofs", you had better exhaust standard f.o.m. along the lines I
indicated above, FIRST. Bringing the notions of propositions and
proofs directly into your foundations for mathematics is actually a
crime against the intellect.

I will let "you" out of prison for this only AFTER people who  have
spent 10,000 - 100,000 hours thinking hard about standard f.o.m. FAIL
to address your issues of general intellectual interest in say a few
years time - although it should be doable in real time for the 100,000
hours people.

Just think about what "you" are doing. Because you don't see some
prima facie way of addressing perfectly sensible and fundamental
issues surrounding identifications and isomorphisms in standard f.o.m.
terms, "you" resort to identifying logical and mathematical notions
that are totally different, and even stick them directly into the
object language of your so called alternative general purpose
foundations!!

CONJECTURE. These are the worst pseudo foundational ideas that have
ever been put forth by high IQ people.

Baez:

So we're unifying topology and logic, while dramatically simplifying the former.

To me, THIS is what makes the field interesting.

Friedman:

And that's what makes it ridiculous - or at least ridiculously
premature. The obvious thing to do is keep them separate like they
fundamentally are, but give a standard f.o.m. treatment of all sorts
of fundamental topological/geometric issues like choice of and
characterization of fundamental equivalence relations between
structures, fundamental characterization of structures by sentences in
appropriate languages, equivalences between such and combinatorial
processes, classification of ways of combining structures that respect
fundamental equivalence classes, and so forth. All replete with
surprising equivalences of approaches, and so forth. Theories of what
a mathematically natural structure is - one that can be uniquely given
by formally simple conditions, unique up to various fundamental
equivalence relations, and formally simple in various fundamental
senses, etcetera. All with deep tools from standard f.o.m.

AFTER this has been mined out, you can try to do something prima facie idiotic.

Baez:

The unification of topology and logic has been underway for a long
time now; it didn't start with HoTT.  But HoTT does it in a nice way.

Friedman:

This reminds me of the topological interpretation of intuitionistic
logic from a long time ago. You there a beautiful completeness
theorem. But the interesting yet dubious idea that mathematics should
be done intuitionistically isn't really addressed by such things. In
fact, the most impressive standard f.o.m. developments in this vein
concern rather intricate and deep theorems concerning the relationship
between intuitionistic logic and mathematics and classical logic and
mathematics. All done with by now classic but tricky standard f.o.m.
tools.

Now that you have given me a little red meat, please give me some more
red meat concerning what you call the "unification of topology and
logic". Again, I come back to my conjecture:

CONJECTURE. anything "you" can do I can do better with standard f.o.m.

Harvey Friedman