Proof in KTB (modal logic) using KTB and propositional logic

Question

I am trying to prove that $\neg \lozenge p$ from $\square (p \rightarrow q)$ and $\lozenge \square \neg q$ using only the axioms in KTB and propositional logic. I can prove using tableux, but not synthetically. Can you help me? Thank you.

UPDATE: Actually, you need B and 4 in order to make this proof. But you can prove in KTB from the premise $\square (p \rightarrow \square q)$.

Answer 1

This formula is invalid in KTB. To see this take three worlds 0,1,2 s.t. $P$ holds at 1, $\Box \neg Q$ holds at 2, but there is no way for 2 to access 1 without transitivity. This is a full counter-model:

Worlds: {0,1,2}

@: 0

P: {1}

Q: {1}

R: {(0,1),(0,2),(0,0),(1,1),(2,2),(1,0),(2,0)}

Answer 2

Restating, we want to show: $$\Bigg[\bigg[\square(p\to q)\bigg]\wedge \bigg[\Diamond\square \neg q\bigg]\Bigg]\vdash_{\Lambda} \bigg[\neg \Diamond p\bigg].$$

Where deduction is in $\Lambda := \langle KTB\cup PL\rangle$

$(K)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }\square(p\to q)\to (\square p \to \square q)$

$(T)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }p\to \Diamond p$

$(B)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }p\to \square \Diamond p$

$(Dual)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }\Diamond p \leftrightarrow \neg \square \neg p$

$(Modus\_Ponens)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }[(\varphi\in \Lambda)\wedge (\varphi\to \psi\in \Lambda)]\implies (\psi \in \Lambda)$

$(Uniform\_Substitution)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }(\varphi \in \Lambda)\implies (\varphi[..subs..]\in \Lambda)$

$(Generalization)$: $\text{ }\text{ }\text{ }\text{ }\text{ }\text{ }(\varphi\in \Lambda) \implies (\square \varphi\in \Lambda)$

---

---

$\underline{\text{Proof:}}$

$0:\text{ }\square(p\to q)\text{ }\text{ }\text{ }$ (Hyp)

$1:\text{ }\Diamond\square \neg q\text{ }\text{ }\text{ }$ (Hyp)

---

$2:\text{ }\square(\neg q \to \neg p)\text{ }\text{ }\text{ }(\text{Contrapositive (0)})$

$3:\text{ }\square(\neg q \to \neg p) \to \big(\square \neg q \to \square \neg p\big)\text{ }\text{ }\text{ }(\text{Unif. Sub (2) into (K))}$

$4:\text{ }\square \neg q \to \square \neg p\text{ }\text{ }\text{ }(M.P.(2,3))$

---

$5-6:\text{ }\neg \square \Diamond q \to \neg q\text{ }\text{ }\text{ }(\text{Contrapositive of (B) with Sub.})$

$7:\text{ }\neg \square \Diamond q\text{ }\text{ }\text{ }(\text{Dual of (1)})$

$8:\text{ }\neg q\text{ }\text{ }\text{ }(\text{M.P.(7,6)})$

$9: \text{ }\square \neg q\text{ }\text{ }\text{ }(\text{Generalize (8)})$

$10:\text{ }\square \neg p\text{ }\text{ }\text{ }(\text{M.P.(9,4)})$

$11:\neg \Diamond p\text{ }\text{ }\text{ }(\text{Dual of (10)})\text{ } \blacksquare$


My reference is Modal Logic by Blackburn et al. (Ch.4, ~pg.190)