Month: September 2020

Smallism

~ David Roberts ~ Leave a comment

A new class of philosophically-minded mathematician that I just learned from the logician Paul Levy: smallist.

CH is a statement of third-order arithmetic. It doesn’t quantify over the universe of sets. GCH, on the other hand, does. For smallists, who take a platonic view of PPN (powerset of powerset of the naturals) but not of the universe of sets, this is a big difference. (http://www.cs.nyu.edu/pipermail/fom/2016-October/020149.html)

I guess it means a mathematician who doesn’t necessarily want in their axiomatic system arbitrary powersets, rather just the few that are needed for ‘ordinary’ mathematics (say up to PPPN, which is plenty to deal with differential geometry, differential equations, functional analysis, number theory, algebraic geometry over number fields or rings of integers therein etc). I think he just invented the word 🙂 but I like it. For a categorically-minded person like me, this means I could work in a pretopos with just a few powersets posited.

(Originally posted to Google+ on 11 November 2016)

MathOverflow question seeking answer, offering bounty

~ David Roberts ~ Leave a comment

Last year I asked a question titled Direct comparison zig-zag between cochain theories on MathOverflow, and it has still no good answer. I’ve offered a bounty, and no takers yet. The satisfaction is yours for the taking! To quote from the end of the question:

…my hope is to show that the class of cochain theories is connected, assuming one exists, and then exhibit one. This may well be singular cohomology, or it might be something else. In particular I want to remove from the proof of uniqueness the privileged position that any one construction has. The only caveat is that I won’t be able to use any super-sophisticated machinery as this is a first course in algebraic topology. I’m happy to have an outline of how to unwind a sophisticated proof.

Want to see the real secrets of set theory in YouTube format?

~ David Roberts ~ 5 Comments

tl;dr Set theorist Asaf Karagila is looking for YouTubers to collaborate.

My colleague and sometime rival Asaf is a top notch young set theorist who works a lot on pushing the frontier of the method of forcing. At one point we were in competition to construct, without using large cardinal assumptions, the first model of set theory where the axiom WISC failed. Asaf won, but as I was working in a different formalism, I still had the satisfaction of arriving at my own solution. This was right at the start of his academic career, and he’s only gone from strength to strength, recently being awarded a prestigious UK Future Leaders Fellowship.

The upshot is, he included explicitly in his Fellowship application that he would produce outreach videos about set theory, and is looking to collaborate with YouTubers with wide reach to achieve this. As he writes:

“There is a clear lack of good videos addressing set theoretic ideas, which I honestly believe that I can make at least somewhat accessible. And hopefully this will make set theory more accessible to the public, or at the very least, to other people interested in mathematics.”

He has set up a contact email if you are a YouTuber:

At the moment I’ve set up an email address, youtube2020@karagila.org, where you can email me. Let me know about your channel, what kind of content you want to make, etc. I cannot make any promises about money, but I’m always happy to advise with regards to content, should the need ever arise.

And if you are not a YouTuber, but want to see some more nitty gritty about what it is that set theorists do nowadays, point them to Asaf’s blog post! Asaf tells me that Numberphile and Tibees have already made contact, but if you are super keen to support the idea, it would help if viewers promoted the idea.

Now, if YouTubers want to make videos about category theory, on the other hand, then, ahem, I don’t mind having a chat 🙂 But they should talk to Asaf first, I don’t want to intercept his efforts!

Initiality conjecture for full Martin-Löf type theory

~ David Roberts ~ 1 Comment

Next Thursday, 10th September, Guillaume Brunerie and Peter LeFanu Lumsdaine are going to present a talk Initiality for Martin-Löf type theory in the HoTT electronic seminar … with a proof of the initiality conjecture!

Here’s the abstract:

“Initiality” is the principle that the term model of some type theory should be an initial object in the category of models of that type theory.  Thomas Streicher gave a careful proof of initiality for the Calculus of Constructions in 1991.  Since then, initiality for more complex type theories (such as Martin-Löf type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.
Around 2010, various researchers (notably Voevodsky) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof.  Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.
In this talk, we present a proof of initiality for a full-featured Martin-Löf type theory.  The proof is formalised in Agda, to dispel any question of thoroughness (and also partly formalised in Coq), and is carefully designed for extensibility to other type theories.  The proof is based on Streicher’s, using some improvements of Hofmann and further refinements by the present authors.  The two formalisations present slightly different versions of the statement — using contextual categories in Agda, categories with attributes in Coq — but the core of the proof is parallel.

Joint work with Menno de Boer and Anders Mörtberg.

This was a big concern of Vladimir Voevodsky and it’s good to finally have it sorted out, with a formalised proof, as it should have.

Unfortunately it’s live at 1am, so I’ll have to grab the recording…