[FOM] New Umbrella?

[Jay Sulzberger]

On Tue, 28 Oct 2014, David Posner <dposner at sbcglobal.net> wrote:

> I think it's pretty obvious that this discussion is not really
> about which formal system can formalize what.  I think people
> are pretty clear about that.  Nor is the discussion about the
> practicality of the competing systems.  It's ridiculous to
> believe that the HoTT people have spent all this effort on a
> system that doesn't make their lives easier.  The discussion is
> about the religion of mathematics.  The HoTT people will
> naturally want to claim that HoTT provides a superior FOM.
> Just as naturally, people invested in the set theoretic FOM are
> going to object to this claim.  Jobs are at stake!  Formerly
> respectable mathematicians might have to become programmers or
> something awful like that.  Professor Awodey you shouldn't be
> shocked when the discussion gets a little hot.  What's
> frustrating is that the proponents of HoTT are beating around
> the bush trying to reduce the fundamental question about God
> the Universe and everything to picayune technical issues.  So
> tell us HoTT people: why should mathematicians believe in the
> HoTT version of the mathematical universe.  In particular why
> should I want to live in a world without real models?

1. Because the old fashioned models gotten by Koenig's Lemma and
some generalized Principle of Surveyability by Us are odd things,
despite Cantor's work and the work of his editors and his
followers.  The New Crazy Types movement is also a reactionary
movement and revives, we hope one sheet above where we were
before Cantor, the research into "what is it to know an object of
mathematics".

2. Because paying careful attention to what depends on what in a
proof helps us to see what to do next, and often what to do
sideways.  To sustain such careful attention to seemingly tiny
details is often difficult for creatures of flesh and blood, and
New Crazy Type Theory offers recipes for how to write computer
programs which handle these dependencies.

3. Because proofs really are also mathematical objects, and there
are connections between the shape of the proof and the shapes of
the objects under discussion.

4. Because the Curry-Howard Theorem, in its first simple and
solid and clear version, namely that for the simply typed lambda
calculus in the style of Church, shows us that the set of all
proofs comes with a native combinatorial topology, the topology
of lambda conversion, which convincingly gives a formalization of
the notion "Proof P0 of statment T is the same as proof P1.".
Thus we suspect that there is something to the Curry-Howard
Program, whose slogan is "You got a logic?  We got a topology on
all proofs of your logic.".

5. Because theories in the lower predicate calculus may be
arranged into a presheaf, old fashioned sense of "presheaf".
Every sentence s of the lower predicate calculus has a set of
predicate, function, and constant symbols associated to it,
namely the predicates, functions, and constants which appear in
the sentence.  Call this set of predicates, functions, and
constants the "signature of the sentence s".  So given a set of
sentences we may take the union over every sentence in the set of
the signature of the sentence.  Thus every theory has a
signature.  So given any signature sig we may define a set of
theories, namely all theories whose signature is contained in
sig.  The set of signatures SS is a partially ordered set, thus a
category, where sig0 -> sig1 just when the set sig0 is a subset
of the set sig1.  The map ST: SS -> SOSS, where SOSS is the
category with objects sets of sentences of the lower predicate
calculus, and

   ST(sig) = {theories with signature contained in sig}
   ST(sig0 -> sig1) = the map which takes a theory th1 \in ST(sig1)
                      to th0, the set of all sentences in th1 which
                      have a signature contained in sig0

is a contravariant functor.  Because every object of SOSS is a
set, namely a set of sets of sentences, ST is a presheaf.  We may
now do topology starting with ST.  The best introduction to these
presheaves is, ah, I cannot find the paper I thought I had a note
of, but here are some in the line of advance:

   Contextual Semantics: From Quantum Mechanics to Logic, Databases, Constraints,
   and Complexity by Samson Abramsky:
   http://arxiv.org/abs/1406.7386

   The Sheaf-Theoretic Structure Of Non-Locality and Contextuality
   by Samson Abramsky, Adam Brandenburger
   http://arxiv.org/abs/1102.0264

   Relational Databases and Bell's Theorem
   by Samson Abramsky
   http://arxiv.org/abs/1208.6416

   The Cohomology of Non-Locality and Contextuality
   by Samson Abramsky, Shane Mansfield, Rui Soares Barbosa
   http://arxiv.org/abs/1111.3620

And one step, indirect, in the line of advance:

   Intersecting families of sets and the topology of cones in economics
   by Graciela Chichilnisky
   http://www.ams.org/journals/bull/1993-29-02/S0273-0979-1993-00439-7/S0273-0979-1993-00439-7.pdf
   The arXiv pdf version of this paper is missing the pictures:
   http://arxiv.org/abs/math/9310228

   The Laws of Thought,
   on which are founded
   the Mathematical Theories of Logic and Probabilities.
   by George Boole
   http://www.gutenberg.org/files/15114/15114-pdf.pdf

More and fuller answers in a bit, I hope.

oo--JS.