[FOM] Alternative Foundations/philosophical

[Steve Awodey]

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

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