Tools

Definition 4.1   With a fixed sentence ${\mathit A}$ we associate a corresponding set of relevant sentences $R({\mathit A})$, or sometimes written just as R. This is the smallest set of sentences containing $\neg \mathit{A}$ which is closed under taking single negation and subformulas.

Definition 4.2   We say Prop(B) is the set of propositional variables occurring in B and define $\widetilde{M}:= \{ \Gamma \mid \Gamma \mbox{ maximal $\mathit{ILM}$ -consistent... ...l \mathrm{A} \in \Gamma , \ \ Prop( \mathrm{A}) \subset Prop( \mathcal{A}) \}.$

Definition 4.3   $\mathit{BR}(\mathcal{A})$ is defined to be the smallest set including the relevant sentences $R(\mathcal{A})$, such that if $A \rhd B \in \mathit{R}( \mathcal{A} )$ then both $\Box \neg A$ and $\Box \neg B$ are in $\mathit{BR}(\mathcal{A})$.

Definition 4.4   We define for $\Gamma , \Delta \in \widetilde{M}$
$\Gamma \prec \Delta \Leftrightarrow \forall \mathrm{A}\ ( \ \Box \mathrm{A} \i... ...s \Box \mathrm{A} \in (\Delta \setminus \Gamma ) \cap \mathit{BR}(\mathcal{A})$

Definition 4.5   We define for $\Gamma , \Delta \in \widetilde{M}$
$\Gamma \prec_{\mbox{\footnotesize {B}}} \Delta \Leftrightarrow \Gamma \prec \De... ...} \in \Gamma \mbox{ one has } \neg \mathrm{A} , \Box \neg \mathrm{A} \in \Delta$. We say that $\Delta$ is a B-critical successor of $\Gamma$.

The following three lemmas form the mathematical fundaments of the modal completeness proof of $\mathit{ILM}$.

Lemma 4.6   Let $\Gamma \in \widetilde{M}$ and $\neg ( A \rhd B ) \in \Gamma \cap R$. There exists $\Delta$ such that $\Gamma \prec_{\mbox{\footnotesize {B}}} \Delta$and $A \in \Delta$. Moreover, $\Delta$ can be chosen to be maximal w.r.t. the number of $\Box$-formula`s.

Lemma 4.7  

Let $\Gamma \in \widetilde{M}$ with $A \rhd B \in \Gamma$ and let $\Delta \in \widetilde{M}$ be such that $\Gamma \prec_{\mbox{\footnotesize {C}}} \Delta$ and $A \in \Delta$. There exists $\Delta' \ _{\footnotesize {C}} \! \succ \Gamma$ , with $B \in \Delta'$.

Lemma 4.8  

Let $\Gamma \in \widetilde{M}$ with $A \rhd B \in \Gamma$ and let $\Delta \in \widetilde{M}$ be such that $\Gamma \prec_{\mbox{\footnotesize {C}}} \Delta$ and $A \in \Delta$. There exists $\Delta' \ _{\footnotesize {C}} \! \succ \Gamma$ , $B \in \Delta'$ and moreover
$\Box E \in \Delta \Rightarrow \Box E \in \Delta'$. Again $\Delta'$ can be chosen to be maximal with respect to $\Box$-inclusion.