Gödel Fibration?

 

A quick blog post in what I hope will be a series on papers out this year. Three of these papers are now on the arXiv and Google Scholar, yay! The Godel Fibration, Dialectica Petri nets and Kolgomorov-Veloso Problems and Dialectica Categories.

The Gödel fibration with Davide Trotta and Matteo Spadetto is very special to me, as it's my first attempt at a logical generalization of the Dialectica construction. Yes, starting with Martin Hyland in 2002 (`Proof Theory in the Abstract' for a celebration of Anne Troelstra's work)  many other people have worked on these ideas. Amongst others, Bodil Biering in her PhD thesis, Pieter Hofstra's paper in honour of Michael Makkai (The dialectica monad and its cousins) and then Tamara von Glehn and Sean Moss phd theses  (also jointly). 

In the early 90's at the Durham category theory meeting, Bart Jacobs, Thomas Streicher and myself had a long conversation about generalizing dialectica to dependent types, and this became the `famous' exercise in page 117 of Jacob's book. I knew I couldn't reproduce the result of that conversation, but was surprised when I couldn't get either Bart or Thomas to write it for me a few years later: they had moved on. 

 So it was very nice when Davide contacted me with a question about weak coproducts  in the category DC and we ended up, with Matteo's help, writing the Gödel fibration preprint. I am really excited  to pursue the ideas of categorical proof theory as we do in this paper. If you think about it, we have learned from Bill Lawvere more than 50 years ago how to model existential and universal quantifiers using a triple of functors in two adjunctions (for substitution, for all and there exists). It's surprising and interesting that we didn't know how to say categorically that a formula is universal-quantifier-free (or existential-quantifier-free, if you prefer). These notions are the crux of the argument in our paper, which we hope to develop a bit more in the next months.

Looking for Bill's website I fell once again into the delightful rabbit hole of reading his lovely commentaries on friends departed. In particular, I had not read  his tribute to  Aurelio Carboni and it's really very nice!

Lazy Days of Summer? Bah, humbug!

 Maybe this would be Dickens' reaction.  or more likely the Muppets' one. Be that as it may, when the very idea of doing the things you enjoy becomes tainted by rage and outrage, maybe it's time to think again. 

There are many situations in the kind of work that I do that remind me of AYSO under-8 football--or soccer, if you insist. One of the hardest things to pass on to the kids is the need to think like a team: all of them want to be strikers, all of them run in a messy swarm towards the ball, there's no one in the defense, no one positioned to lead a new kind of attack, they can only see where the ball is, this second. Category Theory can feel exactly like that: an awful lot of mental energy gets dissipated in the competition for a few seconds of playing ball. This is not my style, it has never been.

By the way,  the picture has nothing to do with these darker thoughts. This was just a warm and fun conversation about "Proofs and Programs", part of the Logic Colloquium session organized by Monika Seisenberg. (my contributed presentation, which was only 20 min, was the same day for me, but the next day in Poland. funny to see the consequences of a round Earth in practical life!)

Congratulations to the Polish organizers of the Logic Colloquium! A huge challenge and they did it all extremely well. Thus I'm hoping to have hybrid versions of the Logic Colloquium henceforth!  I'm also looking forward to next year's Logic Colloquium in Reykjavik, Iceland!

Organizing work

is never easy! Since the office "opened" I've been trying to get there every Friday. 

Last Friday I went by BART to see if this is easier or not. Even going by car very early, it takes at least one hour and a bit to get there and more to come back. And the stress of driving these busy roads and bridges is palpable for someone like me who doesn't like to drive.

Cousins: twice removed?

 A long time ago I wrote a paper Dialectica and Chu constructions: Cousins?(Theory and Applications of Categories, Vol. 17, 2006, No. 7, pp 127-152) because I felt that the Chu construction and the Dialectica construction were similar in some ways, but still very different from each other in other ways.  I wanted some nice, explanatory result connecting the two. I didn't get the nice smooth and informative result that I wanted to get, but at least I got to write down some obvious facts I knew and this was better than nothing. (I still don't know if there are beautiful smooth results to be found. one lives in hopes.) 

Michael Shulman did produce a nice generalization of both constructions in his The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions (2018), but it is still not clear to me that this is the best that we can say. Mike is generalizing the usual 1-categorical Chu and Dialectica constructions into 2-categorical constructs. Going into a different generalization direction  Sean Moss and Tamara von Glehn, in their LiCS paper 2018 (Dialectica models of type theory), generalize the Dialectica construction to deal with dependent types, by starting with a fibration p and constructing a generalized Dial(p).

This is very interesting as their paper indicates that the first of their two models for the generalized Dialectica actually corresponds to some category of  "polynomials". In page 8 they say

We are now ready to give the first of our Dialectica constructions, the polynomial model introduced in [34]. The name, which we explain below, fits while we are considering the predicate-free Dialectica construction. 

 This observation leads us to think of  "polynomials" as a predicate-free Dialectica construction, but it is not clear (at least to me) how to make an honest mathematical statement out of this analogy. Which kind of functor should we have? Can we do it for the  'simply-typed'  original Dialectica? Or do we have to introduce fibrations into the picture? The models in von Glehn's thesis (and in the paper) are not exactly simple: it is a tour de force to provide the dependent products in the paper. 

In any case the analogy seems to be that both polynomials and Dialectica constructions seem to correspond to  a big Sigma followed by a big Pi Something, or

   

Now if the Chu construction and Dialectica looked like cousins in 2005, polynomials look much more distant from Dialectica as I know it, hence the title of this blog post. I am trying to write down the bits of mathematics that I know work. It might take a while. 

On the other hand, I just discovered "POLYNOMIALS, FIBRATIONS AND DISTRIBUTIVE LAWS". Maybe Tamara has already sorted it out everything I wanted to know and I just hadn't realized it. Will be reading it now.

Women in Logic 2021, yay!!

 

We just had another great edition of Women in Logic! Congrats to the organizers Sandra Alves, Sandra Kiefer and Ana Sokolova for a fun, challenging and  diverse meeting! Thanks also to our Invited Speakers Professors Simona Ronchi Della Rocca (Università di Torino) and Rineke Verbrugge (University of Groningen) for very inspiring talks!

This time we didn't have any incidents like last year (my write-up of the incident last year is in https://logic-forall.blogspot.com/2020/07/the-curious-incident-of-dropped.html, if you want to see it), but on the other hand we didn't have the streaming either and this is not so good. 

We are a small workshop, so we follow what the conference we're associating with says; and I think it's fair to say that the main issue this year has been the registration fee, which was plainly terrible. This came as a surprise to me (and, I believe, to everyone else too!). Since last year there was no registration fee for the workshop, I thought this year was going  be the same. After all,  our workshop is about logic work done by women, but it is not exactly a huge source of brownie points (or commercial value) to anyone. We help people get used to presenting their work, in other more 'hostile' environments, and I have been extremely impressed with the quality of the work the young ones do. They get some amount of mentoring on their papers and on dealing with questions, misunderstandings, etc. But for the audience, which is there to cheer them on and to learn a few things about their work, to pay 30 euros for a single day seems excessively expensive! 

After all, the silver lining of the pandemic and of the lockdowns had been the possibility,  for many, to interact with their academic heroes, to watch seminars that happened in all parts of the world, "to be" in Australia one day and the next in Colombia, while still hearing about your favorite subject. That now people insist on gatekeeping these possibilities, by making the conferences unaffordable, seems perverse.

I understand that even online conferences have costs that need to be paid, but I worry that calculations and sponsorships are following outdated models. And I believe the push to make it more accessible needs to be done by everyone in the community, not just a few. Otherwise, the prestigious conferences will carry on being unaffordable, reproducing the sins of the conventional publication model.

Why are videos so difficult to find and keep?

I wanted to make a list of the videos I've recorded recently. 

I thought this would be what a youtube channel meant: a place where you put your own videos. I simply wanted to copy these videos from some other places. For example the talk I gave in the Logic SuperGroup, the one in the Proof Theory Seminar,  the one at the MIT Category Theory, etc. 

And it's probably just me being stupid, but this seems very hard to do.

Ok, the videos are very big and take a lot of space and of time to process. But surely, there must be an easy way to do something like what I want.

Anyways for the time being, here's just a collection of links to talks I've given.

1. Structural and Distributional Meaning Representations Logicos em Quarentena  SBL

2. Dialectica Categories for the Lambek Calculus Logic Super Group

3. Natural Language Inference for Humans women+@DCS Sheffield

4. Benchmarking Linear Logic Proofs  Augusta Colloquium 

5. Relevant Dialectica Categories MIT Category Seminar

6. GraphKR Semantic Parsing for Portuguese Fundacao Getulio Vargas 

7. Benchmarking Linear Logic Proofs Proof theory Seminar 

8. Dialectica Categories: the mathematical version BACAT Meet-up 

9. Ontologies and Semantics for Portuguese Painel Ontobras 

10. PUC-Rio: Digital Technologies and the Areas of Human Knowledge 

11.  World Logic Day video Ambassador of Logic

12. A semantica nossa de cada dia EBCT 

13. Categorical Models for Explicit Substitutions  UnB

14. Entre a cruz e a caldeirinha  Brasileiras no PLN

15. LL for Constructive Mathematics   Working Logician

16. Dialectica and Kolmogorov Problems Finding the Right Abstractions

17. Constructive Modalities Celebrating Women in Mathematics   

We also organized Logica e Representatividade in 14 January 2021 and I was invited to the Emilia's Podcast, which was a blast. Many thanks to Adolfo Neto e Maria Claudia Emer for the fun chat!

Spring has sprung

 

Spring has sprung and knocked me off badly. Had a horrible dental surgery, four hours plus on the dentist chair with billions of bad things happening. This was on Tuesday. Thought, oh dear, I guess I miscalculated how bad this was going to be, now, I will take my medicines and be back on my feet tomorrow. ho, ho, this was the good day. My body mounted a united front against the medication prescribed (medication that I had had several times before) and I got to feel really weak, as I kept being sick several times a day. 

Not good, not good at all. I'm finally better, touch wood, and  now I have read Terry Pratchett's Nation and I loved it. 

I was reminded of the many reasons why I love Pratchett's books: they do make you think about the important things in life in novel ways. My favorites are the Witches stories, I love all the witches, but Granny Weatherwax is a favorite: "If you want to amount to anything as a witch you got to learn three things. What’s real, what’s not real, and what’s the difference.” 

“We look to… the edges,' said Mistress Weatherwax. 'There’s a lot of edges, more than people know. Between life and death, this world and the next, night and day, right and wrong… an’ they need watchin’. We watch ‘em, we guard the sum of things.  

“You can‘t go around building a better world for people. Only people can build a better world for people. Otherwise it‘s just a cage.” 

Cage or no cage, it's time to go back to thinking about multiagent systems and what do we expect of them minimally. Well, if you have many agents, one expects that each one of them is a reasoning agent on its own and that its reasoning can be of the classical, constructive, linear  or modal variety. And similarly, when considering how they interact with each other, the same possibilities arrive. Thus it would make some sense to compare these kinds of reasoning agents. Something that we want to discuss next.

(when the internet is behaving a bit better and I can upload pictures!)