[FOM] Alternative foundations?

[David Roberts]

Hi Victor,

>So, I wonder, what  is this "effort underway to overhaul the foundations of
math in which set theory is no longer central."

The Univalent Foundations program, in which Voevodsky, Awodey and
Coquand play a central role. See, e.g.

http://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics
http://ncatlab.org/nlab/show/homotopy+type+theory (many references at
the bottom of the page)

The objects not in general representable as sets are intensional
types. Some types are (or behave like) sets, but not all of them. The
key part is that equality is not what it usually is in set theory, and
in fact, as I understand it, the substrate of logic is subsumed into
the type theory, rather than sitting behind/under the usual axiomatic
material.

François Dorais has some blog posts discussing what it means to do
"proof relevant" mathematics, which is part of the framework:

http://dorais.org/archives/tag/hott

David



On 19 February 2014 01:28, Victor Marek <marek at cs.uky.edu> wrote:
> In (New York Times) Book Review of February 16, 2014, there is a piece by
> Professor Edward Frenkel of Math/UC Berkeley, entitled "Ad Infinitum." This
> is a review of a book by Max Tegmark, a physicist from M.I.T. The book in
> question is entitled "Our Mathematical Universe" and appears to be one of many
> recent books presenting (an absurd in my opinion, and certainly untestable)
> hypothesis of existence of multiverses (other texts on this hypothesis include
> books by David Deutsch and by Brian Greene).
>
> Regardless of the merits of the multiverses and other antics by physicists,
> a fragment of the review caught my attention, as it pertains to FoM.
>
> Here it is verbatim:
>
> "I tried to process this information, but didn't feel much. Let's go back to
> the notion of `mathematical structure.' We read in the book that it is a `set
> of abstract elements with relations between them,' like the set of whole
> numbers with operations of addition and multiplication. However there is a lot
> more to math than such mathematical structures. Objects other than sets are
> necessary and they now become widespread. Moreover, there is an effort underway
> to overhaul the foundations of math in which set theory is no longer central.
> So mathematical structures constitute but a small island of modern mathematics.
> Why would someone who believes that math is at the core of reality try to
> reduce all of reality to this island? Where would the rest of math then reside?
> Unfortunately these questions are not addressed."
>
> So, I wonder, what  is this "effort underway to overhaul the foundations of
> math in which set theory is no longer central."
>
> Of course, with the logic education from 1960ies, it must be me who is behind
> times, not Professor Frenkel. Still, maybe we should try to see what are these
> efforts to overhaul Foundations of Mathematics. Specifically, what are these
> objects that are not (representable as) sets?
>
> I believe Professor Frenkel opinions bear on the business of FoM, and maybe we
> can see what is going on in the communities beyond FoM.
>
>
> Victor W. Marek                                 Department of Computer Science
> marek at cs.uky.edu                                        University of Kentucky
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom