Return to Answer

Let me explain that argument that I had in mind.

The claim is that if a potentialist system has arbitrarily large finite families of independent unpushed buttons at every world, then it's modal validities (in the language with the buttons) is contained within S4.2.

Your example system does not satisfy the hypothesis, since at the top world all buttons are pushed. And indeed, your statement Top is not even provable in S5, let alone S4.2.

To prove the claim, the main idea is that we don't really need full switches in the main button+switch result that Benedikt Löwe and I proved in our modal logic of forcing paper; rather, it suffices for the switches to be usable a sufficient finite number of times. Consider therefore a weakening of the switch concept, which is a switch that can be flipped a certain number of times.

Specifically, we define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches. When $k=0$, we say that 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. Thus, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

Now, following the usual button+switch proof, if a statement $\varphi$ is not in S4.2, then it fails in a Kripke model $M$ whose frame is a finite pre-Boolean algebra. We can use the buttons and weak switches to label the nodes in this Kripke model, just as before. Every world $w$ in $M$ get assigned a Boolean combination $\Phi_w$ of the buttons and switches, in such a way that pushing a button means moving to a higher cluster, and changing switches only means moving within the cluster. Every propositional variable $p$ is translated to $\psi_p$, the disjunction of $\Phi_w$ for which $p$ is true at $w$ in $M$.

Now, we prove by induction on modal propositional assertions $\varphi$ of depth at most $k$, that if the buttons and switches are $k$-independent at $W$ in the potentialist system $P$, then $$W\models_P\varphi(\psi_{p_0},\ldots,\psi_{p_n})\iff w\models_M\varphi(p_0,\ldots,p_n),$$ where $w$ is the world in $M$ for which $W\models\Phi_w$. The point is that the induction step requires you to use up only one life. This shows that we don't need full switches, but only $k$-independent switches.

The proof is completed by observing that if you have sufficiently many unpushed buttons, you can form these $k$-independent families. Fix any $k$, and suppose that we have a very large family of independent buttons available. Form them into disjoint groups of size $k$, and for each group, let the corresponding weak switch $s$ be the parity count of the number of them that are pushed in that group. And then take as many additional of the buttons as you want.

The point is that you can change the parity count of the button groups simply by pushing one more button in that group. So if button groups have size $k$, you will achieve $k$-independence.

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.

The claim is that if a potentialist system has arbitrarily large finite families of independent unpushed buttons at every world, then it's modal validities (in the language with the buttons) is contained within S4.2.

Your example system does not satisfy the hypothesis, since at the top world all buttons are pushed. And indeed, your statement Top is not even provable in S5, let alone S4.2.

To prove the claim, the main idea is that we don't really need full switches in the main button+switch result that Benedikt Löwe and I proved in our modal logic of forcing paper; rather, it suffices for the switches to be usable a sufficient finite number of times. Consider therefore a weakening of the switch concept, which is a switch that can be flipped a certain number of times.

Specifically, we define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches. When $k=0$, we say that 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. Thus, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

Now, following the usual button+switch proof, if a statement $\varphi$ is not in S4.2, then it fails in a Kripke model $M$ whose frame is a finite pre-Boolean algebra. We can use the buttons and weak switches to label the nodes in this Kripke model, just as before. Every world $w$ in $M$ get assigned a Boolean combination $\Phi_w$ of the buttons and switches, in such a way that pushing a button means moving to a higher cluster, and changing switches only means moving within the cluster. Every propositional variable $p$ is translated to $\psi_p$, the disjunction of $\Phi_w$ for which $p$ is true at $w$ in $M$.

Now, we prove by induction on modal propositional assertions $\varphi$ of depth at most $k$, that if the buttons and switches are $k$-independent at $W$ in the potentialist system $P$, then $$W\models_P\varphi(\psi_{p_0},\ldots,\psi_{p_n})\iff w\models_M\varphi(p_0,\ldots,p_n),$$ where $w$ is the world in $M$ for which $W\models\Phi_w$. The point is that the induction step requires you to use up only one life. This shows that we don't need full switches, but only $k$-independent switches.

The proof is completed by observing that if you have sufficiently many unpushed buttons, you can form these $k$-independent families. Fix any $k$, and suppose that we have a very large family of independent buttons available. Form them into disjoint groups of size $k$, and for each group, let the corresponding weak switch $s$ be the parity count of the number of them that are pushed in that group. And then take as many additional of the buttons as you want.

The point is that you can change the parity count of the button groups simply by pushing one more button in that group. So if button groups have size $k$, you will achieve $k$-independence.

Let me explain that argument that I had in mind.

The claim is that if a potentialist system has arbitrarily large finite families of independent unpushed buttons at every world, then it's modal validities (in the language with the buttons) is contained within S4.2.

Your example system does not satisfy the hypothesis, since at the top world all buttons are pushed. And indeed, your statement Top is not even provable in S5, let alone S4.2.

To prove the claim, the main idea is that we don't really need full switches in the main button+switch result that Benedikt Löwe and I proved in our modal logic of forcing paper; rather, it suffices for the switches to be usable a sufficient finite number of times. Consider therefore a weakening of the switch concept, which is a switch that can be flipped a certain number of times.

Specifically, we define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches. When $k=0$, we say that 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. Thus, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

Now, following the usual button+switch proof, if a statement $\varphi$ is not in S4.2, then it fails in a Kripke model $M$ whose frame is a finite pre-Boolean algebra. We can use the buttons and weak switches to label the nodes in this Kripke model, just as before. Every world $w$ in $M$ get assigned a Boolean combination $\Phi_w$ of the buttons and switches, in such a way that pushing a button means moving to a higher cluster, and changing switches only means moving within the cluster. Every propositional variable $p$ is translated to $\psi_p$, the disjunction of $\Phi_w$ for which $p$ is true at $w$ in $M$.

Now, we prove by induction on modal propositional assertions $\varphi$ of depth at most $k$, that if the buttons and switches are $k$-independent at $W$ in the potentialist system $P$, then $$W\models_P\varphi(\psi_{p_0},\ldots,\psi_{p_n})\iff w\models_M\varphi(p_0,\ldots,p_n),$$ where $w$ is the world in $M$ for which $W\models\Phi_w$. The point is that the induction step requires you to use up only one life. This shows that we don't need full switches, but only $k$-independent switches.

The proof is completed by observing that if you have sufficiently many unpushed buttons, you can form these $k$-independent families. Fix any $k$, and suppose that we have a very large family of independent buttons available. Form them into disjoint groups of size $k$, and for each group, let the corresponding weak switch $s$ be the parity count of the number of them that are pushed in that group. And then take as many additional of the buttons as you want.

The point is that you can change the parity count of the button groups simply by pushing one more button in that group. So if button groups have size $k$, you will achieve $k$-independence.

The claim is that if a potentialist system has arbitrarily large finite families of independent unpushed buttons at every world, then it's modal validities (in the language with the buttons) is contained within S4.2.

Your example system does not satisfy the hypothesis, since at the top world all buttons are pushed. And indeed, your statement Top is not even provable in S5, let alone S4.2.

To prove the claim, the main idea is that we don't really need full switches in the main button+switch result that Benedikt Löwe and I proved in our modal logic of forcing paper; rather, it suffices for the switches to be usable a sufficient finite number of times. Consider therefore a weakening of the switch concept, which is a switch that can be flipped a certain number of times.

Specifically, we define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches. When $k=0$, we say that 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. Thus, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

Now, following the usual button+switch proof, if a statement $\varphi$ is not in S4.2, then it fails in a Kripke model $M$ whose frame is a finite pre-Boolean algebra. We can use the buttons and weak switches to label the nodes in this Kripke model, just as before. Every world $w$ in $M$ get assigned a Boolean combination $\Phi_w$ of the buttons and switches, in such a way that pushing a button means moving to a higher cluster, and changing switches only means moving within the cluster. Every propositional variable $p$ is translated to $\psi_p$, the disjunction of $\Phi_w$ for which $p$ is true at $w$ in $M$.

Now, we prove by induction on modal propositional assertions $\varphi$ of depth at most $k$, that if the buttons and switches are $k$-independent at $W$ in the potentialist system $P$, then $$W\models_P\varphi(\psi_{p_0},\ldots,\psi_{p_n})\iff w\models_M\varphi(p_0,\ldots,p_n).$$ The point is that the induction step requires you to use up only one life. This shows that we don't need full switches, but only $k$-independent switches.

The proof is completed by observing that if you have sufficiently many unpushed buttons, you can form these $k$-independent families. Fix any $k$, and suppose that we have a very large family of independent buttons available. Form them into disjoint groups of size $k$, and for each group, let the corresponding weak switch $s$ be the parity count of the number of them that are pushed in that group. And then take as many additional of the buttons as you want.

The point is that you can change the parity count of the button groups simply by pushing one more button in that group. So if button groups have size $k$, you will achieve $k$-independence.

The claim is that if a potentialist system has arbitrarily large finite families of independent unpushed buttons at every world, then it's modal validities (in the language with the buttons) is contained within S4.2.

Your example system does not satisfy the hypothesis, since at the top world all buttons are pushed. And indeed, your statement Top is not even provable in S5, let alone S4.2.

To prove the claim, the main idea is that we don't really need full switches in the main button+switch result that Benedikt Löwe and I proved in our modal logic of forcing paper; rather, it suffices for the switches to be usable a sufficient finite number of times. Consider therefore a weakening of the switch concept, which is a switch that can be flipped a certain number of times.

Specifically, we define recursively a notion of $k$-independence for a family of buttons $b_j$ and statements $s_i$ to be used as weak switches. When $k=0$, we say that 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. Thus, a family is $k$-independent at a world, when you can operate the controls as you like $k$ times.

Now, following the usual button+switch proof, if a statement $\varphi$ is not in S4.2, then it fails in a Kripke model $M$ whose frame is a finite pre-Boolean algebra. We can use the buttons and weak switches to label the nodes in this Kripke model, just as before. Every world $w$ in $M$ get assigned a Boolean combination $\Phi_w$ of the buttons and switches, in such a way that pushing a button means moving to a higher cluster, and changing switches only means moving within the cluster. Every propositional variable $p$ is translated to $\psi_p$, the disjunction of $\Phi_w$ for which $p$ is true at $w$ in $M$.

Now, we prove by induction on modal propositional assertions $\varphi$ of depth at most $k$, that if the buttons and switches are $k$-independent at $W$ in the potentialist system $P$, then $$W\models_P\varphi(\psi_{p_0},\ldots,\psi_{p_n})\iff w\models_M\varphi(p_0,\ldots,p_n),$$ where $w$ is the world in $M$ for which $W\models\Phi_w$. The point is that the induction step requires you to use up only one life. This shows that we don't need full switches, but only $k$-independent switches.

The proof is completed by observing that if you have sufficiently many unpushed buttons, you can form these $k$-independent families. Fix any $k$, and suppose that we have a very large family of independent buttons available. Form them into disjoint groups of size $k$, and for each group, let the corresponding weak switch $s$ be the parity count of the number of them that are pushed in that group. And then take as many additional of the buttons as you want.

The point is that you can change the parity count of the button groups simply by pushing one more button in that group. So if button groups have size $k$, you will achieve $k$-independence.