[FOM] Alternative foundations?

[henk]

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