[FOM] Friedman/Baez/Gowers

[Harvey Friedman]

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

By the way, https://www.academia.edu/23459457/Set-theoretic_Foundations
was referred to there. I think that this Maddy paper could generate
some interesting FOM discussion.

BAEZ:

...

Freyd said "The purpose of category theory is to show that what is
trivial is trivially trivial."  I utterly disagree that this is the
purpose of category theory - in fact, this is one of the worst
advertising slogans in the history of mankind.   But it's certain one
purpose of category theory - one of the humbler ones.

On the other hand, +Timothy Gowers said "I'm content to let the
trivial be trivial."  And so, there are people content to let
analogies be analogies.

TIMOTHY GOWERS

Did I really say that? If so, I didn't mean to disparage category
theory, but simply to say that in my work that's an attitude I can
afford to take -- I don't need the clarifying effect of category
theory. But that reflects the very particular kind of mathematics that
I do.

BAEZ:

+Gowers:

yes, you said something like that here on G+.  Regardless of what you
actually think, it's such a catchy comeback that it deserves to be
repeated.

Of course I think everyone could benefit from the clarifying effect of
category theory.  That's why I'm trying to apply it to electrical
engineering, control theory and chemistry.  But I am not trying to
convince everyone that it's worth their time to learn category
theory.

ROUX CODY:

...

In computability, there is a well established and standard definition
for the computable functions, the set of (general) recursive
functions. One might define them in terms of, say, Turing Machines
(TMs). The main difference here is that there is virtually no argument
about whether TMs accurately capture the whole concept of "computable
function", an agreement I'll usually refer to as Church's Thesis (CT).
In "foundations" we don't agree on what the range of true statements
in arithmetic are, or what the range of definable mathematical
structures is, but I'd argue that actually, for the most part, there
isn't much debate, and there is something akin to Church's thesis,
that I might be tempted to call "Zermelo's Thesis" (ZT).

Now one might introduce a new model of computation, say the
pi-calculus if we want to be concrete. What I'm trying to express, is
that once the pi-calculus is established to be Turing Complete, i.e.
to express the same range of computable functions, then there is
nothing more to be said about the pi-calculus in the field of
recursive functions.

However, a computer scientist might quite reasonably argue that the
study of the pi-calculus's intensional (or structural) properties are
very different than those of TMs, and that it is a useful endeavor to
study a theory of computations based on the pi-calculus rather than on
TMs. The Harvey Friedmanns of computer science would object that TMs
are a much more established foundation for computation, that
everything expressible in the pi-calculus is expressible in TMs via a
suitable encoding, and that it would be silly to throw decades of
valuable tradition away in favor of a complex and hard to understand
framework like the pi-calculus.

Then when one is interested in the creation of concrete programs and
programming languages, one of course must give in to messy engineering
considerations possibly far removed from theory. Whether they are
based on Turing Machines or the pi-calculus.

I hope this analogy elucidates my point of view, flawed though it might be.

BAEZ:

+roux cody - I completely agree with your analogy.   Computer science
would have been immensely held back if people thought that Turing
machines were the last word on computation, ignoring new programming
methodologies because any recursive function can in principle be
computed by a Turing machine.  Similarly, whether you call them
"foundations", "frameworks" or "entrances", math is by no means done
improving its basic infrastructure, even though everything most
mathematicians want to do can in principle be coded into ZFC, perhaps
with some large cardinal axioms thrown in.
Harvey Friedman
9:20 PM

FRIEDMAN:

+roux cody
+John Baez

The analogy with TMs may look accurate, but a closer look reveals that
it is not.

A main points of ZFC, not the only ones, is that it is

i. It is extremely simple, especially ZC, which really does suffice
for almost all mathematics. (By the way you know that I am involved in
totally transparent cases where ZFC doesn't suffice, but that is
another ongoing story).

ii. It is completely transparent that almost all math is easily and
conveniently construed as being captured in i.

With TMs, you also have i. HOWEVER, TMs are particularly bad for ii.
It is not at all clear when you read, write, and talk about an
algorithm, that it is codable in a TM.

In fact, we don't have an analog in computation for ZFC in
foundations. I am aware that there are some things around in this
direction, of course. Like the kind of RAMs used in algorithms
courses. These are pretty good. The idea being that if you want to be
somewhat careful about reading, writing, and talking algorithms, then
it is supposed to be fairly clear how it fits nicely into the RAM
framework, so you can run asymptotic complexity investigations while
writing only pseudocode or less.

There are other non analogies. The role of philosophical coherence
really doesn't arise in the computation situation. There is no issue,
in models of computation, of legitimacy. (Legitimacy only arises when
you want to try to expand the notion of computability by incorporating
physical processes and the like, but that is really a quite different
matter than what we are talking about here).

On the other hand, the issue of legitimacy is completely central in
foundations of mathematics. A crucial aspect of legitimacy is of
course the famous consistency.

One trapping of the fact that ZFC is the standard f.o.m. and has
remained so for around 100 years, not serious challenged, is that
through its great simplicity and philosophical coherence, it became
and is still the gold standard arbiter for consistency. That is, ZFC
and its fragments. Whenever anybody proposes any new kind of
foundation or framework, everybody wants to interpret it in ZFC or its
fragments.

I do not exclude the possibility that there is an alternative concept
or concepts that could also support great simplicity and philosophical
coherence, and also be seen to be legitimate and in particular
consistent on its own, just as ZFC and its fragments are. Even more
impressive would be that it offers even more simplicity and/or
philosophical coherence than ZFC. IN FACT, I am probably at least as
interested in doing this as anyone living or dead on this planet.

HOWEVER, I have not seen this even close to being done. I am actively
trying to do this myself.

Actually, I have also always been attempting to come up with the
proper analogy of ZFC in computation, as well.

Harvey Friedman