This post concerns Problem 8.13 in Holliday (2025), which asks, roughly, whether the argument of §2.5 of that paper can be extended to what he calls Humberstone frames. The answer is yes, as I’ll show here.
This is a blog post, not a paper, so I won’t repeat any definitions that are already in Holliday’s paper, or for that matter in Humberstone (1981). The only thing I will note is that I’m following Humberstone, and not Holliday, in using \(x \leq y\) to mean that \(y\) is a refinement of \(x\). Relatedly, \(x \geq y\) just means \(y \leq x\).
The frame we’ll use consists of (a) all finite binary strings, plus (b) a ‘code’ for each binary string. When \(y\) is a code, I’ll write \([y]\) for the string that \(y\) is the code of, and when \(x\) is a string, I’ll write \(c(x)\) for the code for \(x\). The refinement relation \(x \leq y\) holds in one of two cases:
- \(x=y\)
- \(x\) and \(y\) are strings, and \(x\) is an initial segment of \(y\).
That is, strings are refined by adding to them, and codes have no non-trivial refinements. We then introduce a bunch of accessibility relations: \(R_i\), which determine modal operators \(\Box_i\), and hence by definition \(\diamond_i\).
- Universal \(R_\forall\)
- \(xR_{\forall}y\) whenever \(x\) and \(y\) are points in the model.
- String-to-code \(R_{\rightarrow}\)
- \(xR_{\rightarrow}y\) iff \(x\) is a string, \(y\) is a code, and one of \(x\) and \([y]\) is an initial segment of the other. I’m imagining the strings on the left, and the codes on the right, hence the left-to-right arrow.
- Code-to-string \(R_{\leftarrow}\)
- \(xR_{\leftarrow}y\) iff \(x\) is a code, \(y\) is a string, and \([x]\) is an initial segment of \(y\). Note this is not the same definition as for \(R_{\rightarrow}\), since here we insist on which is the initial segment.
- Code-zero-remove: \(R_{-}\)
- \(xR_{-}y\) iff \(x\) and \(y\) are codes, and \([x]\) ends with a 0, and \([y]\) is \([x]\) minus that trailing 0.
- Code-shortening: \(R_{\subsetneq}\)
- \(xR_{\subsetneq}y\) iff \(x\) and \(y\) are distinct codes, and \([y]\) is an initial segment of \([x]\)
Call the following proposition \(\alpha\)
\[ \diamond_{-}(\Box_{\leftarrow} p \wedge \neg \diamond_{\subsetneq}\Box_{\leftarrow} p) \]
Let’s build up where this will be true. (Note that I’m following Holliday’s own construction really closely here.)
- \(\Box_{\leftarrow} p\) is true at the code \(x\) iff \(p\) is true at \([x]\).
- So \(\diamond_{\subsetneq}\Box_{\leftarrow} p\) is true at \(x\) if \(p\) is true at some proper initial segment of \([x]\).
- So \(\neg \diamond_{\subsetneq}\Box_{\leftarrow} p\) is true at \(x\) if \(p\) is not true at any proper initial segment of \([x]\).
- So \(\Box_{\leftarrow} p \wedge \neg \diamond_{\subsetneq}\Box_{\leftarrow} p\) is true at \(x\) if \(p\) is true at \([x]\), but not at any shortening of \([x]\). That is, if you were working down the tree of strings, \([x]\) is the first point you’d get to where \(p\) is true. Call a string like this an initial point for \(p\).
- So \(\diamond_{-}(\Box_{\leftarrow} p \wedge \neg \diamond_{\subsetneq}\Box_{\leftarrow} p)\) is true at the code \(x\) if \([x]\) is \(y\frown \langle0\rangle\), where \(y\) is an initial point for \(p\).
Now consider any initial point \(x\) for \(p\). Since \(p\) is persistent, \(p\) will be true at \(x\frown \langle0\rangle\), call this \(x_0\), and at \(x\frown \langle1\rangle\), call this \(x_1\). Since, as we just showed, \(\alpha\) is true at \(c(x_0)\), and \(x_0R_{\rightarrow}c(x_0)\), it follows that \(\diamond_{\rightarrow} \alpha\) is true at \(x_0\). But \(\diamond_{\rightarrow} \alpha\) will not be true at \(x_1\), or at any of its refinements. At \(c(x_1)\), \(\alpha\) fails because this is not the code for a sequence ending in 0. And at the code for any shortening or extension of \(x_1\), \(\alpha\) fails because that’s not the code of a string one element longer than an initial point for \(p\).
That means that if \(p\) is true at some string, it is true at some initial point, and hence both \(p \wedge \diamond_{\rightarrow} \alpha\) and \(p \wedge \neg \diamond_{\rightarrow} \alpha\). If \(\diamond_{\forall}(p \wedge \diamond_{\rightarrow} \top)\) is true (anywhere), then \(p\) is true at some string. (It can’t be that \(p\) is simply true at codes, because \(\diamond_{\rightarrow} \top\) is not true at any code.) So \(\diamond_{\forall}(p \wedge \diamond_{\rightarrow} \alpha)\) and \(\diamond_{\forall}(p \wedge \neg \diamond_{\rightarrow} \alpha)\) will both be true everywhere. Hence at all points, we’ll have this instance of (Split):
\[ \diamond_{\forall}(p \wedge \diamond_{\rightarrow} \top) \rightarrow [\diamond_{\forall}(p \wedge \diamond_{\rightarrow} \alpha) \wedge \diamond_{\forall}(p \wedge \neg \diamond_{\rightarrow} \alpha)] \tag{1}\]
It just remains to show that all the \(R\)-relations satisfy all the conditions for Humberstone-frames. This is trivial for \(R_\forall\), because it always holds, and for \(R_{\subsetneq}\) and \(R_{-}\) because they just relate points that don’t stand in any non-trivial refinement relations. The only questions are for \(R_{\rightarrow}\) and \(R_{\leftarrow}\). Let’s go through the three-conditions on Humberstone-frames, using Holliday’s names for them.
First upR, i.e., \(x \leq x^{\prime} \wedge x^{\prime}Ry \rightarrow xRy\). This can’t fail for \(R_{\leftarrow}\), because the left-hand side has no non-trivial coarsenings. For \(R_{\rightarrow}\), \(x^{\prime}R_{\rightarrow}y\) means either \(x^\prime\) is an initial segment of \([y]\), or \([y]\) is an initial segment of \(x^\prime\). If the former, then clearly \(x\), which is an initial segment of \(x^\prime\), is also an initial segment of \([y]\), so \(xR_{\rightarrow}y\). If the latter, imagine working through all the coarsenings, i.e., shortenings, of \(x^\prime\) sequentially by starting with \(x^\prime\) and removing one element at a time. At first we’ll have sequences that are, like \(x^\prime\), extensions of \([y]\), then we’ll get to \([y]\) itself, then we’ll have shortenings of \([y]\). At every stage, we’ll have something that is either an extension of \([y]\), or a shortening of it, so \(xR_{\rightarrow}y\) will hold.
Now Rdown, i.e., \(xRy \wedge y \leq y^\prime \rightarrow xRy^\prime\). In this case, this is trivial for \(R_{\rightarrow}\), since when \(xR_{\rightarrow}y\), \(y\) has no non-trivial refinements. For \(R_{\leftarrow}\), \(xR_{\leftarrow}y\) means that \(y\) is an extension of \([x]\), so any extension of \(y\) will be an extension of \([x]\), as required.
Now R-ref++, i.e., \(xRy \rightarrow \exists x^\prime \geq x \forall x^{\prime\prime} \geq x^\prime: x^{\prime\prime}Ry\). Again, this is trivial for \(R_{\leftarrow}\), since whenever \(xR_{\leftarrow}y\), \(x\) has no non-trivial refinements. The only tricky case is \(R_{\rightarrow}\). So assume \(xR_{\rightarrow}y\). Again there are two cases to consider. One is where \(x\) is an initial segment of \([y]\). In that case it we can set \(x^\prime\) to be \([y]\). The other is where \([y]\) is an initial segment of \(x\). In that case, we can just set \(x^\prime\) to be \(x\) itself. Either way, there is a witness for the consequent of R-ref++.
The result is that Equation 1 will be valid on the frame. Here we follow Holliday to complete the proof. There is no class of Kripke frames where Equation 1 is valid on the frames without \(\neg \diamond_{\forall}(p \wedge \diamond_{\rightarrow} \top)\) being valid on the frames. Quick proof: if that were not the case, so there was a frame where \(\diamond_{\forall}(p \wedge \diamond_{\rightarrow} \top)\) could be true, there would be a model on that frame where \(p\) was only true at one point, so there could not be witnesses for both \(\diamond_{\forall}(p \wedge \diamond_{\rightarrow} \alpha)\) and \(\diamond_{\forall}(p \wedge \neg \diamond_{\rightarrow} \alpha)\). So there is a class of Humberstone frames (in fact a singleton class), which determines a logic not determinable by any class of Kripke frames.