Jérémie Marquès (Università di Milano) will give a talk on
Monadic monadic second order logic (and polyadic transformers)
Abstract:
“Monadic monadic second order logic” (not a typo!) is the title of a 2023 paper by Bojańczyk, Klin, and Salamanca. A less provocative title would have been “Monadic second order logic with monads”. Monadic second order logic, or MSO for short, is the logic in which we can quantify over unary predicates (monadic predicates) and compare them, in addition to the Boolean operations.
In this talk, we will see how algebraic theories (= monads in categorical logic) sometimes give rise to MSO theories. I will try to convey how natural this construction is from the perspective of categorical logic, using two dual notions close to my heart: hyperdoctrines and polyadic spaces. The end goal will be to formulate the following question, to which I do not know the answer: What are the models of the MSO theory associated to a monad?
(Additional teaser!) The theories arising in this way are not just theories: they can be used to transform theories, hence the name “polyadic transformers”.
Disclaimer: The connection with categorical logic was not in the 2023 paper, and I have not yet written anything on this subject.