*This blog post from August 2019 now includes an update with regard to a result that is now revoked. Research has its ups and downs…*

I would like to share with you a brief description of what I have been doing at Oxford for the past eight months. Since my adviser has already written about our work on his Twitter and blog multiple times, I have decided to embed several tweets pertaining to our project and comment on them.

Let be the class of all models of some first-order theory in some language . One may view this as a Kripke model of possible worlds, where each model accesses the larger models, of which it is a submodel. So is true at a model , if there is a larger model in which holds, and is true at , if holds in all larger models. Write for the language closed under the modal operators and Boolean connectives, and for the language that is also closed under quantification.

The following is a surprising result of elementarily equivalence generalizing to theories in the modal language . The proof utilizes a modal version of Łoś’s theorem, or sometimes called the ultraproduct theorem, and the Keisler-Shelah theorem. The setup is as follows. Let be a family of models indexed by the set and suppose we have a finitely-additive -measure on . The ultraproduct is the set of equivalence classes of , the Cartesian product modulo . If for all , then we call this ultraproduct the ultrapower. Classic Łoś’s theorem, informally, says that a first-order formula is true in almost every model if and only if it is true in the ultraproduct . Our result generalizes the ultrapower case of Łoś’s theorem to formulas in the modal language . We also know that the theorem does not generalize for arbitrary ultraproducts, and for formulas in the expanded language (essential counterexamples and details can be found on Professor Hamkins’s blog). The second part of the argument is an application of the Keisler-Shelah theorem, which says that elementarily equivalent structures have isomorphic ultrapowers.

Introducing modal model theory, where we extend the usual model theory in mathematical logic to include the modal operators, where ◊p means that p is true in some larger model and □p means that p is true in all larger models. https://t.co/voH9XbQutf

— Joel David Hamkins (@JDHamkins) July 6, 2019

A few days after the foregoing tweet was published, David Eppstein, Chancellor’s Professor of Computer Science at the University of California, Irvine, posted fascinating writing on modal model theory in the case of graphs. In particular, Professor Eppstein proves that finiteness is expressible in the modal language of graphs; this cannot be done in the first-order logic of graph theory!

David Eppstein on the modal model theory of graphs. Finiteness is expressible in the modal language of graphs. https://t.co/oFt0TX0doX

— Joel David Hamkins (@JDHamkins) July 14, 2019

David Eppstein, Chancellor's Professor of Computer Science at the University of California, Irvine, writes about modal model theory of graphs – the topic Professor Hamkins and I recently introduced. https://t.co/ZFlQmjggjC

— Wojciech Aleksander Wołoszyn (@WAWoloszyn) July 14, 2019

To move through the multiverse of possible worlds, we use a number of funny tools like buttons, switches, ratchets, and so on. These devices can tell us a lot about the modal nature of our currently inhabited universe or even about the entire multiverse. In particular, they allow us to discern a modal theory by which our modal validities are bounded. A tweet below depicts visualizations of three popular modal theories.

Here is an improved, more suggestive diagram. (Unfortunately, I'm spending too much time with tikz…) pic.twitter.com/S51cFW3xAY

— Joel David Hamkins (@JDHamkins) January 11, 2018

UPDATE: The following was unfortunately revoked. See this mathoverflow answer.

~~An important toolbox is an arbitrarily large family independent of buttons and switches. It is a widely used theorem that modal validities being bounded by S4.2 follow from the existence of such a toolbox. However, sometimes, for example, in the case of models of all groups, it is curiously hard to find independent switches. The great news is that we have managed to prove that switches are redundant and it is enough to find an arbitrarily large family of independent buttons! You can read more about the tools for studying modal validities in this article.~~

Unfortunately, the proof seems now to me to be broken. Alas…

— Joel David Hamkins (@JDHamkins) September 4, 2019

We have many further results revolving around the modal model theory, the details of which I shall share soon.