[FOM] Alternative Foundations/philosophical

[Steve Awodey]

Oops — that was obviously intended as a private message, not for the entire FOM list!

Embarrassed,

Steve

On Mar 4, 2014, at 4:26 PM, Steve Awodey <awodey at cmu.edu> wrote:

> Dear Bas,
> 
> I don't really see the connection -- my paper is about the univalence axiom specifically, not the general program of univalent foundations.
> BTW: I think it's at best pointless, and at worst dangerous, to provoke these people into further discussion of HoTT -- they don't know anything about it, but their minds are already made up
> 
> Regards,
> 
> Steve
> 
> On Mar 3, 2014, at 5:57 AM, Bas Spitters <b.a.w.spitters at gmail.com> wrote:
> 
>> Steve Awodey, Structuralism, invariance, and univalence.
>> https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
>> 
>> Contains answers to many of these questions.
>> 
>> 
>> On Thu, Feb 27, 2014 at 5:05 AM, Jay Sulzberger <jays at panix.com> wrote:
>> 
>> 
>> 
>> 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.
>> 
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>> 
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140306/d274cadf/attachment-0001.html>