[FOM] Alternative foundations?

[Jay Sulzberger]

On Tue, 18 Feb 2014, 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

I think Edward Frenkel means "Homotopy Type Theory":

   http://en.wikipedia.org/wiki/Homotopy_type_theory
   [page was last modified on 27 December 2013 at 04:50]

I believe this work is serious.  Frenkel says:

   If Pythagoras had not lived, or if his work had been destroyed,
   someone else eventually would have discovered the same
   Pythagorean theorem.

Homotopy type theory suggests that there is more than one
Pythagorean Theorem.  Homotopy type theory is part of New Crazy
Type Theory.  New Crazy Type Theory is type theory after Church's
discovery of the lambda calculus.  The advertising team of the
computer programming system Haskell is not entirely mistaken in
their slogan "NCTT gives Haskell Static Strength!".  If one
believes in the lambda calculus' use in type theory then likely
one has doubts about the whole of the theory of the (classical)
lower predicate calculus, as she is taught today in Logic 101.
It took me some years to grasp the connection between recent type
theory and "constructive mathematics", even though most
introductions explained the matter clearly.  A big sinew of the
connection is this:

   In the classical lower predicate calculus we have as part of
   the background, enough classical set theory to produce a wealth
   of models, enough models so that we may prove the Completeness
   Theorem of the lower predicate calculus.

   But, to speak in a misleading way, in NCTT we have no way to
   get an element of a model except by explicitly giving a lambda
   expression which evaluates to the element.

I do not have the paper before me, but somewhere Jean-Yves Girard
states baldly "There are no models.".  This is a more accurate
slogan than my indented paragraph above.

In the usual exposition of most set theories there is no
automatic combinatorial topology associated to a naked set.  More
precisely: there are only two automatically defined topologies on
a naked set, the discrete topology and the trivial all-globbed
together topology.  In homotopy type theory every type has an
associated "homotopy type", which need not be the discrete
"homotopy type", nor the trivial "homotopy type", where "homotopy
type" here means "equivalence class of things homotopic to the
type".  This structure in certain special cases has appeared in
the theory of "Bayesian nets", which are also known as "circuits
of probabilistic gates", and also in Craig's Interpolation Lemma.
The concept of "Riemann surface" is another example.

The study of homotopy types, "types" as in type theory, at the
level of "foundations" has only recently become popular.  Thus
today much is unclear and un-settled, and so the literature is
hard to read.

oo--JS.