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:

- 'L' and 'M' for necessity and possibility

- '!' for negation

- '.' for conjunction (but typically omitted)

- '+' for disjunction

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

allworlds $w'$ which are better"), so that, for example, $\lozenge(p\land q)$ is equivalent to $(\lozenge p)\land(\lozenge q)$. Do you use the usual definition of $\Box$ as $\neg\lozenge\neg$, so that it would mean "holds atat least oneworld which is better"? I would expect hat this inversion of the usual roles of $\lozenge$ and $\Box$ would prevent any close connection between your modal logic and the traditional ones. $\endgroup$ – Andreas Blass Jul 18 '15 at 17:073more comments