To pose my question, I first must first quickly define a language, a model, semantics for such models, and a logical system called S4O.

Consider a language $L$ with a set $PV$ of propositional variables, Boolean connectives $\neg$ and $\vee$(with the other boolean connectives as shorthands for these), the necessity modality $\Box$, and a "next" modality O.

Define a model to be a triple $\langle X,f,V \rangle$ where $X$ is a topological space, $f$ is a continuous function on $X$, and $V: PV \rightarrow \mathcal{P}(X)$. For $A$ and $B$ wffs of $L$ and $p \in PV$, define:

$M(p) = V(p)\\ M(A \vee B) = M(A) \cup M(B)\\ M(\neg B) = X - M(B)\\ M(\Box B) = \textit{Int}(M(B))\\ M(\text{O}B) = f^{-1}(B)\\ $ where $\textit{Int}$ denotes topological interior. Suppose $\langle X,f,V \rangle$ is a model. We can define semantics as follows:

$ M \models B \text{ iff } M(B) = X \\ \langle X,f,V \rangle \models B \text{ iff } M \models B \text{ for every model M} \\ X \models B \text{ iff } \langle X,f,V \rangle \models B \text{ for every continuous function } f. \\ \models B \text{ iff } X \models B \text{ for every topological space } X. $

The system S4O in the language $L$ is given by the following axioms:

$ \text{the classical tautologies} \\ \text{S4 axioms for } \Box \\ (\text{O}(A \vee B) \leftrightarrow (\text{O}A \vee \text{O}B)) \\ (\text{O} \neg A \leftrightarrow \neg \text{O} A) \\ (\text{O} \Box A \leftrightarrow \Box \text{O} A) \\ $ and the inference rules of modus ponens, and necessitation for both O and $\Box$.

I can finally pose my question. Suppose S4O proves the formula $(A \rightarrow B)$ for some special $A, B$. Suppose we've proven soundness. Then $\models (A \rightarrow B)$. In particular, for any model $M$, $M \models (A \rightarrow B)$. If we suppose $M \models A$, does it follow that $M \models B$?

  • $\begingroup$ What do you mean by "more general cases" here? I think giving your specific situation probably will help. $\endgroup$ – Doug Spoonwood Jul 15 '13 at 3:23

Since your semantics agrees with ordinary classical logic on the Boolean connectives, modus ponens will work just as it does classically. In detail, looking at the last two lines of your question, you have $M\vDash(A\to B)$ and $M\vDash A$. Since $\to$ is defined as usual from $\neg$ and $\lor$, the former means $M\vDash((\neg A)\lor B)$. According to your definitions, this means $(X-M(A))\cup M(B)=X$. But since $M\vDash A$, you also have $M(A)=X$, so $X-M(A)=\varnothing$ and therefore $(X-M(A))\cup M(B)=M(B)$. So $M(B)=X$, which means $M\vDash B$.

  • 1
    $\begingroup$ Note that the modality $\square$ and the temporal operator $O$ have no influence on this situation. $\endgroup$ – Andreas Blass Jul 15 '13 at 4:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.