1
$\begingroup$

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.

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

1 Answer 1

5
$\begingroup$

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)$.

$\endgroup$
1
  • 1
    $\begingroup$ 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)$ $\endgroup$ Mar 12, 2019 at 0:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .