[FOM] Alternative foundations?

[meskew at math.uci.edu]

The claims of Frenkel seem to be much grander than this.  Namely:

(1) Objects other than sets are *necessary.*
(2) Alternative foundations will make set theory no longer *central.*
(3) Set-theoretic structures "constitute but a small island of modern
mathematics."

Almost all the advertisements I have seen for Homotopy Type Theory as an
alternative foundation to ZFC set theory focus on the greater ease or
naturalness of formalization and proof-checking available with HoTT. 
While this may be a great virtue, it seems to be only evidence that HoTT
provides a superior foundation for *formal verification* than ZFC, which
was never a goal of ZFC.  But in my opinion, issues of formal coding are
not so central to FOM, which is concerned with the fundamental principles
underlying mathematical truth.

Regarding Frenkel's claim (1), in what sense are the non-set objects of
Category Theory or HoTT "necessary?"  In the same sense that an assumption
is found to be necessary as in Reverse Mathematics or Inner Model Theory?

If Juliette Kennedy is right that all category-theoretic and set-theoretic
approaches are bi-interpretable, this this refutes claims (2) and (3). 
The interpretability of HoTT within ZFC (plus some large cardinals) would
mean set theory remains mathematically central, even if some prefer to
work in a different formal system.  And under such an interpretation,
perhaps it would be rather the structures of HoTT that constitute a "small
island" of the universe.





> To Victor and others
>
> One of the reasons why type theory has something to say that
> is beyond set theory is the following. In contemporary mathematics
> large computations are essential. Think of the use of Groebner bases,
> the proof of the 4CT, and Hales proof of the Kepler conjecture.
>
> Now a FOM has as task to be able to represent proofs, so that others
> can check them. Set theory is a very awkward theory to represent
> computations.
> It can be done in principle, by describing Turing Machines as sets of
> quadruples,
> but then the computational fun gets lost as proofs involving serious
> computing
> become unreadable. In short: set theory doesn't contain a convenient
> computational
> model. This may be one of the reasons that the Bourbaki enterprise did
> come to an end.
>
> Type theory as coming originally from Whitehead-Russell and simplified
> and essentially
> extended by Ramsey (simplifying), Church (adding lambda terms), de
> Bruijn (adding dependent
> types), Scott (adding inductive types with recursion), Girard (adding
> higher order types), Martin-Loef
> (showing the natural position and power of intuitionism) all lead to
> proof-checking based on type
> theory with successes like the full formalization of the 4CT and the
> Feit-Thompson theorem by
> Gonthier and collaborators and the forthcoming one of the Kepler
> conjecture by Hales and
> collaborators.
>
> Now, there are some difficulties with types (which someone else may like
> to describe). For this reason
> there is work in progress by Voevodsky and collaborators to modify this
> theory.
>
> Henk Barendregt
>
>
>
> On 02/18/2014 03:58 PM, Victor Marek 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
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>