Substructural Propositional Dynamic Logics

Abstract

We prove completeness and decidability of a version of Propositional Dynamic Logic where the underlying non-modal propositional logic is a substructural logic in the vicinity of the Full Distributive Non-associative Lambek Calculus. Extensions of the result to stronger substructural logics are briefly discussed.

A Technical Appendix

Lemma 8.

• 1. For all $\varphi \in \varPhi$, $\varphi \in [\![\varSigma ]\!]^{\varPhi }$ iff $\varphi \in \underline{\varSigma }^{+}$.

• 2. If $[\alpha ]\varphi \in \varPhi$ for some $\varphi$, then $X \subseteq \alpha Y$ implies that $\vdash _{\varLambda } f(X) \rightarrow [\alpha ]f(Y)$.

Proof

Induction on subexpressions. 1. holds for $p \in At$ by definition and the inductive steps for the rest of the Boolean connectives are easy. The case for $[\alpha ]\varphi$ is more complicated. Note that we have to prove that $[\alpha ]\varphi \in \underline{\varGamma }^{+}$ iff $\underline{\varGamma } \in \alpha [\![\varphi ]\!]^{\varPhi }$. The “if” part is established using claim 2. for $\alpha$ (a subexpression of $[\alpha ]\varphi$) as follows. If $\underline{\varGamma } \in \alpha [\![\varphi ]\!]^{\varPhi }$, then $\vdash _{\varLambda } f(\underline{\varGamma }) \rightarrow [\alpha ]f([\![\varphi ]\!]^{\varPhi })$ by 2. Note that $\vdash _{\varLambda } f([\![\varphi ]\!]^{\varPhi }) \rightarrow \varphi$ by the induction hypothesis ($\varphi \in \underline{\varDelta }^{+}$ for all $\underline{\varDelta } \in [\![\varphi ]\!]^{\varPhi }$) and so $\vdash _{\varLambda } [\alpha ] f([\![\varphi ]\!]^{\varPhi }) \rightarrow [\alpha ]\varphi$ using the fact that $\varLambda$ contains MAX. Hence, $\vdash _{\varLambda } f(\underline{\varGamma }) \rightarrow [\alpha ]\varphi$. Now $[\alpha ]\varphi$ is assumed to be in $\varPhi$, so if it were the case that $[\alpha ]\varphi \notin \underline{\varGamma }^{+}$, then $\underline{\varGamma } \not \in IP_{\varLambda }$ contrary to our assumption. Hence, $[\alpha ]\varphi \in \underline{\varGamma }^{+}$. The “only if” part is established by induction on the complexity of $\alpha$ using the MAX axioms for the action operators; we skip the details.

2. Assume that $X \subseteq aY$. Take an arbitrary $\underline{\varGamma } \in X$. Suppose, for the sake of contradiction, that

$$\begin{aligned} \not \vdash _{\varLambda } f(\underline{\varGamma }) \rightarrow [a]f(Y). \end{aligned}$$

Let $Z = \{ \psi \mid [a]\psi \in \underline{\varGamma }^{+} \}$. It follows that

$$\begin{aligned} \not \vdash _{\varLambda } \bigwedge Z \rightarrow f(Y). \end{aligned}$$

Hence, by the Pair Extension Lemma, there is a non-trivial prime $\varLambda$-theory $\varDelta$ such that $Z \subseteq \varDelta$ and $f(Y) \notin \varDelta$. Now consider $\underline{\varSigma } = \langle \varDelta \cap \varPhi , \bar{\varDelta } \cap \varPhi \rangle$ (where $\bar{\varDelta }$ is the complement of $\varDelta$). Obviously $\underline{\varSigma } \in IP_{\varLambda }$ and $R^{\varPhi }(a)\underline{\varGamma \varSigma }$. Hence, by our assumption, $\underline{\varSigma } \in Y$, so

$$\begin{aligned} \vdash _{\varLambda } f(\underline{\varSigma }) \rightarrow f(Y), \end{aligned}$$

but also

$$\begin{aligned} \vdash _{\varLambda } \bigwedge Z \rightarrow f(\underline{\varSigma }) \end{aligned}$$

(by the construction of $\underline{\varSigma }$), so

$$\begin{aligned} \vdash _{\varLambda } \bigwedge Z \rightarrow f(Y), \end{aligned}$$

contrary to our assumption. Consequently, it has to be the case that $\vdash _{\varLambda } f(\underline{\varGamma }) \rightarrow [a]f(Y)$. The same argument can be repeated for all $\underline{\varGamma }_i \in X$. Hence, $\vdash _{\varLambda } f(X) \rightarrow [a]f(Y)$.

The inductive steps for concatenation and choice are easily established using the MAX axioms characterising these action operators. It is worthwhile to go through the cases for $\alpha ^{*}$ and $\varphi ?$. Assume first that $X \subseteq \alpha ^{*}Y$. Hence

$$\begin{aligned} \vdash _{\varLambda } f(X) \rightarrow f(\alpha ^{*}Y) \end{aligned}$$

It is easily seen that $\alpha ^{*}Y \subseteq \alpha (\alpha ^{*}Y)$. Hence, using induction hypothesis for $\alpha$,

$$\begin{aligned} \vdash _{\varLambda } f(\alpha ^{*}Y) \rightarrow [\alpha ] f(\alpha ^{*}Y). \end{aligned}$$

So, by the MAX rule characterizing $\alpha ^{*}$,

$$\begin{aligned} \vdash _{\varLambda } f(\alpha ^{*}Y) \rightarrow [\alpha ^{*}] f(\alpha ^{*}Y). \end{aligned}$$

Yet, we have

$$\begin{aligned} \vdash _{\varLambda } [\alpha ^{*}] f(\alpha ^{*}Y) \rightarrow [\alpha ^{*}] f(Y) \end{aligned}$$

(note that $\alpha ^{*}Y \subseteq Y$ and use the monotonicity MAX rule). Therefore,

$$\begin{aligned} \vdash _{\varLambda } f(X) \rightarrow [\alpha ^{*}] f(Y). \end{aligned}$$

The case for $\varphi ?$ is established as follows. Assume that $X \subseteq (\varphi ?)Y$. Take an arbitrary $\underline{\varGamma } \in X$ and assume, for the sake of contradiction, that

$$\begin{aligned} \not \vdash _{\varLambda } f(\underline{\varGamma }) \rightarrow [\varphi ?]f(Y). \end{aligned}$$

Hence, using the MAX rule for $\varphi ?$,

$$\begin{aligned} \not \vdash _{\varLambda } (f(\underline{\varGamma }) \wedge \varphi ) \rightarrow f(Y). \end{aligned}$$

Using the Pair Extension Lemma, there is a non-trivial prime theory $\varDelta$ containing $f(\underline{\varGamma }) \wedge \varphi$ but not containing f(Y). Now take $\underline{\varDelta } = \langle \varDelta \cap \varPhi , \bar{\varDelta } \cap \varPhi \rangle$. It is clear that $\underline{\varGamma } \le ^{\varPhi } \underline{\varDelta }$ and that $\underline{\varDelta } \in [\![\varphi ]\!]^{\varPhi }$ (by induction hypothesis 1. applied to $\varphi$, the subexpression of $\varphi ?$). By the definition of $[\![\varphi ?]\!]^{\varPhi }$, it follows that $\underline{\varGamma } [\![\varphi ?]\!]^{\varPhi } \underline{\varDelta }$ and, hence, $\underline{\varDelta } \in Y$. Consequently,

$$\begin{aligned} \vdash _{\varLambda } f(\underline{\varDelta }) \rightarrow f(Y). \end{aligned}$$

But this contradicts the observation that the prime theory $\varDelta$ does not contain f(Y). Hence, it must be the case that $\vdash _{\varLambda } (f(\underline{\varGamma }) \wedge \varphi ) \rightarrow f(Y)$. Similar reasoning can be applied to each element of X, so

$$\begin{aligned} \vdash _{\varLambda } f(X) \rightarrow [\varphi ?]f(Y). \end{aligned}$$