0
$\begingroup$

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 failed on these. Perhaps some have access to better computer resources or perhaps some may derive these in $KD4.2$?

Improve this question
$\endgroup$
8
  • $\begingroup$ Could you say anything about these formulas which might be helpful? In what context did they occur to you, what are they supposed to express in any semantics? $\endgroup$ Commented Jul 18, 2015 at 9:08
  • $\begingroup$ $\lozenge p$ is supposed to hold in a world $w$ iff $p$ holds in all worlds $w'$ which are $\textit{better}$ than $w$. I use the induced preferential logic $KD4.2$ to interpret other deontic notions, and formulas 1 and 2 are supposed to play a role in a possible interpretation of $\textit{dyadic deontic S5}$. $\endgroup$ Commented Jul 18, 2015 at 13:07
  • 1
    $\begingroup$ I"m somewhat surprised by your comment saying that you use $\lozenge$ for what appears to be a necessity operator ("all worlds $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 at at least one world 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$ Commented Jul 18, 2015 at 17:07
  • $\begingroup$ Sorry, that was a typographical error! I should have written "holds in $\textit{a}$ world w' which is better than w". I will edit now and use $\Box$ instead of $\lozenge$. I presuppose the usual interdefinability relations between $\Box$ and $\lozenge$ and the logic $KD4.2$ I invoke is normal. $\endgroup$ Commented Jul 18, 2015 at 19:03
  • 1
    $\begingroup$ One of your comments is sufficiently readable in my browser to address my concern; the $\lozenge$ at the beginning of your first comment was intended to be $\Box$, and then the semantics makes much better sense. The only remaining problem is that the formulas in the question are far too complicated for me to assimilate and say anything about. I hope some experts in modal logic will be able to grasp them and provide useful information. $\endgroup$ Commented Jul 18, 2015 at 20:38

1 Answer 1

Reset to default
2
$\begingroup$

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
    1. '!' for negation
    1. '.' for conjunction (but typically omitted)
    1. '+' for disjunction
    1. '->' 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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.