Proof of Lindenbaum lemma without deduction theorem

Question

I'm working on a formalization of Lindenbaum's completeness lemma for modal logic systems, but I've been stuck in a property. Namely, when trying to prove that:

$$\forall\Gamma,\forall\phi,\enspace\Gamma\ \textit{is consistent} \implies (\Gamma,\phi)\ \textit{is consistent}\ \lor\ (\Gamma,\neg\phi)\ \textit{is consistent}$$

Following some books, e.g., Blackburn's and Popkorn's, this seems to boil down to a lemma:

$$(\Gamma\vdash\phi)\iff (\Gamma,\neg\phi)\ \textit{is not consistent}$$

However, when trying to prove the only if side by contraposition, I get that, assuming:

1. $(\Gamma\vdash\phi)\implies\bot$
2. $\Gamma\ \textit{is consistent}$ (derivable from 1)
3. $\Gamma,\neg\phi \vdash \psi$
4. $\Gamma,\neg\phi \vdash \neg\psi$

...should derive a contradiction. I can see how to do that if I assume a deduction theorem, thus I can, from 3 and 4, derive both $\Gamma\vdash\neg\phi\rightarrow\psi$ and $\Gamma\vdash\neg\phi\rightarrow\neg\psi$, from which we derive that $\Gamma\vdash\phi$, which is a contradiction, as expected. However, I cannot see how to do this without the deduction theorem, which may not be available in the modal logic system. I'm not sure if I'm missing something, as I've seem this property even left as an exercise to the reader in a book (sorry, I forgot which one).

So, my questions: (1) can this be proved without using the deduction theorem? (2) If so, how? (3) If not so, does this mean that Lindenbaum's lemma actually depends on the deduction theorem?

Answer 1

You need classical logic for this. Presumably the following rules for negation are valid in your logic:

1. Elimination rule: if $\Delta \vdash \psi$ and $\Delta \vdash \neg\psi$ then $\Delta \vdash \bot$.
2. Introduction rule: if $\Delta, \phi \vdash \bot$ then $\Delta \vdash \neg\phi$.
3. Classical logic: if $\Delta, \neg\phi \vdash \bot$ then $\Delta \vdash \phi$.

We say that $\Delta$ is inconsistent if $\Delta \vdash \bot$.

Let us prove that $\Gamma \vdash \phi$ if, and only if $\Gamma, \neg\phi \vdash \bot$:

• Assume $\Gamma \vdash \phi$. Then $\Gamma, \neg\phi \vdash \phi$ by weakening, and $\Gamma, \neg\phi \vdash \neg\phi$ by the hypothesis rule, therefore $\Gamma, \neg\phi \vdash \bot$ by the first rule above.

• Assume $\Gamma, \neg\phi \vdash \bot$. Then $\Gamma \vdash \phi$ by the third rule above.

If the above rules of negation are not valid in your logic, or if the definition of inconsistency is not the one I am using, then please specify the necessary information.