So I recommend keeping at least one or two problems 'on the go' at all times. This, to my mind can be effective, especially in emotionally charged situations like the holidays. All this accounting of things accomplished or not, opportunities taken or missed, goals and deadlines swashing by, can lead to cyclic feelings of inadequacy. We don't need that, we have enough work to do. Our work is cut-out for us!
2021 was a very difficult year for most of us: the pandemic which looked like it was receding in the Spring (at least it looked like that in California, when the vaccine became available) came back, showing that it hasn’t been tamed. Yet, we hope. But we mourn the thousands and thousands that were taken too soon. The economic crisis, brought about in part by the pandemic, is just starting to unfold. (Economics is always a few steps behind politics: it’s much harder to tell the numbers of deaths it causes.) The climatic crisis catastrophes, not as bad as they were in California in 2020, are still very much with us: we have droughts, wildfires, floods, you name it…
Against this backdrop of suffering, it feels almost inconsiderate to think that I am working exactly on what I wanted to for so many years. It feels good to tell people that the Topos mission is to “shape technology for public benefit by advancing sciences of connection and integration”. And it is great to have similarly minded people to do it with! Topos is still starting, but we believe in community, diversity, equity and inclusion; and we’re working for that.
The challenges are enormous: they go from curbing the arrogance of mathematicians and tech people who think they know how to do others’ work better than themselves, to convincing biologists, social scientists, and humanities researchers that we can bring something to the table, in a respectful manner. But if the challenges are considerable, the payoff is incredible. We hope not only “To invent the future” (as in a previous place), but to invent a just, sustainable and equitable future for us all. Thank you for all the joint work, friends!!
Both Davide and Matteo (far above) and Elena and Wilmer (just above) are presenting our joint work at SYCO (Symposium on Compositional Structures) tomorrow and the next day. Good luck friends!
Now this is just one slice of the work. Below to the left, we have our little annotation on NLI group: Katerina, Martha, Annebeth and Livy. To the right Elaine talking at the meeting about 'Women in Logic in Brazil 2019'.
Now there are several other people that I should be adding pictures of in here. Amongst others Luiz Carlos Pereira, Samuel Gomes da Silva, Jacob Collard and Eswaran Subrahmanian. But I am very tired now, so just one more group picture.
Happy Holidays!
I am very proud of this Dagstuhl meeting and wish I could organize another, as Dagstuhl is a great place to do science of high quality. Looking at the abstracts 22 years later, it is very interesting to see the trends that turned out to be very productive. In particular, David Pym and Peter O'Hearn's "Bunched Logic" made its' first appearance in the seminar and it did go places!
`In the past fifty years, the dialectica interpretation proposed by Gödel has become one of the most fundamental conceptual tools in logic and the foundations of mathematics' says Thomas Strahm in his introduction to the special volume of Dialectica dedicated to 50 years of the original paper. Shame that despite being more than ten years old (2008) the articles are not open access, so you can read about them in Richard Zach's blog post, but you'll have to find the articles themselves in the authors' pages or somewhere else.
`Gödel’s functional interpretation can be seen as a possible realization of the so-called modified Hilbert program in the sense that it enables a reduction of a classical system to a quantifier-free theory of functionals of finite type, thereby reducing the consistency problem for the classical theory to the consistency of a quantifier-free system of higher-type recursion, the latter being informally more finitistic and sufficiently well understood. Gödel’s interpretation of arithmetic has been substantially extended in the past fifty years both to stronger and weaker theories. In particular, versions of the dialectica interpretation have been proposed for impredicative classical analysis, subsystems of classical arithmetic, theories of ordinals, predicative subsystems of second order arithmetic, analysis with game quantifiers, systems of feasible arithmetic and analysis, admissible and constructive set theories, as well as iterated arithmetical fixed point theories. A comprehensive survey of many of these results can be found in Avigad and Feferman (1995) as well as Troelstra (1973). In more recent years, work on functional interpretations has shifted from purely foundational purposes to applications to concrete proofs in mathematics in the sense of Kreisel’s unwinding program. In connection with this, Kohlenbach’s proof mining program provides very impressive results making use of variants of Gödel’s dialectica interpretation.'
So far, so good. The mathematicians interested in foundations ought to be happy. I am. Especially because Davide Trotta (above) spoke last Thursday in the Ottawa Category Theory Seminar about our second paper together with Matteo Spadetto. This is "Dialectica Logical Principles" which explains how our categorical modelling of Gödel’s dialectica interpretation also models the principles of Independence of Premise (IP) and Markov's Principle (MP), just like the dialectica does. This is not surprising, but it underscores how faithful the modelling is, a big win for categorical logic. Just like our previous paper, The Gödel Fibration, which is nice because it puts some more explicit steps in the connections between the categorical modelling and the logical system modelled: see the case of quantifier-free objects discussed here.
But 'mathematicians interested in foundations' is a very small demographic. What can we say to others? What about the mythical "person-on-the street"? Have been thinking a lot about it. Recently google Scholar sent me news about Modal Functional (“Dialectica”) Interpretation (by HERNEST AND TRIFONOV. Maybe this will help.
So I thought I'd record some of our conversations--or perhaps a cleaned up version of them. This starting one could be called "Lies Math Teachers Tell us", as it's a list of things that are wrong, but many people in maths departments (or coming out of them) believe to be true. The ones I'm about to discuss are mostly about Natural Language, which contrary to widespread belief (cf. Emily Bender's Rule) is *not* a synonym for English.
The list goes as follows, for the time being:
1. Natural language is not TOO HARD to be modelled mathematically. We have plenty of models, some better than others. Natural language semantics is all about it and many researchers spent decades producing a body of literature that shows the difficulties, but also the progress that has been made.
Of course there's no point in all mathematicians trying to do it. As any other application of mathematics, some people like it, some don't. But saying that it cannot be done, is plainly wrong.
2. Just because I say it's possible to do it, it doesn't mean that I think it's easy.
Ambiguity is not a bug of Natural Language, it's a feature. A feature that evolution has been working on for thousands of years. This is one of the features that makes the subject difficult to model, but it's also why it's so fascinating: we can do wonderful things with words. And all so easily that we take it for granted. Like breathing, we only noticed we're doing it, when somehow the mechanism has problems.
Finesse and sophistication are necessary. The exercises we give in the logic books about formalization of sentences, won't cut it in real life. We don't communicate in sentences used to teach 5-year-old kids how to read (that is, unless this is what we're doing). We understand these sentences too, mostly, but the effort to create a formal model of the language needs to be in the direction of all kinds of sentences: from the abstruse Law contract constructions to slang on Twitter.
This suggests two different implications.
3. We need to deal with intensional phenomena. It's no good saying, I can ditch, say, attitude predicates, and only add them as a bonus feature later on. As we argued, as a collective (rdc+) in `Entailment, Intensionality and Text Understanding', intensionality, which is widespread in natural language, raises a number of meaning detection issues that cannot be brushed aside. I will not repeat the arguments here, as I think they are clearly expounded in the paper.
4. Coverage of different types of text is essential. Anyone can build a model that deals with only their ten favorite sentences. That is not what we're talking about, when we talk about a model. Models need, in principle, to be able to deal with any sentence we throw at them.
Now, a controversial one.
5. Models need to be compositional. This will not bother my kind of mathematicians, as category theorists do believe that compositionality is key to all modelling we do, but it will be controversial to some. So I will postpone this side of the conversation for a little while.
Ok, quite a few times I was late with the goods, but this is OK, I reckon. I also varied quite a lot my own criteria for choosing honorees: I started with a deceased female mathematician thinking that there would be more consensus on them, but then moved on to living people, as consensus is overrated (systemic sexism, anyone?) and other criteria maybe should play a role. So interdisciplinarity has been a favorite criterion. My list so far consists of
