Are buttons really enough to bound validities by S4.2?

Question

Joel Hamkins recently claimed on twitter that buttons suffice to bound the validities of a potentialist system to the modal logic S4.2 (see here), and that switches are not necessary. We have been trying to reproduce this result here in Amsterdam, and encountered a few problems, so we decided to seek help here.

For the sake of this post, let me stick to the standard terminology and notation used in this field (see, for example, these slides of Joel Hamkins). Our aim is to prove the following claim.

Claim. If a potentialist system has infinitely many independent buttons, then its modal validities are contained in the modal logic S4.2.

Let me now describe two problems we encountered while trying to reprove this claim, and related questions.

1. A possible counterexample? Consider the potentialist system on $P = (\mathcal{P}(\mathbb{N}),\subseteq)$ in the language of propositional logic: every world in $P$ is a structure for propositional logic (i.e. this is just a Kripke model for modal propositional logic). We define the valuations of these worlds as follows for every $x \in \mathcal{P}(\mathbb{N})$: $x \vDash p_i$ if and only if $i \in x$. It is now easy to verify that $\{ p_i | i \in \mathbb{N} \}$ constitutes a collection of infinitely many independent buttons.

Consider now the so-called $\mathsf{Top}$-Axiom, i.e. $$ \Diamond((\Box p \leftrightarrow p) \wedge(\Box \neg p \leftrightarrow \neg p)). $$ This axiom is not a consequence of $\mathsf{S4.2}$ (it fails on every $\mathsf{S4.2}$-frame whose top cluster contains at least two different elements), but it is easy to verify that it holds in the potentialist system $P$ defined above (exactly because it has a unique maximal point $\mathbb{N}$ in which all buttons are pushed).

Question. This counterexample shows that the Claim needs some additional assumptions, possibly on the language or the kind of structures we're dealing with. What are these additional assumptions? What is the exact statement that we can prove?

2. A possible proof? Let me now explain how we think the Claim should be proved, and which problems we encounter here. Of course, this will only be a sketch.

Let $P$ be a potentialist system with infinitely many buttons. Given a modal formula $\phi$ such that $\mathsf{S4.2} \not \vdash \phi$, we can find a Kripke model $(K,R,V)$ of $\mathsf{S4.2}$ and a node $v \in K$ such that $(K,R,V), v \not \vdash \phi$. The idea is to unfold the model $K$ for $n$ steps, where $n$ is the modal depth of the formula $\phi$. This yields a finite tree Kripke model $T = (T,R_T,V_T)$ whose root node is $n$-bisimilar to the node $v$ of the original model $K$. By $n$-bisimilarity, it follows that $T, v \not \Vdash \phi$. We can now use the infinitely many buttons to find a labelling that imitates the behaviour of the tree in the potentialist system.

As the original model $K$ is transitive, it follows that the resulting model $T$ cannot possibly transitive and it cannot possibly be reflexive as otherwise, the notion of $n$-bisimilarity is just usual bisimilarity. In particular, the relation $R_T$ of the tree $T$ connects a node of the tree only to its direct successor, and to no other nodes.

Moreover, if the resulting trees $T$ were transitive and reflexive, the above would show that $\mathsf{S4.2}$ is complete with respect to the finite trees, but that is not the case. In particular, the Kripke model $T$ does not satisfy $\mathsf{S4.2}$ anymore.

If we want to continue the proof from the non-reflexive and non-transitive tree $T$, we have to find a labelling of the potentialist system $P$ that imitates the non-reflexive and non-transitive tree $T$. It does not seem that this can be done with usual buttons: At any world $v$ of the potentialist system corresponding now to a node $t$ of the tree $T$, we can press several buttons at once and reach a world $w$ that corresponds to a node $t_1$ of $T$ that is not an immediate successor of the node $t$ we started with, a contradiction. This suggests that the standard way of labelling worlds of the potentialist system does not seem to work.

Question. Given a non-reflexive and non-transitive tree $T$ and a potentialist system $P$ with infinitely many buttons, can we find a labelling of the worlds of $P$ using the buttons to imitate the modal behaviour of $T$ in the potentialist system?

Related is the following:

Question. The above argument could also suggest that the notion of $n$-bisimilarity does not work for this situation. How can this proof be salvaged?

In some sense, we could simplify the question and just ask:

Question. How can we prove (a possibly strengthened version of) the Claim?

I am very curious about this result, and hope that someone here can clarify these questions.

Answer 1

Unfortunately, the argument I had had in mind seems broken to me now, and I retract the claim. I wonder what of it can be salvaged?

Let me explain what I had had in mind. The main idea was this: it seems we don't need to flip the switches infinitely often, but rather only finitely many times for any given formula, based on the modal depth of the formula.

And so I wanted to mimic that by weakening the notion of independence to $k$-independence. Specifically, define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches, as follows: for $k=0$, every such family is $0$-independent at every world; the family is $(k+1)$-independent at a world, if you can operate the buttons and switches to achieve a new configuration (pushing any desired additional buttons and setting the switches as desired) by moving to a world where the family remains at least $k$-independent. Basically, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

The observation was that if one has a lot of independent buttons, then you can easily make $k$-independent families of buttons and switches. Simply form disjoint groups of $k$ buttons, and for each group, let the corresponding assertion $s$ be the parity count of the number of them that are pushed.

With such a family, you can flip the parity count by pushing one button, and so this family will be $k$-independent at the original world.

My idea then was to adapt the usual button+switch proof, by folding in a $k$-independent requirement: the simulation lemma would work for formulas of depth $k$, provided the family remained $k$-independent.

But that part seems broken to me now. I had thought at first one could rule out your counterexample by insisting that every node has independent unpushed buttons. This does in fact rule our your example, but it doesn't seem actually to enable the simulation lemma to go through. If the weak switches are not actually switches, then they could be possibly necessary in the potentialist system, and this will not necessarily be simulated in the Kripke model.

Answer 2

We now know that the existence of arbitrarily many independent buttons suffices to bound the validities by Grz.2. It is one of the results from my forthcoming work—Modal theory of the category of sets—that I am going to present next week in Singapore. Slides from the talk will be available on my website www.woloszyn.org. One can also find a brief discussion of the result among the slides from the talk that I gave for the Oxford Junior Logic Seminar, also available on my website.

Let me describe the details briefly. A Kripke category is a concrete category of structures in a common first-order language $\mathcal L$. Each object in the category is an $\mathcal L$-structure, and each morphism is an $\mathcal L$-homomorphisms. We define modal semantics in the Kripkean manner. Namely, $W \models \lozenge \varphi[\nu]$ if there is a morphism $f \colon W \to U$ such that $U \models \varphi[f \circ \nu]$. In particular, every potentialist system is a Kripke category.

Theorem. A world that admits arbitrarily many independent buttons has its propositional modal validities contained within the propositional modal theory Grz.2.

Proof sketch. It is known that Grz.2 is characterized by finite partial orders. But with the method of partial tree unraveling (see proof of lemma 6.5 in The model logic of forcing), one can show that finite lattices or finite Boolean algebras suffice. That new characterization enables one to provide a standard frame labeling argument. We proceed precisely like in the case of S4.2, but this time we are labeling a Boolean algebra as opposed to a pre-Boolean algebra, hence buttons suffice.

This observation extends to other cases with no switches. Validities are bounded by Grz if there is a cluster-less railyard labeling, and Grz.3 is valid if there is an arbitrarily long ratchet.

Finally, let me give you an example of a world in a Kripke category whose validities are precisely Grz.2. It is any infinite world in the Kripke category of sets and surjective functions $\mathbf{Surj}$ in the language of pure equality with parameters allowed. For the upper-bounds, we take infinitely many pairs of distinct individuals $(u_i,v_i)$ and buttons $b[u_i,v_i]$ saying $u_i=v_i$. This is a button because we can always collapse a chosen pair of distinct individuals to a single individual by following an appropriate surjective mapping. For the lower bounds, we need to show that Grz.2 holds. Modal theory S4.2 is valid, because we can complete any span in the category to a commuting square. What is left is to show that Grz is valid. I like to think of Grz by the means of a notion of penultimacy.

Definition. An assertion $\varphi$ is penultimate at world $W$ just in case $W \models \neg \varphi \land \lozenge \varphi \land \square(\varphi \to \square \varphi)$.

Theorem. Assume S4.2 is valid. Then, Grz is valid at $W$ just in case for each assertion $\varphi$ in the language of substitutions, either $\varphi$ or its negation is necessary or possibly penultimate, on the cone above $W$.

Thus, to prove that any infinite world $W$ in $\mathbf{Surj}$ validates Grz, it suffices to find a penultimate world for each assertion $\varphi$ or its negation. By modality elimination (see page 10 in Modal model theory), one can show that all infinite worlds have the same modal truths. If $\varphi$ or its negation is true at $W$, then we are done. Otherwise, there must be an accessible finite world of the smallest finite non-zero size that is wrong about the ultimate truth-value of $\varphi$. And that world witnesses the possibility of penultimacy of $\varphi$ or $\neg \varphi$ at $W$.