Is there a modal logic axiom corresponding to the condition that for every world w there is some world v such that vRw? (Reverse Seriality)

Question

Seriality on certain modal frames - that for every world w there is some world v such that wRv - corresponds to the axiom: $\square$P$\rightarrow$$\diamondsuit$P, assuming a standard interpretation of the relevant operators.

Consider what we might call the reverse seriality: that for every world w there is some world v such that vRw. Is there an axiom to which reverse seriality corresponds, assuming a standard interpretation of the operators?

I've observed any frame satisfying reflexivity, i.e. every w is such that wRw which corresponds to the axiom: $\square$P $\rightarrow$P, satisfies reverse seriality, but that's as far as I've thought it through.

Answer 1

Expanding on the other answer, there is no such formula in the standard semantics.

Indeed, consider the following two models (here every world will be a $p$ world, where $p$ is the only atomic proposition):

• $\mathfrak{M}_1$ with exactly one world $w_1$ and the empty relation.

• $\mathfrak{M}_2$ with two worlds $x$ and $w_2$, such that $x$ sees $w_2$.

There is a bisimulation linking $w_1$ and $w_2$, so they satisfy the same modal formulas. But if there were a formula that expressed $\exists v . v R w$, then $w_2$ would satisfy it while $w_1$ wouldn't! Thus no such formula exists.

If you really want to express this formula, you need to pass to a richer language. As the other answerer has said, the standard way to do this is by adding symbols that express moving backwards along relations. Often in this context we write $\overset{\rightarrow}{\square}$ and $\overset{\rightarrow}{\lozenge}$ instead of $\square$ and $\lozenge$. We also add symbols $\overset{\leftarrow}{\square}$ and $\overset{\leftarrow}{\lozenge}$ to represent moving backwards along the relation. That is:

$$w \models \overset{\rightarrow}{\square} \varphi \iff \forall v . wRv \to v \models \varphi$$

$$w \models \overset{\leftarrow}{\square} \varphi \iff \forall v . vRw \to v \models \varphi$$

It turns out the following axioms (plus Necessisitation for $\overset{\rightarrow}{\square}$ and $\overset{\leftarrow}{\square}$ and Modus Ponens) are sound and complete wrt the class of all frames with the above semantics:

• All classical tautologies

• $\overset{\rightarrow}{\square}(\varphi \to \psi) \to \overset{\rightarrow}{\square} \varphi \to \overset{\rightarrow}{\square} \psi$

• $\overset{\leftarrow}{\square}(\varphi \to \psi) \to \overset{\leftarrow}{\square} \varphi \to \overset{\leftarrow}{\square} \psi$

• $\varphi \to \overset{\rightarrow}{\square} \overset{\leftarrow}{\lozenge} \varphi$

• $\varphi \to \overset{\leftarrow}{\square} \overset{\rightarrow}{\lozenge} \varphi$

In this system, "reverse seriality" can be expressed as $\overset{\leftarrow}{\square}\varphi \to \overset{\leftarrow}{\lozenge}\varphi$.

---

I hope this helps ^_^

Answer 2

Since there is no other answer, I'd like to give a preliminary, possibly incomplete answer.

I am quite sure that you would need two modal operators to axiomatize the reverse seriality, as we need to talk about the 'forward' direction of the accessibility relation $R$ and its 'backward' direction $R^{-1}$.

To this end, I propose a temporal interpretation of the modal operators: Let

• $[X]\phi$ stand for "next, it will be necessary that $\phi$ holds",
• $\langle X\rangle \phi$ stand for "next, it will be possible that $\phi$ holds",
• $[P]\phi$ stand for "before, it was necessary that $\phi$ holds", and
• $\langle P \rangle \phi$ stand for "before, it was possible that $\phi$ holds.

Now, we can provide the following axiomatization $$ \begin{align} \text{for any tautology $\phi$ infer }&\vdash \phi\\ \text{from } \vdash \phi \to \psi \text{ and } \vdash \phi \text{ infer } &\vdash \psi \tag{mp}\\ \text{from } \vdash \phi \text{ infer } &\vdash [X]\phi \tag{Nec$_X$}\\ \text{from } \vdash \phi \text{ infer } &\vdash [P]\phi \tag{Nec$_P$}\\ &\vdash [X](\phi \to \psi) \to [X]\phi \to [X]\psi \tag{K$_X$}\\ &\vdash [P](\phi \to \psi) \to [P]\phi \to [P]\psi \tag{K$_P$}\\ &\vdash \phi \to [P]\langle X \rangle \phi \tag{C1}\\ &\vdash \phi \to \langle P \rangle \langle X \rangle \phi\tag{C2} \end{align} $$ That is, $X$ and $P$ are modal operators, as for both the necessitation rule $\text{Nec}$ and the axiom $\text{K}$ hold. The cancellation axiom $\text{C1}$ says that whenever $\phi$ holds, then before it was necessary that next $\phi$ will be possible. The second cancellation axiom $\text{C2}$ says that whenever $\phi$ holds, then before it was possible that next $\phi$ will be possible.

On the semantic side we have the equivalences

• $\omega\models [X]\phi$ if and only if for all $\omega'$ with $\omega R \omega'$ it holds $\omega'\models \phi$ and
• $\omega\models [P]\phi$ if and only if for all $\omega'$ with $\omega S \omega'$ it holds $\omega'\models \phi$
• (and corresponding versions for the duals $\langle X \rangle$ and $\langle P \rangle$)

It is easy to show that for any Kripke structure where $S$ is the inverse $R^{-1}$ the axiom $\text{C1}$ holds. Moreover, if $R$ is 'reverse serial', then also $\text{C2}$ has to hold.

I conjecture that this axiomatization is also complete for the class of Kripke structures with $S=R^{-1}$ and $R$ being 'reverse serial'.

I suspect that more elaborated analyses and also completeness results of 'reverse seriality' can be found in the literature on branching time modal logics with (infinite) past.