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?

  • $\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$ Mar 30, 2014 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$
    – FAB
    Mar 31, 2014 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$
    – FAB
    Mar 31, 2014 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$
    – FAB
    Mar 31, 2014 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, 2014 at 12:04

1 Answer 1


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).

  • $\begingroup$ Your claim that C plus S4.2 implies $\diamond p\to\square p$ appears false. $\endgroup$
    – FAB
    Nov 3, 2014 at 15:28
  • 2
    $\begingroup$ Even KT + C implies $\Diamond p\to\Box p$, as it makes the premise of $C$ automatically true. $\endgroup$ Nov 3, 2014 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$
    – FAB
    Nov 3, 2014 at 15:32
  • $\begingroup$ Ah, I see it now. Sorry! :) $\endgroup$
    – FAB
    Nov 3, 2014 at 15:33
  • $\begingroup$ @JuneA I just got around to check your proof today. It is correct. Thanks! $\endgroup$
    – FAB
    Jan 22, 2015 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.