[FOM] Alternative foundations?

[Josef Urban]

Isn't Prolog an example how bare classical first-order logic computes?
Josef

On Sat, Feb 22, 2014 at 1:31 AM,  <meskew at math.uci.edu> wrote:
> 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
>>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom