On directedness, transitivity and ancestral directedness

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?

• 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? – Adam Bjorndahl Mar 30 '14 at 21:56
• 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. – Frode Alfson Bjørdal Mar 31 '14 at 0:04
• 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! – Frode Alfson Bjørdal Mar 31 '14 at 0:17
• 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? – JuneA Oct 17 '14 at 12:04

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

• Your claim that C plus S4.2 implies $\diamond p\to\square p$ appears false. – Frode Alfson Bjørdal Nov 3 '14 at 15:28
• Even KT + C implies $\Diamond p\to\Box p$, as it makes the premise of $C$ automatically true. – Emil Jeřábek Nov 3 '14 at 15:31
• 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. – Frode Alfson Bjørdal Nov 3 '14 at 15:32
• Ah, I see it now. Sorry! :) – Frode Alfson Bjørdal Nov 3 '14 at 15:33
• @JuneA I just got around to check your proof today. It is correct. Thanks! – Frode Alfson Bjørdal Jan 22 '15 at 20:07