Consistency Lemma in Lindenbaum's Theorem

Let $\Lambda$ be a modal logic, we say that a formula $\varphi$ is $\Lambda$-inconsistent if $\vdash_\Lambda (\neg \varphi)$ and is consistent otherwise. Similarly we say that a set of modal formulas $\Gamma$ is $\Lambda$-consistant if, for all finite subset $\{\varphi_1 \dots \varphi_n \} \subseteq \Gamma$, the formula $\varphi_1 \wedge \dots \wedge \varphi_n$ is $\Lambda$-consistent in the sense above. To proove the Lindenbaum's Theorem is needed this Lemma:

Let $\Lambda$ be a modal logic, $\varphi$ a modal formula and $\Gamma$ a consistent set. Then or $\Gamma \cup \{\varphi\}$ either $\Gamma \cup \{\neg \varphi\}$ is $\Lambda$-consistent.

Proof. Suppose both the sets are $\Lambda$ incosistent, then there are formulas $\psi_1 \dots \psi_n,\psi'_1 \dots \psi'_n$ such that $\psi_1 \wedge \dots \wedge \psi_n\wedge \varphi$ and $\psi'_1 \wedge \dots \wedge \psi'_n\wedge\neg \varphi$ are $\Lambda$-incosistent. Then by definition

\begin{gather} \vdash_\Lambda \neg(\psi_1 \wedge \dots \wedge \psi_n\wedge \varphi) \label{one} \\ \vdash_\Lambda \neg(\psi'_1 \wedge \dots \wedge \psi'_n\wedge\neg \varphi) \end{gather} $(*)$ take now $\vdash_\Lambda \neg (a\wedge b) \to(\neg(a'\wedge\neg b)\to \neg(a\wedge a'))$

Then by uniform substitution $a=\psi_1 \wedge \dots \wedge \psi_n$, $a'=\psi_1 \wedge \dots \wedge \psi_n$ and $b=\varphi$, and by modus ponens on $(*)$ we get \begin{gather} \vdash_\Lambda \neg( \psi_1 \wedge \dots \wedge \psi_n\wedge \psi'_1 \wedge \dots \wedge \psi'_n ) \end{gather} against the consistency of $\Gamma$.

My question: I don't undestan why we can proceed with passage $(*)$. It is not clear, a priori, why the modal logic $\Lambda$ should contain that formula (necessary condition for applying the modus ponens). Are we allowed to enlarge the set modal logic $\Lambda$ as we want?

• The formula is a tautology. – Mauro ALLEGRANZA May 30 '16 at 6:06
• Ok, I tried to arrange that formula before, but I didn't realize. – Lorban May 30 '16 at 13:13
• Even now, without truth table, I can't see that algebraically. Nevertheless thank you for your answer. – Lorban May 30 '16 at 13:15
• It is not easy to "see it" without t-t. But you have to consider only the cases when the antecedent of (+) is true, that is when either $a$ or $b$ are false. If $a$ is false, then $\lnot (a \land a')$ is true, and thus also the consequent of (+) is true, so Ok. Finally, when $a,b$ are false we have to compute it, to check that it is again true. – Mauro ALLEGRANZA May 30 '16 at 13:23