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

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.

• Hi! What is $F$? – Charles Bronson Mar 11 at 12:06
• @CharlesBronson It's the sentence "false". – user643175 Mar 11 at 16:09
• For what it's worth, in my experience that's more commonly denoted by "$\perp$." – Noah Schweber Mar 11 at 17:03

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)$$.
• Alternatively Assuming $\square\lnot\top\land p$, then $\square\lnot\top$ may be inferred, which by duality is equivalent to $\lnot\lozenge\top$. However $\top$ (verum, "true") is a theorem, so $\square\top$ by Necessitation, and from the axiom of Seriality, $\square\top\to\lozenge\top$, we infer $\lozenge\top$ by modus ponens. Therefore the assumption derives a contradiction, disproving it. $\vdash_{\mathrm D}\lnot(\square\lnot\top\land p)$ – Graham Kemp Mar 12 at 0:03