[FOM] Alternative Foundations/philosophical

[Jay Sulzberger]

On Tue, 25 Feb 2014, Harvey Friedman <hmflogic at gmail.com> wrote:

> I agree with a great deal of what Chow has just said. However, I have some
> problem with a full endorsement of the following from his message:
> \
> "I am sympathetic to John Conway's "Mathematicians' Liberation Movement"
>
> (which of course has also been discussed before on FOM), which basically
> says that we're mature enough now to be able to pick whatever foundations
> we find convenient, knowing that we can always, in principle, translate
> between any two if them if we really want to.
>
> In other words, if a proponent of a new system claims certain advantages
> over the old system, I do not think the reaction should be to get all
> defensive and say, "But I can do that with the old system too!"  Instead,
> one should open-mindedly explore if the new system helps foster new ideas
> that advance the field.  The sooner we abandon childish turf wars, the
> faster mathematics (and the foundations of mathematics) will advance."
>
> There are two aspects of the usual foundations that are generally
> accepted (or are they generally accepted?).
>
> 1. There is a crucial kind of absolute rigor in the presentation.

I think the HoTT/Intutionist-Types school would say that their
foundations are at least as rigorous as any foundations offered
by the party of Cantor, Dedekind, Frege, Peano, and Hilbert.
Indeed some would say that HoTT/Intuitionist-Types approach is
more correct than anything the old incumbents party of
Cantor, ..., Hilbert has on offer.

>
> 2. There is a completely transparent elementary character that is
> relatively universally understandable.

I have not found the presentation in the HoTT book clear, but I
have not studied it enough.

>
> 3. There is a precious kind of philosophical coherence that transcends
> mathematics itself.

HoTT school members tend to think their way is superior here.

>
> 4. It has been used in order to address the obvious great fundamental
> methodological issues, the most well known of which concern whether or
> not propositions can be proved or refuted - both generally and
> specifically.

The HoTT school agrees, and, again, claims their way is better.

>
> A certain amount of this would also be a priori clear for an
> alternative foundation if that alternative foundation was in an
> appropriate sense interpretable in the usual foundation. However, such
> an interpretation is generally not nearly enough to ensure 2.

Ah, I think the meaning of such "interpretations" is also
contested.  If one is too easily satisfied, then HoTT folk would,
I think, complain that the main point is being missed.

>
> How do 1-4 fare with alternative foundations?
>
> With regard to the "liberation Movement", if one is concerned with
> fully complete rigorous presentations, then has history shown that
> generally speaking one either doesn't have this at all, or one has it
> done incorrectly, replete with inconsistencies?

Ah, hmmhn, hrrhnmh, I think no.

>
> Isn't an example of this kind of thing, the idea of using general category
> theory as an alternative foundation, with the "liberated" use of things
> like the category of all categories? Hasn't that been recently shown to
> lead to convincing inconsistencies within the usual mindset of general
> category theory?
>
> Also, has there been a philosophically coherent presentation of altered
> notions of equality? If so, the FOM would benefit greatly from seeing this
> discussed.
>
> Harvey Friedman

The central propaganda effort of the HoTT movement is to persuade
people that indeed the notions of "equality" and of "isomorphism"
of Bourbaki style "structures" are not what most lay members of
the incumbent party think they are.  As for a good textbook
presentation, I do not know of any, but I am not in command of
the literature.

ad comprehensibility: I am encouraged by Robin Adams" paper
"Pure Type Systems with Judgemental Equality":

   http://www.cs.rhul.ac.uk/~robin/ptseq8.ps.gz

because I can parse every sentence I have read in it.  I have not
finished reading the paper.

oo--JS.