Soundness of temporal modal logic rule

40 Views Asked by At

I am trying to prove the soundness of a temporal modal logic with this rule:

$$ \dfrac{\Sigma \vdash \Theta}{\bigcirc \Sigma \vdash \bigcirc \Theta} $$

The semantics given a $\omega$-word $u : \mathbb{N} \rightarrow 2^{\mathcal{P}}$ and an enviroment $\rho : \mathcal{V} \rightarrow 2^{\mathcal{N}}$ are:

$$ \parallel \bigcirc \varphi \parallel_{\rho}^u = \{n \in \mathbb{N} \;|\; n+1 \in \parallel \varphi \parallel_{\rho}^u \} $$

I believe the correct notion of soundness should be:

Assuming $\forall u. [(\forall \rho \; i. i \in \parallel \Sigma \parallel_{\rho}^u) \implies (\forall \rho \; i. i \in \parallel \Theta \parallel_{\rho}^u)]$ then $\forall u. [(\forall \rho \; i. i \in \parallel \bigcirc \Sigma \parallel_{\rho}^u) \implies (\forall \rho \; i. i \in \parallel \bigcirc \Theta \parallel_{\rho}^u)]$

Is this the correct notion of soundness?