4
$\begingroup$

Let $\textit{C}$ be the modal logical schema $(\square (\square \alpha \rightarrow \alpha) \wedge \square (\square \lnot\alpha \rightarrow \lnot \alpha))\rightarrow (\square \alpha \vee \square \lnot \alpha)$.

I believe we can establish that $\textit{C}$ corresponds to the second order condition that the accessibility relation $\textit{R}$ is ancestrally directed in the following sense: If $xRy_0$ and $xRz_0$ and if $Y$ and $Z$ are the set of possible worlds seen by $y_0$ and $z_0$, respectively, in a finite number of steps, then $Y\cap Z$ is nonempty.

Let $K$, $D$ and $4$ be as usual where $D$ corresponds with the seriality and $4$ with the transitivity of the accessibility relation. The schema $.2$ is $\lozenge \square \alpha \rightarrow \square \lozenge \alpha$ which correponds with the directedness of the accessibility relation.

Questions: How (if at all) is .2 derivable in KD4C? How (if at all) is C derivable in KD4.2?

$\endgroup$
8
  • $\begingroup$ It seems like $C$ derivable in S4, isn't it? But there are transitive, reflexive relations that aren't ancestrally directed, which violates the correspondence you mentioned. Am I missing something? $\endgroup$ – Adam Bjorndahl Mar 30 '14 at 21:56
  • $\begingroup$ My question did not relate to S4, and I do not invoke reflexivity. That C is derivable in S4 does not have the consequence that it is derivable in KD4.2. Indeed, there are transitive reflexive relations which are not ancestrally directed; but that does not in any sense violate the correspondence I mentioned. $\endgroup$ – Frode Alfson Bjørdal Mar 31 '14 at 0:04
  • $\begingroup$ Oops! I think you are right. There is a typo in the schema C of the question! I will edit the schema accordingly now. Thanks! $\endgroup$ – Frode Alfson Bjørdal Mar 31 '14 at 0:17
  • $\begingroup$ I am sorry about this, but the clerical error affected my own thinking about this. Perhaps my questions will now be manageable ... $\endgroup$ – Frode Alfson Bjørdal Mar 31 '14 at 0:20
  • 1
    $\begingroup$ I am not sure I understand the conclusion to the above. Did you actually prove that they are not derivable? how? Then is the question still open? $\endgroup$ – JuneA Oct 17 '14 at 12:04
1
$\begingroup$

Your axiom .2 is $\mathrm{G1}$ from Hughes&Cresswell, so I will use this name. They (and also Wikipedia) call the corresponding frames convergent (another name for directed). Also, I am going to rewrite axiom $\mathrm{C}$ as $(\Diamond p \land \Box(\Box p \rightarrow p) \land \Box(p \rightarrow \Diamond p)) \rightarrow \Box p$.

$\mathrm{C}$ is not derivable in $\mathbf{KD4G1}$.

If it were, then it would also be derivable in $\mathbf{S4.2}$, which extends $\mathbf{KD4G1}$. But $\mathrm{C}$ plus $\mathbf{S4.2}$ reflexivity immediately implies $\Diamond p \rightarrow \Box p$, then $p \rightarrow \Box p$, therefore $p \leftrightarrow \Box p$ and $\mathbf{S4.2}$ would collapse to $\mathbf{Triv}$, which is known not to be the case.

Note that the frame condition you give for C is incorrect, since it implies seriality when $y_0=z_0=y$, while C is valid on the non-serial frame $F=(\{x,y\},\{(x,y)\})$. Assume we fix this by weakening the definition of ancestral convergence to $y_0\not=z_0$. Then we still get only a necessary, but not sufficient, condition for a C-frame. Indeed, the frame $F'=(\{x,y,z\},\{(x,y),(x,z),(y,y),(y,z),(z,z)\})$ is serial, transitive and convergent, therefore ancestrally convergent, yet $\mathrm{C}$ fails to validate at $x$ for valuation $V(p)=\{y\}$. And $F'$ validates $\mathrm{G1}$, which is another proof that $\mathrm{C}$ is not derivable in $\mathbf{KD4G1}$.

$\mathrm{G1}$ is derivable in $\mathbf{KD4C}$.

Here is an outline of the proof:

a) In $\mathbf{KD4}$, derive $(\Box p \land \Box\Box p) \leftrightarrow \Box p$ and $\Box p \rightarrow \Box\Diamond p$ and $\Box\Diamond p \rightarrow \Diamond p$ and $\Box p \rightarrow \Diamond\Box p$ and $\Diamond (p \land \Box p) \leftrightarrow \Diamond\Box p$, all quite straightforward.

b) Substitute $p\land\Box p/p$ in $\mathrm{C}$, then use all a) and simplify it to $(\Diamond\Box p \land \Box(\Box p \rightarrow p)) \rightarrow \Box p$.

c) Substitute $\Diamond p/p$ in the result of b), then apply 3-rd a) and simplify it to $\Diamond\Box\Diamond p \rightarrow \Box\Diamond p$.

d) Apply $\Diamond$-monotony to 2-nd a) and derive $\Diamond\Box p \rightarrow \Diamond\Box\Diamond p$.

e) $\mathrm{G1}$, i.e. $\Diamond\Box p \rightarrow \Box\Diamond p$, follows from c) and d).

$\endgroup$
5
  • $\begingroup$ Your claim that C plus S4.2 implies $\diamond p\to\square p$ appears false. $\endgroup$ – Frode Alfson Bjørdal Nov 3 '14 at 15:28
  • 2
    $\begingroup$ Even KT + C implies $\Diamond p\to\Box p$, as it makes the premise of $C$ automatically true. $\endgroup$ – Emil Jeřábek Nov 3 '14 at 15:31
  • $\begingroup$ Concerning the stated condition for ancestral connectedness, I add that I had assumed seriality as part of the constraints at work when isolating that condition. $\endgroup$ – Frode Alfson Bjørdal Nov 3 '14 at 15:32
  • $\begingroup$ Ah, I see it now. Sorry! :) $\endgroup$ – Frode Alfson Bjørdal Nov 3 '14 at 15:33
  • $\begingroup$ @JuneA I just got around to check your proof today. It is correct. Thanks! $\endgroup$ – Frode Alfson Bjørdal Jan 22 '15 at 20:07

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.