I want to find out the correspondences for the following two formulas or whether they are already derivable in the modal logic $KD4.2$, i.e. whether the formulas are valid in serial, transitive and directed frames.


1:
$(\lozenge (\lozenge p\wedge\Box(p\rightarrow q)) \wedge \Box(\lozenge p\rightarrow\lozenge(p\wedge q)))\rightarrow(\lozenge(\lozenge p\wedge\Box(p\rightarrow(\lozenge(\lozenge p\wedge\Box(p\rightarrow q)) \wedge \Box(\lozenge p\rightarrow\lozenge(p\wedge q))))) \wedge \Box(\lozenge p\rightarrow\lozenge(p\wedge (\lozenge(\lozenge p\wedge\Box(p\rightarrow q)) \wedge \Box(\lozenge p\rightarrow\lozenge(p\wedge q))))))$


2:
$(\lozenge (\lozenge p\wedge\Box(p\rightarrow q)) \vee \Box(\lozenge p\rightarrow\lozenge(p\wedge q)))\rightarrow(\lozenge(\lozenge p\wedge\Box(p\rightarrow(\lozenge(\lozenge p\wedge\Box(p\rightarrow q)) \vee \Box(\lozenge p\rightarrow\lozenge(p\wedge q))))) \wedge \Box(\lozenge p\rightarrow\lozenge(p\wedge (\lozenge(\lozenge p\wedge\Box(p\rightarrow q)) \vee \Box(\lozenge p\rightarrow\lozenge(p\wedge q))))))$


Unfortunately [SQEMA](http://www.fmi.uni-sofia.bg/fmi/logic/sqema/sqema.jsp) failed on these. Perhaps some have access to better computer resources or perhaps some may derive these in $KD4.2$?



A question on two modal formulas
I do have some of my own code that I was able to modify to investigate this.


Short answer
------------


* (1) is not a theorem of $\mathbf{KD4.2}$ since it is invalid on the frame
$F=(W,R)$ where $W=\{A,B,C\}$ and $R=\{(A,A),(B,A),(B,B),(B,C),(C,A)\}$,
and $F$ is serial, transitive and convergent.
* (2) is a theorem of $\mathbf{K4}$, hence it is valid on all transitive frames.
However, since it was substantially weakened from a $\mathbf{K4}$ equivalent axiom,
it is valid on some non-transitive frames too.


Details
-------


I use an algebraic-style notation which is intended to shorten the formulas,
reduce parentheses and also input formulas quickly into the computer.
Precedence is as follows:


* 1. 'L' and 'M' for necessity and possibility
* 2. '!' for negation
* 3. '.' for conjunction (but typically omitted)
* 4. '+' for disjunction
* 5. '->' and '<->'


Note that in both your formulas (1) and (2) the right-hand of the outermost implication
is a conjunction, so we can split them into:



```
(1a)  M( MpL(p->q) ) L( Mp->M(pq) ) -> M( MpL( p -> M( MpL(p->q) )+L( Mp->M(pq) ) ) )
(1b)  M( MpL(p->q) ) L( Mp->M(pq) ) -> L( Mp -> M( pM( MpL(p->q) )L( Mp->M(pq) ) ) )

(2a)  M( MpL(p->q) ) L( Mp->M(pq) ) -> M( MpL( p -> M( MpL(p->q) )+L( Mp->M(pq) ) ) )
(2b)  M( MpL(p->q) ) L( Mp->M(pq) ) -> L( Mp -> M( p( M( MpL(p->q) )+L( Mp->M(pq) ) ) ) )

```

Hopefully I did not make translation mistakes. Then we have the following:



> 
> Formula (1a)
> 
> 
> 



```
Testing formula "M(MpL(p->q))L(Mp->M(pq))->M(MpL(p->M(MpL(p->q))L(Mp->M(pq))))"
on frame {A(A)B(ABC)C(A)}

Valuation {p(C)q(C)} => formula invalid at B

                                                  Sub-formula | A B C
--------------------------------------------------------------|------
                                                            p | 0 0 1
                                                            q | 0 0 1
                                                           Mp | 0 1 0
                                                       (p->q) | 1 1 1
                                                      L(p->q) | 1 1 1
                                                    MpL(p->q) | 0 1 0
                                                 M(MpL(p->q)) | 0 1 0
                                                           pq | 0 0 1
                                                        M(pq) | 0 1 0
                                                  (Mp->M(pq)) | 1 1 1
                                                 L(Mp->M(pq)) | 1 1 1
                                     M(MpL(p->q))L(Mp->M(pq)) | 0 1 0  left hand
                                (p->M(MpL(p->q))L(Mp->M(pq))) | 1 1 0
                               L(p->M(MpL(p->q))L(Mp->M(pq))) | 1 0 1
                             MpL(p->M(MpL(p->q))L(Mp->M(pq))) | 0 0 0
                          M(MpL(p->M(MpL(p->q))L(Mp->M(pq)))) | 0 0 0  right hand
M(MpL(p->q))L(Mp->M(pq))->M(MpL(p->M(MpL(p->q))L(Mp->M(pq)))) | 1 0 1  1a

```


> 
> Formula (1b)
> 
> 
> 



```
Testing formula "M(MpL(p->q))L(Mp->M(pq))->L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))"
on frame {A(A)B(ABC)C(A)}

Valuation {p(C)q(C)} => formula invalid at B

                                                  Sub-formula | A B C
--------------------------------------------------------------|------
                                                            p | 0 0 1
                                                            q | 0 0 1
                                                           Mp | 0 1 0
                                                       (p->q) | 1 1 1
                                                      L(p->q) | 1 1 1
                                                    MpL(p->q) | 0 1 0
                                                 M(MpL(p->q)) | 0 1 0
                                                           pq | 0 0 1
                                                        M(pq) | 0 1 0
                                                  (Mp->M(pq)) | 1 1 1
                                                 L(Mp->M(pq)) | 1 1 1
                                     M(MpL(p->q))L(Mp->M(pq)) | 0 1 0  left hand
                                    pM(MpL(p->q))L(Mp->M(pq)) | 0 0 0
                                 M(pM(MpL(p->q))L(Mp->M(pq))) | 0 0 0
                           (Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1
                          L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1  right hand
M(MpL(p->q))L(Mp->M(pq))->L(Mp->M(pM(MpL(p->q))L(Mp->M(pq)))) | 1 0 1  1b

```


> 
> Formula (2a)
> 
> 
> 



```
( 1)    p -> (Lq->pLq)                                  PC
( 2)    Mp -> M(Lq->pLq)                                (1) + M-monotony
( 3)    Mp -> (LLq->M(pLq))                             (2) + M-addition + PC
( 4)    MpLLq -> M(pLq)                                 (3) + PC
( 5)    Lq -> LLq                                       Axiom 4
( 6)    MpLq -> MpLLq                                   (5) + PC
( 7)    MpLq  ->  M(pLq)                                (4),(6) + MP 

( 8)    Lq -> Mp+Lq                                     PC
( 9)    LLq -> L(Mp+Lq)                                 (8) + L-monotony
(10)    Lq -> L(Mp+Lq)                                  (5),(9) + MP
(11)    pLq -> pL(Mp+Lq)                                (10) + PC
(12)    M(pLq) -> M( pL(Mp+Lq) )                        (11) + M-monotony
(13)    MpLq -> M( pL(Mp+Lq) )                          (7),(12) + MP

(14)    MpLr -> M( pL(Mp+Lr) )                          (13) + US q/r
(15)    M(qs)Lr -> M( qsL(M(qs)+Lr) )                   (14) + US p/qs
(16)    qsL(M(qs)+Lr) -> sL(M(qs)+Lr)                   PC
(17)    M( qsL(M(qs)+Lr) ) -> M( sL(M(qs)+Lr) )         (16) + M-monotony
(18)    M(qs)Lr -> M( sL(M(qs)+Lr) )                    (15),(17) + MP

(19)    M(qs)+Lr -> ( p->M(qs)+Lr )                     PC
(20)    L( M(qs)+Lr ) -> L( p->M(qs)+Lr )               (19) + L-monotony
(21)    sL( M(qs)+Lr ) -> sL( p->M(qs)+Lr )             (20) + PC
(22)    M( sL( M(qs)+Lr ) ) -> M( sL( p->M(qs)+Lr ) )   (21) + M-monotony
(23)    M(qs)Lr -> M( sL( p->M(qs)+Lr ) )               (18),(22) + MP

(24)    M(qMp)Lr -> M( MpL( p->M(qMp)+Lr ) )            (23) + US s/Mp

(25)    2a                         from (24) + US q/L(p->q), r/Mp->M(pq)

```


> 
> Formula (2b)
> 
> 
> 



```
(26)    Lq -> ( Mp->M(pLq) )                            (7) + PC
(27)    LLq -> L( Mp->M(pLq) )                          (26) + L-monotony
(28)    Lq -> L( Mp->M(pLq) )                           (5),(27) + MP
(29)    Lr -> L( Mp->M(pLr) )                           (28) + US q/r

(30)    ( Mp->M(pLr) ) -> ( Mp->M(ps)+M(pLr) )          PC
(31)    ( Mp->M(pLr) ) -> ( Mp->M( p(s+Lr) ) )          (30) + M-addition
(32)    L( Mp->M(pLr) ) -> L( Mp->M( p(s+Lr) ) )        (31) + L-monotony
(33)    Lr -> L( Mp->M( p(s+Lr) ) )                     (29),(32) + MP
(34)    sLr -> L( Mp->M( p(s+Lr) ) )                    (33) + PC

(35)    2b                         from 34 + US s/M(MpL(p->q)), r/Mp->M(pq)

```

In fact, by eliminating step 34 above we obtain a stronger formula:



```
(2b')  L( Mp->M(pq) ) -> L( Mp->M( p( M( MpL(p->q) )+L( Mp->M(pq) ) ) ) )

```

And you can try to prove the following using similar methods:



```
(2a')  M( MpL(p->q) ) -> M( MpL( p->M( MpL(p->q) )+L( Mp->M(pq) ) ) )

```

Please doublecheck all this. At some point my program was absolutely correct,
but I hacked into it many times since.


