0

I need to prove $\Diamond p \rightarrow \lnot\Diamond\lnot\Diamond p$ in B axiomatic, which contains next conversion rules:
1.$(p\land q)\rightarrow(q\land p)$
2.$(q\land p)\rightarrow p$
3.$p\rightarrow(p\land p)$
4.$p\land(q\land r)\rightarrow(p\land q)\land r$
5.$p\rightarrow \lnot(\lnot p)$
6.$(p\land q)\land(q\land r)\rightarrow(p\land r)$
7.$(p\land(p\rightarrow q))\rightarrow q$
8.$\Diamond(p\land q)\rightarrow\Diamond p$
9.$p\rightarrow p$
10.$\Box p\rightarrow\Box\Box p$
11.$p\rightarrow\lnot\Diamond\lnot\Diamond p$
12.$p\rightarrow q\equiv \not\Diamond(p\land \lnot q) $

Git Gud
  • 31,356
romtsn
  • 125
  • Is your rule 12 really the only rule you have for "$\equiv$"? – hmakholm left over Monica Dec 24 '13 at 14:33
  • Also are you sure all of the rules are copied correctly? For example, rule 6 would look a lot less random if it said $\neg(p\land q)\land\neg(\neg q\land r)\to\neg(p\land r)$ instead. – hmakholm left over Monica Dec 24 '13 at 14:42
  • Yes, rule 6 is copied correctly. Also, we should prove equivalents from our rules, if we need. In modal logic we can: 1.Substitute variables to formulas 2. Substitute equivalent formulas 3. If A and B is seted, then A $\land$ B seted (the formula is one of rules) – romtsn Dec 24 '13 at 14:56
  • I was going to show this using the method of analytic tableaux, my favourite tool, but I'm not familiar with "B axiomatic"; there are similar systems in this brilliant book though. – Shaun Dec 24 '13 at 15:09
  • Is it taken for granted that $\square$ is an abbreviation for $\neg\lozenge\neg$ (or that $\lozenge$ is an abbreviation for $\neg\square\neg$) ? Or are $\lozenge$ and $\square$ independent modal operators? – Andreas Blass Dec 24 '13 at 16:02
  • Yes it is. That operators are not independent. – romtsn Dec 24 '13 at 16:27
  • I am wondering about rule 12 (which is equal to (P -> Q) <-> [](~P v Q) ), this is not a normal classical implication, and is also not a theorem in standard minimal normal modal logic(modal logic K) are you sure about this rule? – Willemien Feb 22 '14 at 16:04

0 Answers0