Sets, Types and Categories

Joao Marcos managed to establish, quite a few years ago now, a Brazilian mailing list of logic and logicians. This can be very useful at times. (Some times I just despair of humanity. But this is the essence of mailing lists, I suspect.)

Anyways there was a good discussion over the Christmas break and I thought I should summarize it here for my own future benefit.

The discussion started with JM pointing to a question on some unsolved problems in mathematics. The answers were not about mathematics, but about Set Theory and Andrej Bauer had a pithy comment, as pointed out by Vivek Nigam:
"Logic of the early 20th century was a reaction to a conceptual and methodological crisis in mathematics. Logic of the early 21st century is the tool for conquering the newly discovered land of computer science. Now is a good time to be an Edison or a Tesla of logic, and a little less a Cantor or a Russell. (It's always good to be a Gödel or a Turing, of course.)"

I commented that it's always good to be some one like Cantor or Russell (captain-obvious that I am) and that, despite liking Andrej and logic in computing very much, I  thought he was being too narrow-minded with this observation, as logic is going plenty of other places too.  Mind you, I have talked about computing being the physics of this century in several places, as far as questions, challenges and theories in mathematics goes. So I'm not disagreeing with Andrej, only saying that he should've gone further.

Because I was having a different discussion in facebook, I posted a link to MacAllester's post on a new foundation for mathematics, saying that I disagree with his solution very much, but that people in the list may find it interesting (it's the kind of discussion to have after too much good food and wine, I say). Decio Krause asked me why. I recalled Vijay Saraswat's description of the issue:

(a) One is looking for a framework for mechanically checkable mathematics, much in the way Coq can be used to mechanically check proofs of correctness of various algorithms. (e.g. various theorems related to semantics of programming languages or properties of type systems). (b) A starting point is Martin-Lof's (constructive, dependent) type theory. (c) The underlying notion of type in this framework has proven hard to pin down mathematically. (d) Homotopy theory is claimed to provide some mathematical understanding of types. (e) Hence the enormous interest in HoTT amongst logicians and theoretical computer science (semantics) folks. (f) David is trying to develop a similar framework but based on classical rather than intuitionistic ideas, he wants to retain  the power of "Platonic" worlds and reasoning.

and explained that I agree with MacAllester that there might be a need for a new foundation, but then I don't like his solution.

But then something interesting happened, JM posted a link to Tom Leinster's Rethinking Set Theory, which is pretty impressive. To me at least. Looks sane and sensible, I like it a lot.

I  posted Steve Awodey's From Sets to Types to Categories to Set and lots of discussion ensued. Steve starts his manifesto with:

Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby.

Forced by Decio's question "Valéria, Será que o autor consegue falar algo que não saibamos?" I had to read it, which was good as I was thinking about the subject in any case, given the beautiful write-up that Samuel just produced on our work on categorical understanding of set theoretical cardinalities of the continuum.

So here are my own personal preliminary conclusions, half-translated from Portuguese.

Just til page 11 I knew the constructions that make up his "triangle". Thus what is new to me, who hadn't stopped to think about the consequences of the functors in the triangle, are his conclusions in section 5. Awodey says:

1.The first and most obvious conclusion to be drawn from this is that the three systems of foundations are therefore mathematically equivalent.[...] This is perhaps the definition of the “mathematical content” of a system of foundations, i.e. those definitions, theorems, etc. that are independent of the specific technical machinery, that are invariant under a change of foundational schemes.

yay, this works for me!!

2.the objects of type theory and set theory are structured by the operations of their respective systems in certain ways that are not mathematically salient.[..] Categorical structure is closer to the mathematical content, and it is not lost in translation. Equivalence of categories preserves categorical properties and structures, because these are determined only up to isomorphism in the first place.[..] The structural approach implemented by category theory is thus more stable, more robust, more invariant than type or set theoretic constructions. 

Again I like it a lot! This of course does not solve all my problems, all three vertices  of the triangle have their own problems and challenges. 

E da minha parte, como "brinco" entre a teoria de categorias e as `type theories' da vida, as vezes tendo pra um lado, as vezes pro outro. Por exemplo no Unilog de 2005, (junto com a entao minha research assistent Milly Maietti que e' super fan de type theory), eu defendi uma posicao mais pra TT na competicao de como devemos definir logicas. Naquela altura eu estava dizendo que o que a gente precisa 'e de uma sintaxe forte que prove "internal language theorems" pra gente. Mais recentemente venho dizendo que talvez seja melhor firmar sua intuicao nas categorias, pois a sintaxe a gente acaba acertando... Nao sei, nao tenho certeza. 

Como eu acredito na conclusao de que essas coisas sao mesmo "mathematically equivalent"  posso trabalhar tranquila com o Samuel no universo dele que tem Choice(de todo tipo), tem elementos, tem infinitos completos, o escambau.

Anyways, I think the whole episode was very productive, despite a few mishaps. And I would like to thank JM, Decio, Rodrigo for all the knowledge imparted.