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 theClaimneeds 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) theClaim?

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