Proof. By induction on x. For a noun $p\in {\mathbf {N}}$ , this is by definition of the model. For a term of the form $({r \ \mathsf{all} \ x})\in {\mathbb {T}}$ , note that $x\in {\mathbb {T}}$ , since ${\mathbb {T}}$ is closed under subterms.

Suppose that $\{t,u\}\in {[\![ {{r \ \mathsf{all} \ x}} ]\!]}$ . Since $x\leq x$ by $({\scriptstyle \mathrm{AX}})$ , the induction hypothesis implies $\{x\}\in [\![ x ]\!]$ . So $\{t,u\}[\![ r ]\!]\{x\}$ . By the definition of $[\![ r ]\!]$ , either $t\leq {r \ \mathsf{all} \ x}$ , or else $u\leq {r \ \mathsf{all} \ x}$ .

Conversely, fix $\{t,u\}\in M$ , and suppose that (without loss of generality) $t\leq {r \ \mathsf{all} \ x}$ . Let $\{v,w \}\in M$ be an element of $[\![ x ]\!]$ . By the induction hypothesis, we have (without loss of generality) $v\leq x$ . By $({\scriptstyle \mathrm{ANTI}})$ , ${r \ \mathsf{all} \ x} \leq {r \ \mathsf{all} \ v}$ . By $({\scriptstyle \mathrm{BARBARA}})$ , $t \leq {r \ \mathsf{all} \ v}$ . So $\{t,u\}[\![ r ]\!]\{v,w \}$ , and hence $\{t,u\}\in {[\![ {{r \ \mathsf{all} \ x}} ]\!]}$ . □

Proof. Suppose $({\mathsf{all } \ x \ y})\in \Gamma $ . If $\{t,u\}\in [\![ x ]\!]$ in ${\cal M}(\Gamma ,{\mathbb {T}})$ , then by Lemma 2.1 (without loss of generality), $t\leq x$ . But then $t\leq y$ by $({\scriptstyle \mathrm{BARBARA}})$ , so $\{t,u\}\in [\![ y ]\!]$ by Lemma 2.1, and ${\cal M}(\Gamma ,{\mathbb {T}})\models {\mathsf{all } \ x \ y}$ .

Now suppose $x,y\in {\mathbb {T}}$ . Since $x\leq x$ and $y\leq y$ , we have $\{x,y\}\in [\![ x ]\!]\cap [\![ y ]\!]$ by Lemma 2.1, so ${\cal M}(\Gamma ,{\mathbb {T}})\models {\mathsf{some} \ x \ y}$ .

If ${\mathbb {T}}$ contains all subterms of sentences in $\Gamma $ , then ${\cal M}(\Gamma ,{\mathbb {T}})\models {\mathsf{all } \ x \ y}$ whenever $({\mathsf{all } \ x \ y})\in \Gamma $ by the first assertion, and ${\cal M}(\Gamma ,{\mathbb {T}})\models {\mathsf{some} \ x \ y}$ whenever $({\mathsf{some} \ x \ y})\in \Gamma $ by the second assertion. □

Proof. Choose ${\mathbb {T}}$ so that it contains x, y, and all terms in $\Gamma $ . If $\Gamma \models {\mathsf{all } \ x \ y}$ , then ${\cal M}(\Gamma ,{\mathbb {T}}) \models {\mathsf{all } \ x \ y}$ by Lemma 2.2. Then $\{x\}\in [\![ x ]\!]\subseteq [\![ y ]\!]$ by $({\scriptstyle \mathrm{AX}})$ and Lemma 2.1. By Lemma 2.1 again, $\Gamma \ {\vdash }_0\ {\mathsf{all } \ x \ y}$ .

To see that the proof uses only the rules $({\scriptstyle \mathrm{AX}})$ , $({\scriptstyle \mathrm{BARBARA}})$ , and $({\scriptstyle \mathrm{ANTI}})$ , we just need to examine the rules in the proof system and note that no rule which produces a conclusion of the form $({\mathsf{all } \ x \ y})$ has a premise of the form $({\mathsf{some} \ a \ b})$ . □

Proof. The proof of (1) is exactly like the proof of Lemma 2.1, with the following adjustment: If $\{t,u\}\in {[\![ {{r \ \mathsf{all} \ x}} ]\!]}$ and $\{x\}\in M'$ , the proof in Lemma 2.1 goes through as written. But if $\{x\}\notin M'$ , then $\Gamma \not\vdash_0\ {\mathsf{some} \ x \ x}$ , so $t\leq {r \ \mathsf{all} \ x}$ (and also $u\leq {r \ \mathsf{all} \ x}$ ), since $\Gamma $ determines existentials for ${\mathbb {T}}$ .

The proof of (2) is exactly as in the proof of Lemma 2.2.

The proof of (3) is also exactly as in the proof of Lemma 2.2, with the following adjustment: We need to use the fact that $({\mathsf{some} \ x \ y})\in \Gamma $ to see that $\{x,y\}\in M'$ .

Putting this together, suppose $\Gamma $ is any theory, ${\mathbb {T}}$ contains all subterms of sentences in $\Gamma $ , and $\Gamma ^*\supseteq \Gamma $ determines existentials for ${\mathbb {T}}$ . If $({\mathsf{all } \ x \ y})\in \Gamma \subseteq \Gamma ^*$ , then ${\cal M}'(\Gamma ^*,{\mathbb {T}})\models {\mathsf{all } \ x \ y}$ . And if $({\mathsf{some} \ x \ y})\in \Gamma \subseteq \Gamma ^*$ , then since $x,y\in {\mathbb {T}}$ , ${\cal M}'(\Gamma ^*,{\mathbb {T}})\models {\mathsf{some} \ x \ y}$ . □

Proof. Since $\Gamma \subseteq \Gamma ^*$ , ${\cal M}'(\Gamma ^*,{\mathbb {T}})\models \Gamma $ by Lemma 2.5, so ${\cal M}'(\Gamma ^*,{\mathbb {T}})\models {\mathsf{some} \ x \ y}$ . Suppose $\{t,u\}\in [\![ x ]\!]\cap [\![ y ]\!]$ . Since $\{t,u\}\in M'$ , $\Gamma ^*\ {\vdash }_0\ {\mathsf{some} \ t \ u}$ . And by Lemma 2.5, $\Gamma ^*\ {\vdash }_0\ {\mathsf{all} \ v\ x}$ and $\Gamma ^*\ {\vdash }_0\ {\mathsf{all} \ w \ y}$ for some $v,w\in \{t,u\}$ . By analyzing the four cases and using $({\scriptstyle \mathrm{SOME}}_{1})$ , $({\scriptstyle \mathrm{SOME}}_{2})$ , and $({\scriptstyle \mathrm{DARII}})$ , we see that $\Gamma ^*\ {\vdash }_0\ {\mathsf{some} \ x \ y}$ . □

Proof. The implication $\Gamma \ {\vdash }_0\ \varphi $ implies $\Gamma \models \varphi $ is just soundness of the rules in ${\vdash }_0$ . The converse follows immediately from Theorems 2.3 and 2.6, taking $\Gamma ^* = \Gamma $ in Theorem 2.6. □

Proof. Suppose $x = t_1,\dots ,t_n = y$ is a $\Gamma $ -sequence. If $n = 1$ , then $x = y$ , and $\Gamma \ {\vdash }_0\ {\mathsf{all } \ x \ y}$ by $({\scriptstyle \mathrm{AX}})$ . If $n>1$ , then for all $1\leq i < n$ , $\Gamma\ {\vdash }_0\ {\mathsf{all} \ {t_i} \ {t_{i+1}}}$ by repeated applications of $({\scriptstyle \mathrm{ANTI}})$ . And by repeated applications of $({\scriptstyle \mathrm{BARBARA}})$ , $\Gamma \ {\vdash }_0\ {\mathsf{all } \ x \ y}$ .

We prove the converse by induction on the height of the proof tree. In the base case, $({\mathsf{all } \ x \ y})\in \Gamma $ , and $x, y$ is a $\Gamma $ -sequence as desired.

Case 1: If the root of the proof tree is

then x is a $\Gamma $ -sequence from x to x.

Case 2: If the root of the proof tree is

then by induction we have $\Gamma $ -sequences $t_1,\dots , t_n$ and $t_1^{\prime },\dots ,t_m^{\prime }$ with $x = t_1$ , $y = t_n = t_1^{\prime }$ , and $z = t_m^{\prime }$ . Then $t_1,\dots ,t_{n-1}, t_1^{\prime },\dots ,t_m^{\prime }$ is a $\Gamma $ -sequence from x to z.

Case 3: If the root of the proof tree is

then by induction we have a $\Gamma $ -sequence $t_1,\dots , t_n$ with $x = t_1$ and $y = t_n$ . Then $(r \ \mathsf{all} \ t_n),\dots ,(r \ \mathsf{all} \ {t_1})$ is a $\Gamma $ -sequence from $({r \ \mathsf{all} \ y})$ to $({r \ \mathsf{all} \ x})$ .□

Proof. Suppose there is a sentence $({\mathsf{some} \ {t_1} \ {t_2}})\in \Gamma $ such that $\Gamma\ {\vdash }_0\ {\mathsf{all} \ t_i \ x}$ and $\Gamma\ {\vdash }_0\ {\mathsf{all} \ {t_j} \ y}$ , for some $i,j\in \{1,2\}$ . Then applying $({\scriptstyle \mathrm{SOME}}_1)$ or $({{\scriptstyle \mathrm{SOME}}_2})$ if necessary, $\Gamma \ {\vdash }_0\ {\mathsf{some} \ {t_i} \ {t_j}}\ \mathsf{some}\ t_i\ t_j.$ By two applications of $({\scriptstyle \mathrm{DARII}})$ and $({\scriptstyle \mathrm{SOME}}_2)$ , $\Gamma \ {\vdash }_0\ {\mathsf{some} \ x \ y}$ .

We prove the converse by induction on the height of the proof tree. In the base case, when $({\mathsf{some} \ x \ y})\in \Gamma $ , we have $\Gamma\ {\vdash }_0\ {\mathsf{all} \ x \ x}$ and $\Gamma\ {\vdash }_0\ {\mathsf{all} \ y \ y}$ by $({\scriptstyle \mathrm{AX}})$ .

Case 1: If the root of the proof tree is

then by induction there is a sentence $({\mathsf{some} \ {t_1} \, {t_2}})\in \Gamma $ such that $\Gamma\ {\vdash }_0\ {\mathsf{all}\ t_i \ x}$ for some $i\in \{1,2\}$ .

Case 2: If the root of the proof tree is

then by induction there is a sentence $({\mathsf{some} \ {t_1}\ {t_2}})\in \Gamma $ such that $\Gamma\ {\vdash }_{0}\ {\mathsf{all}\ {t_i}\;y}$ and $\Gamma\ {\vdash }_0\ {\mathsf{all}\ {t_j}\ x}$ , for some $i,j\in \{1,2\}$ .

Case 3: If the root of the proof tree is

then by induction there is a sentence $(\mathsf{some} \ {t_1} \ {t_2})\in \Gamma $ such that $\Gamma\ {\vdash }_0 \ {\mathsf{all} \ t_i \ x}$ and $\Gamma\ {\vdash }_0\ {\mathsf{all} \ {t_j} \ y}$ , for some $i,j\in \{1,2\}$ . But also $\Gamma \ {\vdash }_0\ {\mathsf{all } \ y \ z}$ , so $\Gamma \ {\vdash }_0\ {\mathsf{all} \ {t_j} \ z}$ by $({\scriptstyle \mathrm{BARBARA}})$ .□

Proof. Let ${\cal M}\models \Gamma _n$ . If $[\![ a ]\!] \neq \emptyset $ , we are done. So we shall assume that $[\![ a ]\!] = \emptyset $ . Then for any verb r, $[\![ {{r \ \mathsf{all} \ a}} ]\!] = M$ . By $\alpha $ , ${\cal M}$ contains an $r_1$ -king x. Then $ {\varphi} _1$ implies that x is also an $r_2$ -king. Continuing by induction, $ {\varphi} _i$ implies that x is an $r_{i+1}$ -king. Finally, x is an $r_n$ -king, and $\omega $ implies that $x\in [\![ a ]\!]$ , which is a contradiction. □

Proof. By Theorem 2.3, $\Gamma _n\ {\vdash }_0\ {\mathsf{all} \ u \ v}$ , and by Lemma 2.9, there is a $\Gamma _n$ -sequence $u = t_1,\dots ,t_m = v$ of length m. If $m =1$ , then $u = v$ and we are done. If $m = 2$ , then $({\mathsf{all} \ u \ v}) = {\text {Anti}}({\vec {r}},\psi )$ for some sequence ${\vec {r}}$ and some $\psi \in \Gamma _n$ ; we are again done.

It remains to prove a contradiction from $m \geq 3$ . Suppose that we have $\psi , \theta \in \Gamma _n$ and sequences of verbs ${\vec {r}}$ and ${\vec {s}}$ such that $(\mathsf{all} \ {t_1} \ {t_2}) = {\text {Anti}}({\vec {r}},\psi )$ and $(\mathsf{all} \ {t_2} \ t_3) = {\text {Anti}}({\vec {s}},\theta )$ . Notice that $t_2$ must contain either a or b. Assume that $t_2$ contains a. The argument when $t_2$ contains b is similar. Let m be the number of verbs in $t_2$ , the second term of ${\text {Anti}}({\vec {r}},\psi )$ . Since it is a rather than b which occurs in the second term of ${\text {Anti}}({\vec {r}},\psi )$ , m is even. We see this by examining the sentences in $\Gamma _n$ . And let n be the number of verbs in $t_2$ , the first term of ${\text {Anti}}({\vec {s}},\theta )$ . This time, we see that n is odd. But $m = n$ , since the second term of ${\text {Anti}}({\vec {r}},\psi )$ is the first term of ${\text {Anti}}({\vec {s}},\theta )$ . This is a contradiction. □

Proof. It suffices to show that for every term $t\neq (r_1 \ \mathsf{all} \ (r_1\ \mathsf{all} \ a))$ , there is a model of $\Delta _{n,i}$ in which $[\![ t ]\!] = \emptyset $ . Indeed, then $\Delta _{n,i}\not \models {\mathsf{some} \ u \ v}$ when $u = t$ or $v = t$ .

We proceed by cases. In every case except $t = a$ , we actually obtain a model of $\Gamma _n$ in which $[\![ t ]\!] = \emptyset $ . Since the models ${\cal M}_4$ of $\Gamma _n$ constructed in Case 4 have ${\cal M}_4\not \models \mathsf{some} \ a \ (r_1 \ \mathsf{all} \ (r_1 \ \mathsf{all} \ a ))$ , this implies the additional result that if $\Gamma _n\models {\mathsf{some} \ u \ v}$ , then $u = v = (r_1 \ \mathsf{all} \ (r_1 \ \mathsf{all} \ a))$ or $u = v = a$ .

Case 1: $t = (\vec {s} \ \mathsf{all} \ b)$ or $t = (\vec {s} \ \mathsf{all} \ a)$ , where the length of ${\vec {s}}$ is odd. Let $M_1 = \{*\}$ , and define the model ${\cal M}_1$ with domain $M_1$ by $[\![ a ]\!] = [\![ b ]\!] = \{*\}$ , and ${[\![ r_i ]\!]} = \emptyset $ for all i. In ${\cal M}_1$ , we have

$$ \begin{align*} [\![ \vec{s} \ \mathsf{all} \ a ]\!] = [\![\vec{s} \ \mathsf{all} \ b ]\!] = \begin{cases} \{*\} & \text{if the length of }\ {\vec{s}} \text{ is even}\\ \emptyset & \text{if the length of }\ {\vec{s}} \ \text{ is odd}, \end{cases} \end{align*} $$

so ${\cal M}_1\models \Gamma _n$ .

Case 2: $t = (\vec {s} \ \mathsf{all} \ b)$ , where the length of ${\vec {s}}$ is even. Define ${\cal M}_2$ in the same way as ${\cal M}_1$ , but with $[\![ b ]\!] = \emptyset $ . This time, we have

$$ \begin{align*} [\![\vec{s} \ \mathsf{all} \ a ]\!] &= \begin{cases} \{ * \} & \text{if the length of } \vec{s} \text{ is even}\\ \emptyset & \text{if the length of } \vec{s} \text{ is odd}\end{cases}\\ [\![\vec{s} \ \mathsf{all} \ b]\!] &= \begin{cases} \emptyset & \text{if the length of } \vec{s} \text{ is even}\\ \{* \} & \text{if the length of } {\vec{s}} \text{ is odd},\end{cases} \end{align*} $$

so again ${\cal M}_2\models \Gamma _n$ .

Case 3: $t = a$ . Fix $1\leq i\leq n$ , let $M_3 = \{*\}$ , and define the model ${\cal M}_3(i)$ with domain $M_3$ by $[\![ a ]\!] = \emptyset $ , $[\![ b ]\!] = \{*\}$ , and

$$ \begin{align*} [\![ r_j ]\!] =\begin{cases}\{(*,*)\} & \text{for }j\leq i\\ \emptyset & \text{for }j>i \end{cases} \end{align*} $$

In ${\cal M}_3(i)$ , we have

$$ \begin{align*} [\![r_j \ \mathsf{all} \ a]\!] = [\![ b ]\!] &= \{* \}\\ {[\![r_j \ \mathsf{all} \ (r_j \ \mathsf{all} \ a) ]\!]} = [\![r_j \ \mathsf{all} \ b ]\!] & = \begin{cases} \{* \} & \text{if } j\leq i\\ \emptyset & \text{if } j> i, \end{cases} \end{align*} $$

so ${\cal M}_3(i)\models \Delta _{n,i}$ .

Case 4: $t = (\vec {s} \ \mathsf{all} \ a)$ , where ${\vec {s}} = (s_1,\dots ,s_k)$ , k is even and nonzero, and ${\vec {s}}\neq (r_1,r_1)$ . Let $M_4 = \{w,x,y,z\}$ , and define a model ${\cal M}_4$ with domain $M_4$ by $[\![ a ]\!] = \{w\}$ and $[\![ b ]\!] = \{w,x,y,z\}$ . To define the verb interpretations $[\![ r_i ]\!]$ , we break into subcases.

Subcase 4a: $s_k\neq r_1$ . Set $x[\![ r_1 ]\!]w$ , $y[\![ r_1 ]\!] x$ , $z{[\![ {s_k} ]\!]}w$ , and no other instances of verbs:

Subcase 4b: $s_k = r_1$ and $s_{k-1}\neq r_1$ . Set $x[\![ r_1 ]\!]w$ , $y[\![ r_1 ]\!] x$ , and no other instances of verbs.

Subcase 4c: $s_k = r_1$ , $s_{k-1} = r_1$ , and $k>2$ . Set $x[\![ r_1 ]\!]w$ , $y[\![ r_1 ]\!] x$ , $z[\![ s_{k-2} ]\!] y$ , and no other instances of verbs.

In all three subcases, ${[\![ r_1 \ \mathsf{all} \ a]\!]} = \{x\}$ and ${[\![ r_1 \ \mathsf{all} \ (r_1 \ \mathsf{all} \ a) ]\!]} = \{y\}$ , so ${\cal M}_4\models \alpha $ . And for all $1\leq i\leq n$ , ${[\![ r_i \ \mathsf{all} \ b]\!]} = \emptyset $ , so ${\cal M}_4 \models \Gamma _n$ . It remains to show that ${[\![ \vec {s} \ \mathsf{all} \ a ]\!]} = \emptyset $ . We introduce some notation: write ${\vec {s}}_{\geq j}$ for the sequence $(s_j,\dots ,s_k)$ .

In subcase 4a, ${[\![s_k \ \mathsf{all } \ a]\!]} = \{z\}$ , and ${[\![s_{\geq k-1} \ \mathsf{all} \ a]\!]} = \emptyset $ . Since k is even we have

$$ \begin{align*} {[\![ \vec{s}_{\geq j} \ \mathsf{all} \ a]\!]} = \begin{cases} \emptyset & \text{if } j \ \text{ is odd} \\ M_4 & \text{if } j \text{ is even}, \end{cases} \end{align*} $$

and ${[\![ \vec {s} \ \mathsf{all} \ a]\!]} = {[\![\vec {s}_{\geq 1}\ \mathsf{all } \ a]\!]} = \emptyset $ .

In subcase 4b, $[\![ s_k \ \mathsf{all} \ a]\!] = \{x\}$ , and ${[\![ s_{\geq k-1} \ \mathsf{all} \ a]\!]} = \emptyset $ . As in subcase 4a, ${[\![ \vec {s} \ \mathsf{all} \ a ]\!]} = \emptyset $ .

In subcase 4c, ${[\![ \vec {s}_{\geq k-2} \ \mathsf{all} \ a]\!]} = \{z\}$ . So ${[\![ \vec {s}_{\geq k-3} \ \mathsf{all} \ a]\!]} = \emptyset $ . And then since k is even and $k\geq 4$ , ${[\![\vec {s}_{\geq 1} \ \mathsf{all } \ a]\!]} = \emptyset $ by the same argument which we have seen above.

This completes the proof. □

Proof. By induction on the depth of the tree witnessing $\Gamma _n\models _k {\mathsf{some} \ u \ v}$ . In the base case, $({\mathsf{some} \ u \ v})$ is a leaf in $\Gamma _n$ . Since $\alpha $ is the only sentence of the form $({\mathsf{some} \ u \ v})$ in $\Gamma _n$ , we are done.

Now suppose the root of the tree is $({\mathsf{some} \ u \ v})$ with children $\{\psi _1, \dots , \psi _j\}$ , where $j\leq k$ , $\Gamma _n\models _k \psi _i$ for all $1\leq i\leq j$ , and $\{\psi _1, \dots , \psi _j\}\models {\mathsf{some} \ u \ v}$ .

We claim that for all $\psi _i$ , there is a single sentence $\chi _i\in \Gamma _n$ such that $\{\chi _{i}\}\models \psi _i$ . By induction, if $\psi _i$ has the form $({\mathsf{some} \ x \ y})$ , then $\psi _i = \alpha $ , and we can take $\chi _i = \alpha $ . On the other hand, if $\psi _i$ has the form $({\mathsf{all } \ x \ y})$ , then since $\Gamma _n\models \psi _i$ , by Lemma 2.13 either $\psi _i = ({\mathsf{all} \ x \ x})$ and we can take $\chi _i$ to be any sentence in $\Gamma _n$ , or $\psi _i = {\text {Anti}}({\vec {r}}_i,\chi _i)$ for some $\chi _i\in \Gamma _n$ , and $\{\chi _{i}\}\models \psi _i$ .

By the claim, $\{\chi _k :k \leq j\} \models {\mathsf{some} \ u \ v}$ . And since $j\leq k \leq n-1$ , there is some $1\leq i^*\leq n$ such that $\{\chi _k :k \leq j\} \subseteq \Delta _{n,i^*}$ . For this $i^*$ , we see that $\Delta _{n,i^*}\models \psi _k$ for all $k\leq j$ , so $\Delta _{n,i^*}\models {\mathsf{some} \ u \ v}$ . Our result follows from Lemma 2.14. □

Proof of Theorem 2.11. By Lemma 2.12, $\Gamma _{n+1}\models {\mathsf{some} \ a \ a }$ . And by Lemma 2.15, $\Gamma _{n+1}\not \models _n {\mathsf{some} \ a \ a }$ .

Suppose that ${\vdash }^*$ is a sound and complete syllogistic proof system for ${\cal L}_{2}$ . Let n be the maximum number of premises in any rule in ${\vdash }^*$ . Then since $\Gamma _{n+1}\models {\mathsf{some} \ a \ a }$ , we have $\Gamma _{n+1}\ {\vdash }^*\ {\mathsf{some} \ a \ a }$ by completeness, and $\Gamma _{n+1}\models _n {\mathsf{some} \ a \ a }$ by soundness. This is a contradiction. □

Proof. As in §1.4, we are going to save on some notation below by writing T for $T(\Gamma \cup \{ {\varphi} \})$ , $T^+$ for $T^+(\Gamma \cup \{ {\varphi} \})$ , and A for $g(\Gamma \cup \{ {\varphi} \})$ .

We are going to do this entire proof in two parts. The first part handles the case that $ {\varphi} $ is either $(\mathsf{all} \ a \ b)\lor (\mathsf{some} \ x \ y)$ or else $(\mathsf{some} \ x \ y)$ . After that, we handle the relatively simpler case that $ {\varphi} $ is $(\mathsf{all} \ a \ b)$ .

So until further notice, we are in the first part of this theorem. Please note that x, y, a, and b are fixed throughout the rest of this proof.

Let $M = M_{xy}$ be the set of unordered pairs $\{t,u\}$ of terms from T such that there is some $z\in \{x,y\}$ such that for all $v\in \{t,u\}$ , $\Gamma \not\vdash_{ A} (\mathsf{all} \ v \ z )\lor (\mathsf{some} \ x\ y)$ .

We allow $t= u$ , and it follows that whenever M contains $\{t,u\}$ , then it also contains $\{t\} = \{t,t\}$ . The point of the definition of M will become clearer after we see the Truth Lemma and Claim 2.35 below: we are building a model which is guaranteed to have $[\![ x ]\!]\cap [\![ y ]\!] = \emptyset $ .

We define a model ${\cal M}$ with domain M by setting

$$ \begin{align*} \begin{aligned} \{t,u\}\in [\![ p ]\!] &{\quad \text{iff}\quad} \text{either } \Gamma \ {{\vdash}_{ A}}\ ({\mathsf{all} \ t \ p})\lor (\mathsf{some} \ x \ y) \text{, or } \Gamma \ {{\vdash}_{ A}}\ {(\mathsf{all} \ u \ p)}\lor (\mathsf{some} \ x \ y)\\\{t,u\}[\![ r ]\!]\{v,w \} & \quad \text{iff}\quad \text{for some}\ c\in \{t,u\}\ \text{and } d\in\{v,w \},\\& \quad \hphantom{\text{iff}}\quad \Gamma\ \vdash_{ A}\ (\mathsf{all} \ c \ (r \ \mathsf{all} \ d))\lor (\mathsf{some} \ x \ y). \end{aligned} \end{align*} $$

Claim 2.33 (Truth Lemma). In ${\cal M}$ ,we have the following for all terms $z\in T$ ,

$$ \begin{align*} {[\![ {z} ]\!]} = \{\{t,u\}\in M : \Gamma \ {{\vdash}_{ A}}\ (\mathsf{all} \ t \ z)\lor (\mathsf{some} \ x \ y) \text{ or }\Gamma \ {{\vdash}_{ A}}\ (\mathsf{all} \ u \ z)\lor (\mathsf{some} \ x \ y)\}.\\ \end{align*} $$

□