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!