Modal model theory

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 \text{Mod}(T) be the class of all models of some first-order theory T in some language L. 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 \Diamond \varphi is true at a model M, if there is a larger model N in which \varphi holds, and \Box \varphi is true at M, if \varphi holds in all larger models. Write \Diamond(L) for the language L closed under the modal operators and Boolean connectives, and L^\Diamond 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 \Diamond(L). 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 M_i be a family of models indexed by the set I and suppose we have a finitely-additive \{0,1\}-measure \mu on I. The ultraproduct \prod_\mu M_i is the set of equivalence classes of \prod M_i/\mu, the Cartesian product \prod M_i modulo \mu. If M_i = M for all i \in I, then we call this ultraproduct the ultrapower. Classic Łoś’s theorem, informally, says that a first-order formula is true in almost every model M_i if and only if it is true in the ultraproduct \prod_\mu M_i. Our result generalizes the ultrapower case of Łoś’s theorem to formulas in the modal language \Diamond(L). We also know that the theorem does not generalize for arbitrary ultraproducts, and for formulas in the expanded language L^\Diamond (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.

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!

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.

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.

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s