[FOM] Friedman/Baez/getting HOT

Tue Apr 12 08:44:51 EDT 2016

Dear FOM,

The following was written in the below email by Harvey Friedman, quoting Baez and Rowan.

> 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.

Taking a (historical) step back here may be in order:

1) Theorems of constructive/recursive mathematics are often much more complicated 
than their classical counterpart (having lots of ‘extra data’) because of the need to  
enforce computability (or constructivity).  

For instance, a colleague of mine looked at the definition of “atlas” in topology 
and tried to formulate this in recursive math.  After the definition grew from a paragraph
to more than three pages, he gave up.  

2) Related to this, Reverse Math (RM) came about by shifting the framework/point of view:  
Rather than enforcing computability, people in RM study theorems `as they stand’ and try 
to determine ‘how much non-computability’ is necessary (actually, which set existence axioms are needed).  

3) As far as I understand it, HoTT enforces (via the Univalence axiom) that “isomorphic objects are identified”.  
Similar to the case of constructive/recursive math, this ‘enforcement' has the potential to lead to very complicated
theorems, especially in areas of mathematics where one does not normally/naturally identify isomorphic objects.

Hence two questions:

a) What makes HoTT different from constructive/recursive math, i.e. why will enforcing a given paradigm not lead to more complicated theorems this time around?

b) What about “Reverse HoTT”, where one classifies theorems according to how much univalence / “identifying isomorphic objects” is needed?

Best,

Sam

> On 10 Apr 2016, at 06:23, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom