[FOM] Coherence:Friedman/Cody/Roberts

[Jay Sulzberger]

On Sat, 9 Apr 2016, Harvey Friedman <hmflogic at gmail.com> wrote:

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

< some discussion suppressed here />

> David Roberts
> 
> There we go again with philosophical coherence. Define it for us
> please, and not in such a way that, surprise, only ZFC (or relatives)
> can possibly satisfy it; I don't believe that there is a unique
> philosophically coherent system on which to base mathematics. This
> would be a more amazing theorem, if it could be elevated to such
> status, than incompleteness.
> 
> Friedman:
> 
> I think there is a theorem to the effect that any two natural systems
> that interpret PA are comparable under interpretation. Also in the
> suitable sense, their Pi-0-1 theorems are comparable. And stronger
> things. I wrote about this on the n-category cafe in response to John
> Baez. Here "natural" is much weaker than "philosophically coherent".
> 
> Also I wrote on the n-category cafe I responded to Eugene Lerman when
> he asked me what foundations of X is. My answer is relevant there.
> 
> There is a whole big Western philosophy community that is in the
> business of writing philosophically coherent papers, and I have yet to
> see them carefully define what that means. So this is not going to be
> easy to do. It is also not easy to define "musically coherent in the
> context of classical piano performance". 

But surely the question of what is "a philosophically coherent
foundation for mathematics" is in part a logical question.  And
the triumphs of first order logic and of the study of ZFC are, in
part, triumphs of philosphical and, most important, plain old
mathematical, analysis and synthesis.  I am glad that we agree
that making things more clear here is not easy.  My claim, and I
think, John Baez's, is that New Crazy Type Theory^W^W^W^WHomotopy
Type Theory is, in part, an attempt at just this analysis and
clarification using quite standard techniques, namely
formalization of things that once, that is to say, before HoTT,
mathematicians "swept under the rug", as Gian-Carlo Rota used to
say.

> 
> Arnaud Spiwack:
> 
> Man! This is entertaining!
> 
> http://media.riffsy.com/images/7260ad7de2d77fa3b597026aee82b391/raw
> 
> Roberts:
> 
> If you cannot say what philosophical coherence is, how are proponents
> of non-ZFC foundational systems supposed to fulfil your demand for
> such an explanation? If responses I've seen are merely code for "*I*
> don't find that philosophically coherent", then the issue of
> communication is worse than previously suspected, since I've seen
> plenty of explanations that seem to have a good deal of thought behind
> them, and which make sense.
> 
> Comparisons to music are fraught with risk: the European musical scene
> that rejected Beethoven's late string quartets became after a few
> decades the movement that would have called them too conservative. Is
> it not possible we are seeing a similar shift in attitudes here? For
> some people, Lawvere's ETCS, so derided on the fom mailing list in the
> late 90s, is just another set theory and doesn't go far enough.
> 
> Friedman:
> 
> I claim that everybody on the discussion has a good working idea of
> what philosophical coherence means without the difficult and important
> work of analyzing what it means. I'm just not in a position to do
> this. There is a whole philosophy community who is more in a position
> to do this, and certainly does it in a practical sense all through
> their Western curriculum

Ah, indeed the issue of what has been proved when one shows a
cryptomorphism lies at the heart of NCTT.  Let us take up again
the example of finite matroids.  Here are two formalism:

1. A finite matroid is a finite set E with a subset Circ of
Pow(E), where Pow(E) is the collection of all subset of E, with
Circ being subject to certain laws, or if you wish "axioms".

2. A finite matroid is a finite set E with a given "rank
function" dim: Pow(E) -> NNI where NNI is the non-negative
integers, again subject to certain laws.

Now we know that given a matroid, call it M1, presented under
definition 1 we may form a matroid M2 presented under definition
2, such that M1 and M2 are "cryptomorphic", that is, to every
"operation under definition 1" on M1 we have a corresponding
"operation under definition 2" on M2.  M1 and M2 are "essentially
the same".  Well what does this mean?  Do we have a formal
definition of "essentially the same" which works for every pair
of type definitions so that we have a clear determination of the
cases in which the two definitions give essentially the same type
versus the cases in which the two definitions give essentially
different types?  (To forestall an elementary error, "clear
determination" does not imply we have to hand a total recursive
function on pairs of type definitions which returns correctly
"Yea" or "Nay" for all pairs.)

Let us return to ZFC.  Suppose we consider one of the standard
definitions, no not "definition", rather one particular
implementation of the type "ordered pair", ah I am an old Lisper,
so let us just say "Cons".  I think that the value of (cons a b),
if implemented as {a, {a, b}}, gets us an implementation of
the type Cons, the type of an ordered pair.  Now let us consider
ZFC but with two ur-elements, call them "first" and "second".
Call this system "ZFC2".  Here is an implmentation of the
value of (cons a b) in ZFC2: the unique function pair from the
set {first, second} to the set {a, b} such that

pair(first) = a and pair(second) = b.  Now, in many contexts,
under various assumptions, I think most mathematicians, well if
you could get them to sit still long enough to ask the question,
would say that our two different implementations of the type Cons
really are just two different implementions of the same thing.
We do not have two different Cons types, but just one.  We do
have two different implementations.  Indeed the different
implementations do not even lie in the same world: one lies in
ZFC, the other in ZFC2.  And I think even many logicians would
agree that our two implementations of Cons give us the same type.
Indeed I think you have written something close to this in a post
in this thread.  We know the two implementations differ, but only
in things having to do with the implementations, not having to do
with the, please forgive this computer jargon!, the abstract data
type Cons.  That is, it is the same Cons in both cases, and it is
just irrelevant that one implementaion is a set with a certain
arrangement of elements and the other is a map from the set of
ur-elements.  Let us sink to the level of mathematical texts: If
we read in a mathematics paper the sentence:

   "Let X be the ordered pair (a, b)."

and then, in most cases, if the referee were to say "I do not
understand.  Do you mean {a, {a,b}} in ZFC, or do you mean
pair: ur2 -> {a, b} with pair(first) = a and pair(second) = b?
in ZFC2?"  one might supect that the referee were new at reading
mathematics papers.

I think John Baez has written up thread something close to these
argument in defense of Homotopy Type Theory.  And I have written
before, and so have others, that the two implementations of the
type FinMatroid, tend to suggest different variations of the
type.  The first definition might suggest oriented matroids, and
the second polymatroids.  The argument here, well the argument
lifted up to grandiose heights, is, and we have discussed this
before, different "foundations", different "implementations",
suggest different questions, different lines of investigation.

I will now attempt a shallow argument, by a fork, against the
unique fitness of ZFC as a foundation for mathematics:

   If there have two different foundational systems and they are
   inter-interpretable then clearly it does not matter which we
   use to "implement mathematics".

   But if you defend one as being better than the other on the
   basis of "coherence", and venerability by reason of the high
   seriousness of work done on/with it, then I think you are
   committed to offer a logical/mathematical explanation, or at
   least a clear understanding of what "coherence" means, and also
   an argument to this effect: that before the work is done, that
   the second, let us say, younger foundational system, cannot be
   the object of serious work, at least by comparison to the Most
   Honorable and Most Ancient Foundational System.

If you take the first fork, well one is just as good as the
other, then you are admitting that one can have systematic
cryptomorphisms, indeed, one gigantic cryptomorphism, between two
different foundations, better, two different implementations of
one mathematics.  OK, so then you agree with the program of
Homotopy Type Theory.  If you take the second fork, I think your
analysis will likely make use of the various distinctions and
make note of the various mathematical phenonomena that are the
characteristic tools and objects of study of Homotopy Type
Theory.

> 
> This is sort of like asking what a rigorous proof is. Sure, we have
> formalisms, but as a practical matter, a working mathematician must
> use instinct in order to actually create rigorous proofs and also
> evaluate whether someone else has given a rigorous proof. Of course,
> the formalisms are important as final arbiters, when issues really
> arise. ZFC has been around for so long and is so natural, that just
> about everybody knows without much thought and very reliably whether
> they have stayed within ZFC.

I hope this incomplete paraphrase is not unfair: "We
professionals generally agree on what is a rigorous proof.  But
we must pass to irrelevancies, precise irrelevancies admittedly,
to check that a proof really is a proof.".

Harvey!  You are a logician!  You must feel in your breast the
radical illogic of this!  Advertisement for type theory: In
particular you must want an explication of the concept of "these
two proofs are essentially the same".  There begin to be some
results here: For the "minimal intuitionist sentential calculus
with one logical connective ->" we have the wonderful analysis by
the paradigm Curry-Howard Theorem, the one for the simply typed
lambda calculus.  Now that is a good theorem and it gives us a
convincing explication of when two proofs are the same for this
simple logical formalism.

> 
> I don't think there is any serious communication problem along the
> lines that you are worried about. There does seem to be other
> disagreements, intellectual value conflicts, or whatever. Here is how
> I see it.
> 
> All of you definitely agree that I can give an explanation of standard
> f.o.m. from first principles that relies only on the audience having
> some sort of reasonably competent basic mathematical instincts, with
> essentially no special mathematical knowledge or experience. Putting
> together prescribed things into a set, where those things might
> themselves be sets, and using words like not, if then, there exists,
> equal, element of, and so forth, these are IQ matters. Especially in
> the finite world. I have some theorems about going from the finite
> world to the infinite world here, and experience with this sort of
> thing would make my explanation of standard f.o.m. from first
> principles arguably more compelling than everybody else's (maybe).

No.  Of course not.  If people understand this it is because, as
a result of the outcome of a convulsive internal struggle of the
European and allied mathematical cultures, fought out in the late
Nineteenth Centure and the first half of the Twentieth,
professional mathematicians are today inculcated with a world
view in which ZFC is The Foundation.  Now by popularization,
including the almost incredibly mis-managed New Math of the
1960s, very educated folk have some grasp of set theory.  And so
when you speak with them, they often can follow.  I also think
you are a good teacher ;) But really, the implementation of Cons
is just a coding trick.  Recently a student I know made a first
study of Goedel's Incompleteness Results.  The student thought
that the result had something to do with prime numbers, because
the texts used Goedel's original Goedel numbering.  As Mike
Shulman vigorously, in public, points out "This is not right".
And we are back to our fork.

> 
> So there is definitely the recognition out there that making standard
> f.o.m. part of you depends on nothing but a raw brain, and perhaps can
> be absorbed while in the womb.

No.  Euclid, Archimedes, Newton, and Gauss, had not the benefit
of this foundation, and I think that even were you to be
transported back to speak with them, and give your Introduction
to the Foundations of Mathematics with Special Attention to ZFC,
you might find some resistance.  Surely just the concept of
"model" as used in the theory of First Order Logic, is big enough
to require a day or two to grasp.  After presenting the concept
of "formal language" of course.

> 
> I have been looking for a similar fundamental explanation from first
> principles for ANY purported foundation for mathematics, and consider
> that the first standard for getting into the foundations game.
> 
> I have been using this harsh sieve and asking people to conform to
> this standard in open forums such as the FOM and the Baez (and now
> Cody) sites.
> 
> Nobody seems to want to take this up for a number of varying reasons.
> 
> 1. They know what I mean, but they recognize that this is hard to do
> and would require some serious thought. They think they could do this,
> but it would not be worth their time given their other priorities.
> 
> 2. The know what I mean, but they recognize that they don't know how
> to do this, because their understanding of seriously alternative
> foundations is simply too closely tied with some special mathematical
> situations that are not compelling from first principle thinking.
> 
> 3. Most think that this is not an important criteria for a seriously
> alternative foundation for mathematics. I suspect that some minority
> do think that it is, but more in the public relations sense, not in
> any deep intellectual sense.
> 
> So there you have my assessment of the so called "communications problem".
> 
> When I explain standard f.o.m. from first principles, I don't tell you
> to go learn some complex variables or algebraic topology or finite
> group theory or differential equations. I present it from first
> principles, and YOU pick something YOU like to think about, ANYWHERE
> in math, and see how this works for YOU. Now that's general purpose.
> Ideally, you may need very modest doses of this, but the main point is
> that you get to pick if you want a reference point and see it in
> action.

No.  But I beg your indulgence here.  I hope to respond further
in future.

I cannot refrain: No.  First complex variables.  Then, well
later, set theory.  After all I think Cantor began working on set
theory when he faced a puzzle about where a Fourier Series could
converge.

Please forgive one more squib: Few people, except professional
mathematicians, or people who have studied seriously some good
popular works, are willing, easily, to believe in the concept
"arbitrary subset of a set".  They are much more likely to grasp
the idea, let us speak vaguely here, of elements "constructed",
ridiculous word, by ordinary, pre-Cantor, mathematical arguments.

oo--JS.


> 
> When you are willing and able to do this for your alternative
> foundations for mathematics, you have a seat at the foundational
> table. You may have to vastly improve on what you have before you can
> get that seat at the table.
> 
> Actually, at this point, I have no idea how far you are from a seat at
> the table. Maybe you are not too far, and I can lift you up and carry
> to over there and sit you down. Maybe you are essentially there and
> are missing maybe two sentences from somebody like me.
> 
> Harvey Friedman