I'm reading van Bentham's Modal Logic for Open Minds (section 5.7), where he proves the (weak) completeness of K. I'm trying to work out each step, but I seem to need to use an intuitionistically invalid inference, which I'm not sure if necessary for this proof. I'm also not sure how to extend the same proof to prove strong completeness.
Consider this part of the proof:
Consistency: A set $\Sigma$ of formulas is consistent iff for no finite conjunction $\Psi$ of formulas in Σ, the negation $\lnot\Psi$ is derivable.
Lemma: If $\nvdash\phi$ then $\{\lnot\phi\}$ is consistent.
If $\nvdash\phi$ then $\nvdash\lnot\lnot\phi$, since $\vdash\lnot\lnot\phi\rightarrow\phi$. But this is intuitionistically invalid. Is there anyway around this?
Even though all the theorems of classical propositional logic are true here (in K), but I would like to know if there is a way to avoid this so that the exact same proof would go through for an intuitionistic propositional modal logic.In trying to extend the same proof to strong completeness (which the author implies we can), I need to prove that if $\Sigma\cup\{\lnot\phi\}$ is inconsistent then $\Sigma\vdash\phi$ (To use the contrapositive). But I only know how to do this via the same method as (1):
If $\Sigma\cup\{\lnot\phi\}$ is inconsistent then $\Sigma,\lnot\phi\vdash\Psi$ where $\vdash\lnot\Psi$ for some $\Psi$ whose subformulas are in $\Sigma\cup\{\phi\}$. So $\Sigma \vdash \lnot\phi\rightarrow\Psi$, and we only get that $\Sigma\vdash\phi$ since $\Sigma\vdash\lnot\lnot\phi$.
Links:
Click here for van Bentham's proof (section 5.7, page 54):
Click here for my notes on his proof (I've made some reasoning more explicit).