Prove $\vdash \neg(\square F\land p)$ in $KD$

89 Views Asked by At

How to prove that $\vdash \neg(\square F\land p)$ in $KD$? The allowed rules are natural deduction rules and the axiom $\square p\to\diamond p$ where $\diamond p=\neg\square\neg p$.

I actually don't have any ideas except that I have to assume $\square F\land p$ and deduce $F$ by using any propositional tautology, any known inference rule, or the Necessitation Rule, or the Distribution Axiom (https://en.wikipedia.org/wiki/Modal_logic#Axiomatic_systems). The Necessitation rule looks totally irrelevant here. So the only "modal" tool is the distribution axiom, but I can't see how it can be applied.

1

There are 1 best solutions below

1
On BEST ANSWER

How about the following. (I will write $\bot$ instead of $F$).

$\top$ is a theorem, and hence $\square \top$ is a theorem by the necessitation. Next, from $\square \top \rightarrow \lozenge \top$ (which is an instance of the axiom) by MP we have that $\lozenge \top$ is a theorem. As $\lozenge \top$ is a theorem, then $\neg p \vee \lozenge \top$ is a theorem as well. Using the duality between box and diamond, and $\top$ and $\bot$, the latter is equivalent to $\neg p \vee \neg \square \bot$. Finally, by the DeMorgan rule, we obtain $\neg (p \wedge \square\bot)$.