Proof Let $\mathcal {M}$ be a structure such that $F_{c}\in \mathsf {D}_{c}$ for all $c\in \mathsf {KIND}_{t}$ . In the first place, $F_{t}=F$ and $\mathsf {D }_{t}^{w}=\left \{ T,F\right \} $ , by condition 4(b) of Definition 2.3. Moreover, $\mathsf {D}_{ab}^{w}=\{f\in \mathsf {D}_{ab}\mid f(\theta )=F_{b}$ for all $\theta \in \mathsf {D}_{a}-\mathsf {D}_{a}^{w}\}$ (by definition), and $F_{ab}(\theta )=F_{b}$ for all $\theta \in \mathsf {D} _{a}$ (by Definition 2.3, Clause (4)(d)). Therefore, $F_{ab}\in \mathsf {D}_{ab}^{w}$ for all $\left \langle a,b\right \rangle \in \mathsf {KIND}_{t}$ .

Proof By induction on the construction of rigid expressions.

Proof By induction on the construction of meaningful expressions, with the help of Lemma 4.2. Please, keep in mind the definition of substitution for downarrow formulas.

Proof By induction on the construction of meaningful expressions, with the help of Lemma 4.2.

Proof By induction on the construction of meaningful expressions.

Proof We will only prove the soundness of two of our more complex schemas, namely the Global constraints schemas (13a and 13b), because the proof is easy for the rest of the elements of the calculus.

• • Global constraints schema for kind e.

  $\mathsf {DEN}(\gamma _{ab})\rightarrow (@_{i}(\mathsf {EXISTS}(\gamma _{ab}))\equiv \mathsf {A}(\lnot i\rightarrow \forall x_{a}(\lnot @_{i}(\mathsf { EXISTS}(x_{a}))\rightarrow \lnot \mathsf {DEN}(\gamma _{ab}x_{a}))))$ ,

  where $\gamma _{ab}\in \mathsf {CME}_{ab}\cap \mathsf {RIGIDS} $ , $\langle a,b\rangle \in \mathsf {TYPES}_{e}$ .

  Let $\left \langle \mathcal {M},g\right \rangle $ be any general interpretation and $w\in W$ an arbitrary world. To see that the Global constraints schema is true under this interpretation at that world we assume that $\lbrack \lbrack \mathsf {DEN}(\gamma _{ab})]]^{\mathcal {M},w,g}=T$ , and so $[[\gamma _{ab}]]^{\mathcal {M},w,g}\not =\divideontimes $ .We divide the proof of the biconditional $\lbrack \lbrack @_{i}(\mathsf {EXISTS}(\gamma _{ab}))\equiv \mathsf {A}(\lnot i\rightarrow \forall x_{a}(\lnot @_{i}(\mathsf {EXISTS}(x_{a}))\rightarrow \lnot \mathsf {DEN}(\gamma _{ab}x_{a}))]]^{\mathcal {M},w,g}=T$ into two conditional parts. By definition:

  1. – $[[@_{i}(\mathsf {EXISTS}(\gamma _{ab}))]]^{\mathcal {M},w,g}{\kern-1.2pt}={\kern-1.2pt}T$ iff $[[\gamma _{ab}]]^{\mathcal {M},v,g}{\kern-1.2pt}\in{\kern-1.2pt} \mathsf {\ D}_{ab}^{v}$ , with $\left [ \mathsf {I}(i)\right ] (v){\kern-1.2pt}={\kern-1.2pt}T$ .

  2. – $[[\mathsf {A}(\lnot i\rightarrow \forall x_{a}(\lnot @_{i} \mathsf {\ EXISTS}(x_{a}))\rightarrow \lnot \mathsf {DEN}(\gamma _{ab}x_{a}))]]^{\mathcal {\ M},w,g}=T$ iff for all $u\in W$ , $\left [ \mathsf {I }(i)\right ] (u)=T$ or $\ [[\forall x_{a}(\lnot @_{i}(\mathsf {EXISTS} (x_{a}))\rightarrow \lnot \mathsf {\ DEN}(\gamma _{ab}x_{a}))]]^{\mathcal {M} ,u,g}=T$ .

  $(\Rightarrow )$ Let $[[@_{i}(\mathsf {EXISTS}(\gamma _{ab}))]]^{\mathcal {M} ,w,g}=T$ . So we know that $[[\gamma _{ab}]]^{\mathcal {M},v,g}$ , as any member of $\mathsf {D}_{ab}^{v}$ , must satisfy the locality for kind e condition and returns undefined $[[\gamma _{ab}]]^{\mathcal {M} ,v,g}(\theta )=\divideontimes $ for any $\theta \in \mathsf {D}_{a}-\mathsf {D} _{a}^{v}$ .

  To be true at w the universal modality formula, it has to be true at any $ u\in W$ . In case $\left [ \mathsf {I}(i)\right ] (u)=T$ the proof is done. Suppose that $\left [ \mathsf {I}(i)\right ] (u)=F$ . To prove that the generalization formula is true at u, take any $\theta \in \mathsf {D} _{a}^{u}$ and assume, in order to arrive to a contradiction, that $\lbrack \lbrack \lnot @_{i}\mathsf {EXISTS}(x_{a})]]^{\mathcal {M} ,u,g_{x_{a}}^{\theta }}=T$ but $\lbrack \lbrack \mathsf {DEN}(\gamma _{ab}x_{a})]]^{\mathcal {M} ,u,g_{x_{a}}^{\theta }}=T$ . From the first assumption we get that $\theta \not \in \mathsf {D}_{a}^{v}$ . From the second, we get that there is a world $w^{\ast }$ where $[[\gamma _{ab}]]^{\mathcal {M} ,u,\left ( g_{x_{a}}^{\theta }\right ) _{s}^{u}}(\theta )\in \mathsf {D} _{b}^{w^{\ast }}$ and so $[[\gamma _{ab}]]^{\mathcal {M},u,\left ( g_{x_{a}}^{\theta }\right ) _{s}^{u}}(\theta )\not =\divideontimes $ . However, $\gamma _{ab}\in \mathsf {CME}_{\langle a,b\rangle }\cap \mathsf {RIGIDS}$ and so $[[\gamma _{ab}]]^{\mathcal {M} ,u,\left ( g_{x_{a}}^{\theta }\right ) _{s}^{u}}=[[\gamma _{ab}]]^{\mathcal {M} ,v,g}$ . Being equal functions, the value of $\theta $ must be the same, but $ [[\gamma _{ab}]]^{\mathcal {M},v,g}(\theta )=\divideontimes $ (due to the locality for kind e condition) while $[[\gamma _{ab}]]^{\mathcal {M},u,\left ( g_{x_{a}}^{\theta }\right ) _{s}^{u}}(\theta )\not =\divideontimes $ . This is a contradiction. Therefore, $[[\lnot \mathsf { DEN}(\gamma _{ab}x_{a})]]^{\mathcal {M},u,g_{x_{a}}^{\theta }}=T$ .

  $(\Leftarrow )$ Suppose that the universal modality formula is true at w. We want to prove that $[[@_{i}(\mathsf {EXISTS}(\gamma _{ab}))]]^{\mathcal {M} ,w,g}=T$ . To obtain a contradiction suppose the opposite, that $[[\gamma _{ab}]]^{ \mathcal {M},v,g}\not \in \mathsf {D}_{ab}^{v}$ , with $\left [ \mathsf {I}(i) \right ] (v)=T$ . By definition of local domains, the last condition means: (a) $Def([[\gamma _{ab}]]^{\mathcal {M},v,g})\not \subseteq \mathsf {D}_{a}^{v}$ or (b) $[[\gamma _{ab}]]^{\mathcal {M},v,g}=\divideontimes $ .

  Case $(a)$ : If $Def([[\gamma _{ab}]]^{\mathcal {M},v,g})\not \subseteq \mathsf {D} _{a}^{v}$ , there is some $\theta \in \mathsf {D}_{a}-\mathsf {D}_{a}^{v}$ such that $[[\gamma _{ab}]]^{\mathcal {M},v,g}(\theta )\neq \divideontimes $ and so $[[\mathsf {DEN}(\gamma _{ab}x_{a})]]^{\mathcal {M},v,g_{x_{a}}^{\theta }}=T $ .

  Let $u\in W$ with $\left [ \mathsf {I}(i)\right ] (u)=F$ and so: if $[[\lnot @_{i}(\mathsf {EXISTS}(x_{a}))]]^{\mathcal {M},u,g_{x_{a}}^{\theta }}=T$ then $ [[\lnot \mathsf {DEN}(\gamma _{ab}x_{a})]]^{\mathcal {M},u,g_{x_{a}}^{\theta }}=T$ . As $\theta \not \in \mathsf {D}_{a}^{v}$ , $[[\lnot \mathsf {DEN}(\gamma _{ab}x_{a})]]^{\mathcal {M},u,g_{x_{a}}^{\theta }}=T$ . However, $\gamma _{ab}$ is closed and rigid and so $[[\gamma _{ab}]]^{\mathcal {M},v,g}=[[\gamma _{ab}]]^{\mathcal {M},v,g_{x_{a}}^{\theta }}=[[\gamma _{ab}]]^{\mathcal {M} ,u,g_{x_{a}}^{\theta }}$ . Therefore, $[[\gamma _{ab}]]^{\mathcal {M} ,u,g_{x_{a}}^{\theta }}(\theta )\neq \divideontimes $ and then $[[\mathsf {DEN }(\gamma _{ab}x_{a})]]^{\mathcal {M},u,g_{x_{a}}^{\theta }}=T$ , which is a contradiction.

  Case $(b)$ : $[[\gamma _{ab}]]^{\mathcal {M},v,g}=\divideontimes $ is not possible as $[[\mathsf {DEN}(\gamma _{ab})]]^{\mathcal {M},w,g}=T$ and so there is a $v^{\ast }\in W$ where $[[\gamma _{ab}]]^{\mathcal {M} ,w,g_{s}^{w}}\in \mathsf {D}_{ab}^{v^{\ast }}$ , and so $[[\gamma _{ab}]]^{ \mathcal {M},w,g_{s}^{w}}\not =\divideontimes $ . But we already noted that the interpretation of $\gamma _{ab}$ remains the same when we change worlds or pass to assignments $g^{\ast }$ that are either s-variant or $x_{a}$ -variant of g. Therefore, $[[\gamma _{ab}]]^{\mathcal {M},v,g}=[[\gamma _{ab}]]^{\mathcal {M},w,g_{s}^{w}}\not =\divideontimes $ , which is a contradiction.

• • Global constraints schema for kind t.

  $@_{i}(\mathsf {EXISTS}(\gamma _{ab}))\equiv \mathsf {A}(\lnot i\rightarrow \forall x_{a}(\lnot @_{i}(\mathsf {EXISTS}(x_{a}))\rightarrow \gamma _{ab}x_{a}\equiv \bot _{b})))$ , where $\gamma _{ab}\in \mathsf {CME}_{ab}\cap \mathsf {RIGIDS} $ , $\langle a,b\rangle \in \mathsf {TYPES}_{t}$ . By definition:

  1. – $[[@_{i}(\mathsf {EXISTS}(\gamma _{ab}))]]^{\mathcal {M},w,g}=T$ iff $ [[\gamma _{ab}]]^{\mathcal {M},v,g}\in \mathsf {D}_{ab}^{v}$ , with $\left [ \mathsf {I}(i)\right ] (v)=T$ .

  2. – $[[\mathsf {A}(\lnot i\rightarrow \forall x_{a}(\lnot @_{i}(\mathsf {EXISTS}(x_{a}))\rightarrow \gamma _{ab}x_{a}\equiv \bot _{b}))]]^{\mathcal {M} ,w,g}=T$ iff for all $w^{\prime }\in W$ , $\left [ \mathsf {I}(i)\right ] (w^{\prime })=T$ or $[[\forall x_{a}(\lnot @_{i}(\mathsf {EXISTS} (x_{a}))\rightarrow \gamma _{ab}x_{a}\equiv \bot _{b})]]^{\mathcal {M},w^{\prime },g}=T$ .

  $(\Rightarrow )$ Suppose that $[[\gamma _{ab}]]^{\mathcal {M},v,g}\in \mathsf {D}_{ab}^{v}$ . Let $w^{\ast }\in W$ . In case $\left [ \mathsf {I}(i)\right ] (w^{\ast })=T$ the proof is done. In case $\left [ \mathsf {I}(i)\right ] (w^{\ast })=F$ the consequent of the formula will be proved. Let $\theta \in \mathsf {D}_{a}^{w^{\ast }}$ . Assume that $[[\lnot @_{i} (\mathsf {EXISTS}(x_{a}))]]^{\mathcal {M},w^{\ast },g_{x_{a}}^{\theta }}=T$ . Hence $\theta \not \in \mathsf {D}_{a}^{v}$ . Since $[[\gamma _{ab}]]^{\mathcal { M},v,g}\in \mathsf {D}_{ab}^{v}$ , we can apply the locality for kind t condition to get $[[\gamma _{ab}]]^{\mathcal {M},v,g}(\theta )=F_{b}$ . We have that, $[[\gamma _{ab}]]^{\mathcal {M},w^{\ast },g_{x_{a}}^{\theta }}(\theta )= \ [[\gamma _{ab}]]^{\mathcal {M},v,g}(\theta )=F_{b}$ (because $ \gamma _{ab}$ is rigid and closed). Therefore, $[[\gamma _{ab}x_{a}\equiv \bot _{b}]]^{\mathcal {M},w^{\ast },g_{x_{a}}^{\theta }}=T$ , as desired.

  $(\Leftarrow )$ Suppose that for all $w^{\prime }\in W$ : If $\left [ \mathsf {I} (i)\right ] (w^{\prime })=F$ then for all $\theta \in \mathsf {D}_{a}^{w^{\prime } } $ we have that $[[(\lnot @_{i}(\mathsf {EXISTS}(x_{a}))\rightarrow \gamma _{ab}x_{a}\equiv \bot _{b})]]^{\mathcal {M},w^{\prime },g_{x_{a}}^{\theta }}=T$ . Let $w^{\ast }\in W$ and $w^{\ast }\not =v$ . So $\left [ \mathsf {I}(i)\right ] (w^{\ast })=F$ (because $\left [ \mathsf {I}(i)\right ] (v)=T$ ). Take any $ \theta \in \mathsf {D}_{a}^{w^{\ast }}$ : if $\theta \not \in \mathsf {D} _{a}^{v} $ then $[[\gamma _{ab}]]^{\mathcal {M},w^{\ast },g_{x_{a}}^{\theta }}(\theta )=F_{b}$ . So, $[[\gamma _{ab}]]^{\mathcal {M},v,g}(\theta )=F_{b}$ (because $\gamma _{ab}$ is rigid and closed and Proposition 2.12). We want to see that $[[@_{i}(\mathsf {EXISTS}(\gamma _{ab}))]]^{\mathcal {M} ,w,g}=T$ . In the first place, being a general structure, $[[\gamma _{ab}]]^{ \mathcal {M},v,g}\in \mathsf {D}_{ab}$ , as this expression is of kind t. Moreover, we just saw that it satisfies the locality for kind t condition because for all $\theta \in \mathsf {D}_{a}-\mathsf {D} _{a}^{v}$ the value of the function is $F_{b}$ . Therefore, $[[\gamma _{ab}]]^{\mathcal {M},v,g}\in \mathsf {D}_{ab}^{v}$ and so $[[@_{i}(\mathsf { EXISTS}(\gamma _{ab}))]]^{\mathcal {M},w,g}=T$ , as desired.

Proof A straightforward exercise in propositional hybrid logic.

Proof The first claim follows because $@_{i}i^{\prime }\rightarrow \left ( @_{i}\Diamond j\rightarrow @_{i^{\prime }}\Diamond j\right ) $ is provable by Axiom 3c, rule Gen $_{@}$ , and Axioms 1c and 3d, and so belongs to $\Gamma ^{\ast }$ . Thus, as $@_{i}i^{\prime }\in \Gamma ^{\ast }$ and $@_{i}\Diamond j\in \Gamma ^{\ast }$ , we have that $ @_{i^{\prime }}\Diamond j\in \Gamma ^{\ast }$ (as $\Gamma ^{\ast }$ is closed under Modus Ponens). The second claim follows because $@_{i}\Diamond j\wedge @_{j}j^{\prime }\rightarrow @_{i}\Diamond j^{\prime }$ is the Bridge $ _{\Diamond }$ theorem (page 14) and so belongs to $\Gamma ^{\ast }$ . Thus, as $@_{i}\Diamond j\in \Gamma ^{\ast }$ and $@_{j}j^{\prime }\in \Gamma ^{\ast }$ , we have that $@_{i}\Diamond j^{\prime }\in \Gamma ^{\ast }$ , as required.

Proof We establish the six items as follows:

1. (1) By definition, $\mathsf {D}_{t}=\{T,F\}$ . We will prove that

   $\{T,F\} = \left \{ \Phi (\varphi )\mid \varphi \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash \mathsf {DEN}(\varphi )\right \}$ .

   First, we show that $\{T,F\}\subseteq \{ \Phi (\varphi )\mid \varphi \in \mathsf {CME} _{t}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash \mathsf {DEN}(\varphi ) \}$ . Clearly, $\bot \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS}$ , $\Gamma ^{\ast }\vdash \mathsf {DEN}(\bot )$ by Axiom 8b, and $\Phi (\bot )=F$ by the consistency of $\Gamma ^{\ast }$ . Thus, $F\in \{ \Phi (\varphi )\mid \varphi \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS}\text{and }\Gamma ^{\ast }\vdash \mathsf {DEN}(\varphi ) \}$ . We also prove it for T using a similar reasoning.

   Secondly, we have that either $\Phi (\varphi )=T$ or $\Phi (\varphi )=F$ for every $\varphi \in \mathsf {CME}_{t}$ , because by maximality either $\Gamma ^{\ast }\vdash \varphi $ or $\Gamma ^{\ast }\vdash \lnot \varphi $ .

2. (2) On the one hand, by definition $\Phi (\varphi )\not =\mathsf {\ \divideontimes }$ for any $\varphi \in \mathsf {CME}_{t}$ . On the other hand, since $\Gamma ^{\ast }\vdash \mathsf {DEN}(\varphi )$ (by Axiom 8b) and $\Gamma ^{\ast }$ is maximal consistent, $\Gamma ^{\ast }\not \vdash \lnot \mathsf {DEN}(\varphi )$ for any $\varphi \in \mathsf {CME}_{t}$ . Thus, $\Phi (\varphi )=\mathsf {\divideontimes }$ iff $ \Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\varphi )$ .

3. (3) Let $\varphi $ , $\psi \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS}$ . On the one hand, by using the definitions and the properties of maximal consistent sets, it is easy to see that (1) if $\Phi (\varphi )=T=\Phi (\psi )$ then $\Gamma ^{\ast }\vdash \varphi $ and $\Gamma ^{\ast }\vdash \psi $ and so $\Gamma ^{\ast }\vdash \varphi \equiv \psi $ , and (2) if $ \Phi (\varphi )=F=\Phi (\psi )$ then $\Gamma ^{\ast }\vdash \lnot \varphi $ and $\Gamma ^{\ast }\vdash \lnot \psi $ and so $\Gamma ^{\ast }\vdash \varphi \equiv \psi $ . On the other hand, if $\Gamma ^{\ast }\vdash \varphi \equiv \psi $ then it is impossible to have $\Phi (\varphi )=T$ and $\Phi (\psi )=F$ . For $\Phi (\varphi )=T$ implies $\Gamma ^{\ast }\vdash \varphi $ and so $\Gamma ^{\ast }\vdash \psi $ too, which means that $\Phi (\psi )=T$ as well.

4. (4) By definition, $\mathsf {D}_{t}^{\left [ i\right ] }=\{T,F\}$ . We want to prove that $\{T,F\}=\{\Phi (\varphi )\mid \varphi \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS }\text { and }\Gamma ^{\ast }\vdash @_{i}(\mathsf {EXISTS}(\varphi ))\}$ . On the one hand, $\{\Phi (\varphi )\mid \varphi \in \mathsf {CME}_{t}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash @_{i}(\mathsf {EXISTS}(\varphi ))\}\subseteq \{T,F\}$ , by definition of $\Phi $ . Also, we have already seen that $\Phi (\bot )=F$ and $\Phi (\top )=T$ . Moreover, $\vdash @_{i}(\mathsf {EXISTS}(\varphi ))$ , as $(\varphi \equiv \top )\vee (\varphi \equiv \bot )$ is a tautology and we can use Rule Gen $_{@}$ . In particular, $\vdash @_{i}( \mathsf {EXISTS}(\bot ))$ and $\vdash @_{i}(\mathsf {EXISTS}(\top ))$ . Thus we have the reverse inclusion as well.

5. (5) That $\mathsf {D}_{t}=\{T,F\}=\bigcup \limits _{[i]\in W}\mathsf {D} _{t}^{[i]}$ is now clear.

6. (6) Condition (6) is immediate as, by consistency, $\Gamma ^{\ast }\not \vdash \bot $ and so $\Phi (\bot )=F$ .

Proof We establish these conditions as follows:

1. (1) Immediate: the definition of $\mathsf {D}_e$ simply restates the first condition.

2. (2) If $\Gamma ^\ast \vdash \lnot \mathsf {DEN}(\alpha _e)$ then by consistency $\Gamma ^\ast \not \vdash \mathsf {DEN}(\alpha _e)$ and so $\Phi (\alpha _e)=\mathsf {\divideontimes }$ . If $\Phi (\alpha _e)= \mathsf {\divideontimes }$ then $\Gamma ^\ast \vdash \lnot \mathsf {DEN}(\alpha _e)$ .

3. (3) Let $\alpha _{e}$ , $\delta _{e}\in \mathsf {CME}_{e}\cap \mathsf {RIGIDS}$ such that $\Gamma ^{\ast }\vdash \mathsf {DEN}(\alpha _{e})$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\delta _{e})$ . Then, $\Phi (\alpha _{e}) =\{\beta _{e}\mid \beta _{e}\in \mathsf {CME}_{e}\cap \mathsf {RIGIDS}$ and $\Gamma ^{\ast }\vdash \alpha _{e}\equiv \beta _{e}\},\ \text {and}$

   $\Phi (\delta _{e}) =\{\beta _{e}\mid \beta _{e}\in \mathsf {CME}_{e}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash \delta _{e}\equiv \beta _{e}\}$ . If $\Phi (\alpha _{e})=\Phi (\delta _{e})$ then $\Gamma ^{\ast }\vdash \alpha _{e}\equiv \delta _{e}$ , using Equality Schemas (Axioms 4) for $\simeq $ and the fact that $\Gamma ^{\ast }\vdash \mathsf {DEN}(\alpha _{e})$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\delta _{e})$ that allow us to use $\equiv $ instead of $\simeq $ (by applying Proposition 6.3(1b)). The other direction, $\Gamma ^{\ast }\vdash \alpha _{e}\equiv \delta _{e}$ implies $\Phi (\alpha _{e})=\Phi (\delta _{e})$ , is obvious (by the same reasons as above).

4. (4) We define $\mathsf {D}_{e}^{[i]}=\{\Phi (\alpha _{e})\mid \alpha _{e}\in \mathsf {CME} _{e}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash @_{i}(\mathsf {EXISTS}(\alpha _{e}))\}$ . This set is not empty because for every $v_{e}\in \mathsf {VAR}_{e}$ , $ \vdash \exists v_{e}\top $ (Axiom 2a) and then, using the Gen $_{@}$ Rule, we have that $@_{i}\exists v_{e}\top \in \Gamma ^{\ast }$ as well. As $\Gamma ^{\ast }$ is $\exists $ -saturated, there is a constant $ c_{e}$ such that $@_{i}(\mathsf {EXISTS}(c_{e}))\in \Gamma ^{\ast }$ . Thus, $\Phi (c_{e})\in \mathsf {D}_{e}^{[i]}$ . As $\vdash @_{i}(\mathsf {EXISTS }(c_{e})\equiv @_{i}\mathsf {EXISTS}(@_{i}c_{e}))$ (by Axiom 5b and Proposition 6.3(1b)) we obtain $@_{i}(\mathsf {EXISTS}(@_{i}c_{e}))\in \Gamma ^{\ast }$ and then we have $\Phi (@_{i}c_{e})\in \mathsf {D}_{e}^{[i]}$ because $ @_{i}c_{e}\in \mathsf {CME}_{e}\cap \mathsf {RIGIDS}$ .

5. (5) Suppose that $\Phi (\alpha _{e})\in \mathsf {D}_{e}$ . Note that this means that $\alpha _{e} \in \mathsf {RIGIDS}$ . Hence from the fact that $\Gamma ^{\ast }\vdash \mathsf {DEN}(\alpha _{e})$ , and Proposition 6.3(3a) we have $\Gamma ^{\ast }\vdash \mathsf {E(EXISTS} (\alpha _{e})$ . Hence by the $\mathsf {E}$ -saturation of $\Gamma ^{\ast }$ , there is a nominal i such that $\Gamma ^{\ast }\vdash @_{i}\mathsf {(EXISTS} (\alpha _{e}))$ . So $\Phi (\alpha _{e})\in \mathsf {D}_{e}^{\left [ i\right ] }$ . The reverse inclusion follows using $\vdash @_{i}(\mathsf {EXISTS}(\alpha _{a}))\rightarrow \mathsf {DEN}(\alpha _{a})$ (it follows easily from Axiom 9b, Rule Gen $_{@}$ , Distributivity Axiom 1c, Proposition 6.3(1c), and previous Proposition 6.3(1e)). Thus, we have shown that $\mathsf {D}_{e}=_{\ }\bigcup \limits _{i\in \mathsf {NOM}}\mathsf {D}_{e}^{\left [ i\right ]}$ .

Proof Let $\Phi (\alpha _{a}),\Phi (\beta _{a})\in \mathsf {D}_{a}$ , and $\Phi (\alpha _{a})=\Phi (\beta _{a})$ . By the induction hypothesis on type a, as $\Gamma ^{\ast }\vdash \mathsf {DEN}(\alpha _{a})$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\beta _{a})$ , we have that $\Gamma ^{\ast }\vdash \alpha _{a}\equiv \beta _{a}$ , and so $\Gamma ^{\ast }\vdash \alpha _{a}\simeq \beta _{a}$ , by definition of $\simeq $ . Then $\Gamma ^{\ast }\vdash @_{i_{n}}\gamma _{ab}\alpha _{a}\simeq @_{i_{n}}\gamma _{ab}\beta _{a}$ , by Axiom 11a and maximal consistency.

We now have two cases: (i) $\Gamma ^{\ast }\vdash @_{i_{n}}\gamma _{ab}\alpha _{a}\equiv @_{i_{n}}\gamma _{ab}\beta _{a}$ or (ii) $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(@_{i_{n}}\gamma _{ab}\alpha _{a})$ and $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(@_{i_{n}}\gamma _{ab}\beta _{a})$ . Either way, we have that $\Phi (@_{i_{n}}\gamma _{ab}\alpha _{a})=\Phi (@_{i_{n}}\gamma _{ab}\beta _{a})$ , by the induction hypothesis on type b (conditions (3) and (2) from Figure 2).

Proof We establish these conditions as follows:

1. (1) By definition $\mathsf {D}_{ab}=\left \{ \Phi (\gamma _{ab})\mid \gamma _{ab}\in \mathsf {CME}_{ab}\cap \mathsf {RIGIDS} \text { and } \Gamma ^\ast \vdash \mathsf {DEN}(\gamma _{ab})\right \}$ .

2. (2) By definition of $\Phi $ , $\Phi (\gamma _{ab})=\mathsf {\ \divideontimes }$ iff $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\gamma _{ab})$ .

3. (4) $\mathsf {D}_{ab}^{\left [ i\right ] }=\left \{ \Phi (\gamma _{ab})\mid \gamma _{ab}\in \mathsf {CME}_{b}\cap \mathsf {RIGIDS}\text { and }\Gamma ^{\ast }\vdash @_{i}(\mathsf {EXISTS}(\gamma _{ab}))\right \} $ by definition. We need to show that each local domain is non-empty. By the induction hypothesis, $\mathsf {D}_{b}\not =\varnothing $ , and so there is $\Phi (\beta _{b})\in \mathsf {D}_{b}$ with $\beta _{b}\in \mathsf {CME}_{b}\cap \mathsf {RIGIDS}$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\beta _{b})$ . By the induction hypothesis, $\mathsf {D}_{b}^{\left [ i\right ]}\not =\varnothing $ , and so there is $\Phi (\beta _{b})\in \mathsf {D}_{b}$ with $\beta _{b}\in \mathsf {CME}_{b}\cap \mathsf {RIGIDS}$ and $\Gamma ^{\ast }\vdash @_{i}(\mathsf {EXISTS}(\beta _{b}))$ . From the Comprehension axiom (9a) and the Rule Gen $_{@}$ , we have that $\vdash @_{i}(\mathsf {EXISTS}\left \langle \lambda x_{a}\beta _{b}\right \rangle )$ and so $\Gamma ^{\ast }\vdash @_{i}(\mathsf { EXISTS}@_{i}\left \langle \lambda x_{a}\beta _{b}\right \rangle )$ , as $\vdash @_{i}(\mathsf {EXISTS}\left \langle \lambda x_{a}\beta _{b}\right \rangle ) \ \equiv @_{i}(\mathsf {EXISTS}@_{i}\left \langle \lambda x_{a}\beta _{b}\right \rangle )$ (by Axiom 5b and Proposition 6.3(1b)) and maximal consistency. Therefore, $\Phi (@_{i}\left \langle \lambda x_{a}\beta _{b}\right \rangle )\in \mathsf {D}_{ab}^{\left [ i\right ] }$ , as required.

4. (5) We want to prove that $\mathsf {D}_{ab}=\displaystyle \bigcup \limits _{[i]\in W}\mathsf {D}_{ab}^{[i]}$ . First, any element of $\mathsf {D}_{ab}$ is of the form $\Phi (\gamma _{ab})\in \mathsf {D}_{ab}$ with $\Gamma ^{\ast }\vdash \mathsf {DEN} (\gamma _{ab})$ and $\gamma _{ab}\in \mathsf {CME}_{b}\cap \mathsf {RIGIDS}$ . By Proposition 6.3(3a) it follows that $\Gamma ^{\ast }\vdash \mathsf {E(EXISTS}(\gamma _{ab}))$ . Hence, by $\mathsf {E}$ -saturation, there is a nominal i such that $@_{i}\mathsf {(EXISTS}(\gamma _{ab}))\in \Gamma ^{\ast }$ . Therefore, $\Phi (\gamma _{ab})\in \mathsf {D}_{ab}^{[i]}$ . To prove the converse, use the logical theorem $@_{i}\mathsf {(EXIST}(\gamma _{ab}))\rightarrow \mathsf {DEN}(\gamma _{ab})$ . The proof of this theorem uses the same axioms and rules already applied in Proposition 9.7(5).

5. (3) Let $\gamma _{ab}$ , $\delta _{ab}\in \mathsf {CME}_{ab}\cap \mathsf {RIGIDS}$ such that $\Gamma ^{\ast }\vdash \mathsf {DEN}(\gamma _{ab})$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\delta _{ab})$ . We want to show that $\Phi (\gamma _{ab})=\Phi (\delta _{ab})$ iff $\Gamma ^{\ast }\vdash \gamma _{ab}\equiv \delta _{ab}$ .

   ( $\Rightarrow $ ) Suppose that $\Phi (\gamma _{ab})=\Phi (\delta _{ab})$ . From conditions (4) and (5) in Figure 2, we have $\Phi (\gamma _{ab}),\Phi (\delta _{ab})\in \mathsf {D}_{ab}^{[i]}$ for some nominal i. Thus the following two statements are true: (1) $\Gamma ^{\ast }\vdash @_{i}( \mathsf {EXISTS}(\gamma _{ab}))$ and (2) $\Gamma ^{\ast }\vdash @_{i}( \mathsf {EXISTS}(\delta _{ab}))$ . Furthermore, using Extensionality (Axiom 12), the Gen $_{@}$ Rule, and Axiom 1c we can prove that $(@_{i}(\mathsf {EXISTS}(\gamma _{ab}))\wedge @_{i}(\mathsf {\ EXISTS}(\delta _{ab})))\rightarrow (@_{i}\forall x_{a}\left ( \gamma _{ab}x_{a}\simeq \delta _{ab}x_{a}\right ) \rightarrow @_{i}(\gamma _{ab}\equiv \delta _{ab}))$ is a theorem. Therefore, $\Gamma ^{\ast }\vdash (@_{i}\forall x_{a}\left ( \gamma _{ab}x_{a}\simeq \delta _{ab}x_{a}\right ) \rightarrow @_{i}(\gamma _{ab}\equiv \delta _{ab}))$ .

   So let us suppose for the sake of contradiction that $\Gamma ^{\ast }\not \vdash \gamma _{ab}\equiv \delta _{ab}$ . Since $\gamma _{ab}$ , $\delta _{ab}\in \mathsf {RIGIDS}$ , $\Gamma ^{\ast }\not \vdash @_{i}(\gamma _{ab}\equiv \delta _{ab})$ (by Equality schemas, Axioms 3d and 5a, and Proposition 6.3(1b)) and so we have $\Gamma ^{\ast }\vdash \lnot @_{i}\forall x_{a}(\gamma _{ab}x_{a}\simeq \delta _{ab}x_{a})$ . Hence, using Axiom 3b we have that $\Gamma ^{\ast }\vdash @_{i}\exists x_{a}\lnot (\gamma _{ab}x_{a}\simeq \delta _{ab}x_{a})$ . So by existential saturation there is a constant $c_{a}$ such that $@_{i}(\mathsf { \ EXISTS}(c_{a}))\in \Gamma ^{\ast }$ and $\Gamma ^{\ast }\vdash @_{i}\lnot (\gamma _{ab}@_{i}c_{a}\simeq \delta _{ab}@_{i}c_{a})$ . Now, by using Proposition 6.3(2f) as well as the functional schemas (11a and 11b) and Axiom 3d, we obtain $\Gamma ^{\ast }\vdash \lnot (\gamma _{ab}@_{i}c_{a}\simeq \delta _{ab}@_{i}c_{a})$ . However, as we shall now show, $\Gamma ^{\ast }\vdash (\gamma _{ab}@_{i}c_{a}\simeq \delta _{ab}@_{i}c_{a})$ , and we have the contradiction. In the first place, since $\Phi (\gamma _{ab})=\Phi (\delta _{ab})$ , we have that $\Phi (\gamma _{ab})(\Phi (@_{i}c_{a}))=\Phi (\delta _{ab})(\Phi (@_{i}c_{a}))$ and we will prove that $\Phi (\gamma _{ab}(@_{i}c_{a}))=\Phi (\delta _{ab}(@_{i}c_{a}))$ . To see this, note that by the definition of $ \Phi $ , the induction hypothesis for condition (3) of Figure 2, Axiom 3d, then, since either both $ @_{i_{n}}\gamma _{ab}(@_{i}c_{a})$ and $\gamma _{ab}(@_{i}c_{a})$ denote or neither of them do, we have that:

   1. – $\Phi (\gamma _{ab})(\Phi (@_{i}c_{a}))=\Phi (@_{i_{n}}\gamma _{ab}(@_{i}c_{a}))=\Phi (\gamma _{ab}(@_{i}c_{a}))$ , and

   2. – $\Phi (\delta _{ab})(\Phi (@_{i}c_{a}))=\Phi (@_{i_{n}}\delta _{ab}(@_{i}c_{a}))=\Phi (\delta _{ab}(@_{i}c_{a}))$ .

   Therefore, $\Phi (\gamma _{ab}(@_{i}c_{a})\kern-0.3pt)\kern1.2pt{=}\kern1.2pt\Phi (\delta _{ab}(@_{i}c_{a}\kern-0.1pt)\kern-0.3pt)$ . Moreover, either $\Gamma ^{\ast }\kern1.2pt{\vdash}\kern1.2pt \mathsf {DEN} (\gamma _{ab}@_{i}c_{a}\kern-0.1pt)$ and $ \Gamma ^{\ast }\vdash \mathsf {DEN}(\delta _{ab}@_{i}c_{a})$ , or $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\gamma _{ab}@_{i}c_{a})$ and $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\delta _{ab}@_{i}c_{a})$ . Hence, by the induction hypothesis and the definition of $\simeq $ , we have $\Gamma ^{\ast }\vdash (\gamma _{ab}@_{i}c_{a}\simeq \delta _{ab}@_{i}c_{a})$ . This contradicts our previous statement, which was obtained from the supposition that $\Gamma ^{\ast }\not \vdash \gamma _{ab}\equiv \delta _{ab}$ .

   ( $\Leftarrow $ ) Suppose $\Gamma ^{\ast }\vdash \gamma _{ab}\equiv \delta _{ab}$ . Then, $\Gamma ^{\ast }\vdash \gamma _{ab}\simeq \delta _{ab}$ . So by Axiom 11b we have that for any $\alpha _{a}$ , all the equalities of the form $\gamma _{ab}\alpha _{a}\simeq \delta _{ab}\alpha _{a}$ are in $\Gamma ^{\ast }$ . Now, let $\Phi (\alpha _{a})$ be some arbitrary element of $\mathsf {D}_{a}$ . Then we have:

   1. – $\Phi (\gamma _{ab})(\Phi (\alpha _{a}))=\Phi (@_{i_{n}}\gamma _{ab}(\alpha _{a}))=\Phi (\gamma _{ab}(\alpha _{a}))$ , and

   2. – $\Phi (\delta _{ab})(\Phi (\alpha _{a}))=\Phi (@_{i_{n}}\delta _{ab}(\alpha _{a}))=\Phi (\delta _{ab}(\alpha _{a}))$ .

   So using the equalities $\gamma _{ab}\alpha _{a}\simeq \delta _{ab}\alpha _{a}$ that are in $\Gamma ^{\ast }$ we have that either $\Gamma ^{\ast }\vdash \mathsf {DEN}(\gamma _{a,b}\alpha _{a})$ and $\Gamma ^{\ast }\vdash \mathsf {DEN}(\delta _{ab}\alpha _{a})$ and $\Gamma ^{\ast }\vdash \gamma _{ab}\alpha _{a}\equiv \delta _{ab}\alpha _{a}$ , or $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\gamma _{ab}\alpha _{a})$ and $\Gamma ^{\ast }\vdash \lnot \mathsf {DEN}(\delta _{ab}\alpha _{a})$ . Either way we have that $\Phi (\gamma _{ab}\alpha _{a})=\Phi (\delta _{ab}\alpha _{a})$ , as by the induction hypothesis on type b, the first holds by condition (3) from Figure 2, and in the second case both are undefined by condition (2). Therefore, $\Phi (\gamma _{ab})=\Phi (\delta _{ab})$ .