Dialectica Logical Principles

 

 `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.

Conversations with Sophie

One of the pleasures of going to Topos on Mondays is the conversations with Sophie in the car journey. Some have been quite revealing to me, as I do believe I think better when talking, then when simply thinking. When talking I need to finish thoughts, complete sentences, all these boring trifles that actually help you make sense. I know, it sounds strange, but rings true to me.

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.

 

Ada Lovelace Day 2021

 So this is the 10th anniversary of me doing Ada Lovelace Day posting, as I started in 2011 with Christine Ladd-Franklin.  From Algebraic Logic to Optics and Psychology this honoree is very fashionable nowadays.

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

Christine Ladd-Franklin(2011), Karen Sparck-Jones(2012), Marta Bunge(2013), Helena Rasiowa(2014),  Nyedja Nascimento(2015), Manuela Sobral(2016), Maryam Mirzakhani(2016), Christine Paulin-Mohring(2017), Angela Olinto(2018), Andrea Loparic(2020).

  This list is very personal and idiosyncratic, of course. It has three Brazilians, five friends, two category theorists. It's not representativie of anything, but my own "on the spur of the moment" decisions. But it reflects more than ten years thinking about the issues that make Ada Lovelace Day necessary. As necessary now, as it was ten years ago, despite big social movements like #MeToo and #BlackLivesMatter. 

One thing I've written a lot about, but that the list does not reflect, is the danger of losing the memory of the fights. Forgetting the plight of the suffragists, forgetting all the sisters that could not get degrees, that worked for free to show women could do the work, the ones that could not stay in academia because the pressure to leave was too huge.

 Now recently, reading the lovely interview of Hélène Langevin Joliot reminded me that this fight is not so old.

She's the real granddaughter of Marie Curie and in this interview she says "It's a myth that the Curies sacrificed their lives for Science".

Hélène is 94 years old, but she still debating, giving interviews, a living link to a past where things were indeed much worse. Like me, like many others much younger, she thought that discussing gender equality was not necessary, had been done before. Like us, she discovered that this fight needs to happen every day, all the days. That things will only be good, when everyone is treated fairly, when inclusivity prevails. So

Hélène is my Ada Lovelace Day heroine for 2021!

oh, if you don't read Spanish you might need to use translation software as Helene Joliot's interview above is only in Spanish, so far. Thanks to Women with Science for making it available.

(I promise to put a version in English here pretty soon!)