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](https://twitter.com/JDHamkins/status/1126869905217867776)), 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](http://jdh.hamkins.org/wp-content/uploads/2017/12/Potentialism-Tutorial-Winter-School-Hejnice-2018.pdf)). 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.



Are buttons really enough to bound validities by S4.2?
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.


