Proof The proof derives as a special case from the proof of Theorem 2.10. ⊣

Proof Let S be:

$$\begin{align*}\phi _{1}(v_0, \ldots , v_n), \ldots , \phi _{p}(v_0, \ldots , v_n) \vdash \psi _{1}(v_0, \ldots , v_n), \ldots , \psi _{q}(v_0, \ldots , v_n).\end{align*}$$

Writing $\phi $ for $\sum_{1\leq k\leq p}\phi _k$ and $\psi $ for $\sum_{1\leq l\leq q}\psi _l$ , one has, for n even:

$$ \begin{align*} & \partial^{\exists}_n(S)\\&= (\exists x\phi(x,v_{0},\ldots,v_{n-1})\vdash \exists x\psi(x,v_{0},\ldots,v_{n-1}))\\& - (\exists x\phi(v_0,x,v_{1},\ldots,v_{n-1})\vdash \exists x\psi(v_0,x,v_{1},\ldots,v_{n-1})) + \cdots \\& \cdots + (\exists x\phi(v_{0},\ldots,v_{n-1},x)\vdash \exists x\psi(v_{0},\ldots,v_{n-1},x))\\&= (\exists x\phi(x,v_{0},\ldots,v_{n-1}), \exists x\psi(v_0,x,v_{1},\ldots,v_{n-1}), \exists x\phi(v_0,v_1,x,\ldots,v_{n-1}), \end{align*} $$

$$ \begin{align*} & \ldots, \exists x\phi(v_{0},\ldots,v_{n-1},x)) \vdash (\exists x\psi(x,v_{0},\ldots,v_{n-1}), \exists x\phi(v_0,x,v_{1},\ldots,v_{n-1}),\\& \exists x\psi(v_0,v_1,x,\ldots,v_{n-1}), \ldots, \exists x\psi(v_{0},\ldots,v_{n-1}, x)). \end{align*} $$

Then, writing ‘ $\phi _{01x2\ldots. n}$ ’ as a shorthand for $\exists x\phi (v_0, v_1, x, v_2, \ldots , v_n)$ , one can see that each $\widetilde {\exists _i}$ , for $0\leq i\leq n-1$ , will produce, if i is even (resp. odd), $\phi _{x0\ldots i-1yi\ldots n-2}$ , $\psi _{0x1\ldots i-1y i\ldots n-2}$ , …, $\phi _{0\ldots i-1yi\ldots x}$ on the left side (resp. right side) of the sequent and $\psi _{x0\ldots i-1yi\ldots n-2}$ , $\psi _{0x1\ldots i-1yi\ldots n-2}$ , …, $\psi _{0\ldots i-1yi\ldots x}$ on the right side (resp. left side). So $\widetilde {\exists _i}$ and $\widetilde {\exists _{i+1}}$ , put together, will produce the same sequent. Since n is supposed to be even, the n indices i between $0$ and $n-1$ can all be considered pairwise, and so in the end the right and left sides of $\partial ^{\exists }_{n-1}(\partial ^{\exists }_n(S))$ match up. The proof in case n is odd is analogous. ⊣

Proof The simplicial identities between the operators $\exists ^{M}_i$ and $E_j^{M}$ are the semantic counterpart of the simplicial identities which turn $F_*$ into a simplicial set. ⊣

Proof Let N be an extension of M. Then $r_n : D_n(N)\rightarrow N^M_n$ , where $N^M_n$ is the set of all $\phi (N, M) := \{\vec {a}\in |M|^{n+1} : N\vDash \phi (v_0, \ldots , v_n) [\vec {a}]\}$ for $\phi \in F_n$ . Furthermore, the sequence $(N^M_n)_{n\in \mathbb {N}}$ can be endowed with a simplicial structure $N^M_*$ , with $\exists ^{N^M}_i : \{\vec {b}\in |M|^{n+1} : N\vDash \phi (\vec {v}) [\vec {b}]\}\mapsto \{\vec {b^{\prime }}\in |M|^{n} : N\vDash \exists _i(\phi ) [\vec {b^{\prime }}]\}$ and $E^{N^M}_j : \{\vec {b}\in |M|^{n} : N\vDash \phi (\vec {v}) [\vec {b}]\}\mapsto \{(\vec {b}, b_j)\in |M|^{n+1} : N\vDash \phi (\vec {v}) [\vec {b}]\}$ , for each $\phi \in F_n$ .

Now, suppose that $r_*$ is a simplicial morphism:

Then it turns out that $N^M_*$ is in fact $M_*$ . This point is proved by induction on $\phi $ . Since M is a substructure of N, $\phi (N, M) = \phi ^M$ for each negatomic L-formula $\phi \in F_n$ . It is straightforward, by induction, that $(\phi \wedge \psi )(N, M) = (\phi (N, M)\wedge \psi (N, M)) = (\phi ^M\wedge \psi ^M) = (\phi \wedge \psi )^M$ . Finally:

$$ \begin{align*} (\exists x\phi(v_0, \ldots, v_{i-1}, x, v_i, \ldots, v_n))(N, M) &= r_n(\exists^{N}_i(\phi(v_0, \ldots, v_{n+1})))\\ &= \exists^{N^M}_i(r_{n+1}(\phi(v_0, \ldots, v_{n+1}))). \end{align*} $$

By induction hypothesis, $r_{n+1}(\phi )\in D_{n+1}(M)$ , so $\exists ^{N^M}_i(r_{n+1}(\phi )) = (\exists x\phi )(N, M)$ is in $D_n(M)$ . Now, the fact that the restriction maps $r_n$ make up a simplicial morphism from $N_*$ to $M_*$ is the direct expression that the Tarski–Vaught test is met. Indeed, suppose $N\vDash \exists x\phi (x, \overline {a_1}, \ldots , \overline {a_n})$ . Then $(\phi (v_0, \overline {a_1}, \ldots , \overline {a_n}))^N\in N_0'$ , so $r_0(\phi (v_0, \overline {a_1}, \ldots , \overline {a_n})^N) = \phi (v_0, \overline {a_1}, \ldots , \overline {a_n})(N, M)\in M_0'$ is nonempty, which means that there is some $a\in |M|$ such that $N\vDash \phi (v_0, \overline {a_1}, \ldots , \overline {a_n}) [a]$ . As a result, M is an elementary substructure of N.

Conversely, suppose that M is an elementary substructure of N. Then, it is routine verification to check that $r_*$ is a simplicial map, with codomain $M_*$ , and thus a simplicial morphism $r : N_*\rightarrow M_*$ . The elementwise commutativity of the diagram involving $r_n$ and $r_{n-1}$ follows from the Tarski–Vaught test. Indeed, let us consider $\phi \in F_n$ and let us suppose that $(a_1, \ldots , a_n)\in |M|^n$ . Then:

$N\vDash \exists x\phi (\overline {a_1}, \ldots , \overline {a_i}, x, \overline {a_{i+1}}, \ldots , \overline {a_n})$

iff there exists $a\in |M|$ such that $N\vDash \phi (\overline {a_1}, \ldots , \overline {a_i}, v_0, \overline {a_{i+1}}, \ldots , \overline {a_n}) [a]$

iff there exists $a\in |M|$ such that $(a_1, \ldots , a_i, a, a_{i+1}, \ldots , a_n)\in \phi ^N\cap |M|^{n+1}$

iff $(a_1, \ldots , a_n)\in \exists _i(\phi ^N\cap |M|^{n+1})$ .

Thus $\exists _i(\phi ^N)\cap |M|^n = \exists _i(\phi ^N\cap |M|^{n+1})$ for every L-formula $\phi \in F_n$ .⊣

Proof Any elementary embedding $f : M\rightarrow N$ gives rise to a simplicial morphism $f_* : N_*\rightarrow M_*$ , in a functorial way, with $f_n : \phi ^N\mapsto \{\vec {a}\in |M|^{n+1} : N\vDash \phi [f(\vec {a})]\} = \phi ^M$ .⊣

Proof Suppose $|M|$ is definable in N by some L-formula $\underline {M}(v_0)$ . Since $N\vDash \phi [\vec {b}]$ iff $\vec {b}\in |M|^{n+1}$ and $M\vDash \phi [\vec {b}]$ , for any $\phi \in F_n$ , the diagram

commutes. Indeed, using the Tarski–Vaught test, one has:

$$ \begin{align*} N\vDash \exists_i(\phi^{\underline{M}}) [\vec{b'}]\ & \text{iff}\ N\vDash \phi^{\underline{M}} [b'_0, \ldots, b'_{i-1}, c_i, b'_i, \ldots, b'_{n-1}]\ \ \text{for some}\ c_i\in |N|\\&\text{iff}\ N\vDash \phi^{\underline{M}} [b'_0, \ldots, b'_{i-1}, d_i, b'_i, \ldots, b'_{n-1}]\ \ \text{for some}\ d_i\in |M|\\&\text{iff}\ N\vDash \exists v_i\ (\underline{M}(v_i)\wedge \phi^{\underline{M}}) [\vec{b'}]\\&\text{iff}\ N\vDash (\exists_i(\phi))^{\underline{M}} [\vec{b'}]. \end{align*} $$

That is to say, the collection of maps $(e_n : D_{n}(M)\rightarrow D_{n}(N))_{n\in \mathbb {N}}$ defines a simplicial map. Now, one easily checks that $(e_n r_n)(\phi ^N) = \phi ^M$ and that $(r_n e_n)(\phi ^M) = \phi ^M$ for every $\phi \in F_n$ :

$$\begin{align*}(e_nr_n)(\phi ^N)& = e_n(\{\vec {a}\in |M|^{n+1} : N\vDash \phi [\vec {a}]\}) = e_n(\phi ^M) = (\phi ^{\underline {M}})^N\\&= \{\vec {b}\in |N|^{n+1} : N\vDash \phi ^{\underline {M}} [\vec {b}]\}= \{\vec {a}\in |M|^{n+1} : N\vDash \phi ^{\underline {M}} [\vec {a}]\}= \phi ^M, \\(r_ne_n)(\phi ^M) &= r_n((\phi ^{\underline {M}})^N) = \{\vec {a}\in |M|^{n+1} : N\vDash \phi ^{\underline {M}} [\vec {a}]\} = \phi ^M.\end{align*}$$

Consequently, $r_* : N_*\rightarrow M_*$ defines a retraction of $N_*$ over $M_*$ . Conversely, the very condition $r_* e_* = \text {id}_{M_*}$ supposes that $e_*$ is well defined, and thus that M is a definable elementary substructure of N. As a matter of fact, there must be some L-formula $\chi (v_0)$ such that $e_0(|M|) = e_0((v_0 = v_0)^M) = \chi (v_0)^N$ .⊣

Proof Given any type $q\in S_n(T)$ , there is a type $p\in S_{n+1}(T)$ such that $p\supseteq \{E_i(\psi ) : \psi \in q\}$ . Indeed, since every finite subset of q is consistent and realized in some model of T, this is obviously the case of $\{E_i(\psi ) : \psi \in q\}$ too. But then $\exists _ip\supseteq \{(\exists _iE_i)(\psi ) : \psi \in q\} = q$ . Since q is supposed to be complete, it follows that $\exists _ip = q$ . (However, all the L-formulae in q are not in an existentially quantified form: they are only so up to graded logical equivalence —see Definition 1.3.) As to the simplicial identities, they are verified by straightforward extension from L-formulae to types. ⊣

Proof In combinatorial terms, one has to show, given n simplices $p_0$ , …, $\widehat {p_k}$ , …, $p_n\in S_{n-1}(T)$ such that $\exists _ip_j = \exists _{j-1}p_i$ for all $i, j\neq k$ with $i<j$ , the existence of $p\in S_n(T)$ such that $\exists _i p = p_i$ for all $i\neq k$ . But the complete ( $n+1$ )-type p generated by the family $\{(v_j = v_j\ \wedge \ \phi ^j(v_0, \ldots , v_{j-1}, v_{j+1}, \ldots , v_n)) : \phi ^j\in p_j,\ j\neq k\}$ matches that condition. A preliminary remark is in order: the hypothesis $\exists _ip_j = \exists _{j-1}p_i$ (for $i<j$ and $i,j\neq k$ ) means that, for any L-formula $\phi ^j(v_0, \ldots , v_{n-1})\in p_j$ , there exists an L-formula $\psi _{\phi }^i(v_0, \ldots , v_{n-1})\in p_i$ such that $\exists x \phi ^j(v_0, \ldots , v_{i-1}, x, v_{i}, \ldots , v_{n-2})$ is logically equivalent (in the graded sense) with $\exists x \psi _{\phi }^i(v_0, \ldots , v_{j-2}, x, v_{j-1}, \ldots , v_{n-2})$ . Renaming ‘ $v_{j-1}$ ’, …, ‘ $v_{n-2}$ ’ is immaterial, so actually, for any variable symbols ‘ $u_1$ ’, …, ‘ $u_{n-1}$ ’:

$$\begin{align*}&\exists x \phi ^j(u_1, \ldots , u_{i}, x, u_{i+1}, \ldots , u_{j-1}, \ldots , u_{n-1})\\&= \exists x \psi _{\phi }^i(u_1, \ldots , u_{j-1}, x, u_{j}, \ldots , u_{n-1}).\end{align*}$$

In the same way, for any L-formula $\phi ^i\in p_i$ , there exists an L-formula $\chi _{\phi }^j\in p_j$ such that:

$$\begin{align*}& \exists x \phi ^i(u_1, \ldots , u_{j-1}, x, u_{j}, \ldots , u_{n-1})\\&=\exists x \chi _{\phi }^j(u_1, \ldots , u_{i}, x, u_{i+1}, \ldots , u_{j-1}, \ldots , u_{n-1}).\end{align*}$$

As a consequence, for any $\phi ^j\in p_j$ with $j>0$ and $j\neq k$ :

$$ \begin{align*} & \exists_0((v_j = v_j \wedge \phi^j(v_0, \ldots, v_{j-1}, v_{j+1}, \ldots, v_n)))\\ &= (v_{j-1} = v_{j-1} \wedge \exists x\phi^j(x, v_0, \ldots, v_{j-2}, v_{j}, \ldots, v_{n-1}))\\ &= (v_{j-1} = v_{j-1} \wedge (\exists x\phi^j)[v_j/v_{j-1}, \ldots, v_{n-1}/v_{n-2}])\\ &= (v_{j-1} = v_{j-1} \wedge (\exists x\psi_{\phi}^0)[v_j/v_{j-1}, \ldots, v_{n-1}/v_{n-2}])\\ &= (v_{j-1} = v_{j-1} \wedge \exists x\psi_{\phi}^0(v_0, \ldots, v_{j-2}, x, v_{j}, \ldots, v_{n-1})). \end{align*} $$

But the latter L-formula is obviously a member of $p_0$ . As to the case $j=0$ (supposing $k\neq 0$ ), $\exists _0((v_0 = v_0 \wedge \phi ^0(v_1, \ldots , v_n))) = \phi ^0(v_0, \ldots , v_{n-1})\in p_0$ . Gathering both cases ( $j>0$ and $j=0$ ), one has that $\exists _0p = p_0$ (for $k\neq 0$ ).

Let us prove now that $\exists _n p = p_n$ (for $k\neq n$ ). As above, for any $\phi ^i\in p_i$ with $i<n$ and $i\neq k$ :

$$ \begin{align*} & \exists_n((v_i = v_i \wedge \phi^i(v_0, \ldots, v_{i-1}, v_{i+1}, \ldots, v_n)))\\ &= (v_{i} = v_{i} \wedge \exists x\phi^i(v_0, \ldots, v_{i-1}, v_{i+1}, \ldots, v_{n-1}, x))\\ &= (v_{i} = v_{i} \wedge (\exists_{n-1}\phi^i)[v_{i+1}/v_{i}, \ldots, v_{n-1}/v_{n-2}])\\ &= (v_{i} = v_{i} \wedge (\exists_{i}\chi_{\phi}^n)[v_{i+1}/v_{i}, \ldots, v_{n-1}/v_{n-2}])\\ &= (v_{i} = v_{i} \wedge \exists x\chi_{\phi}^n(v_0, \ldots, v_{i-1}, x, v_{i+1}, \ldots, v_{n-1}))\in p_n. \end{align*} $$

As to the case $i = n$ , again $\exists _n((v_n = v_n \wedge \phi ^n(v_0, \ldots , v_{n-1}))) = \phi ^n(v_0, \ldots , v_{n-1})\in p_n$ . So $\exists _n p = p_n$ (for $k\neq n$ ). The proof of the other identities $\exists _jp = p_j$ , for all j such that $0<j<n$ and $j\neq k$ , is analogous. ⊣

Proof Let $p\in S_0(M)$ be definable: for each L-formula $\phi (v_0, \ldots , v_n)$ , there is an L-formula $d^{p, n}_i(\phi )(v_0, \ldots , v_{n-1})$ , possibly with parameters in M, such that, for any $(a_0, \ldots , a_{n-1})\in |M|^n$ , $\phi (\overline {a_0}, \ldots , \overline {a_{i-1}}, v_0, \overline {a_i}, \ldots , \overline {a_{n-1}})\in p$ iff $M\vDash d^{p, n}_i(\phi ) [a_0, \ldots , a_{n-1}]$ . One has: $d^{p, n}_i(\neg \phi ) = \neg d^{p, n}_i(\phi )$ and $d^{p, n}_i(\phi \wedge \psi ) = d^{p, n}_i(\phi )\wedge d^{p, n}_i(\psi )$ . Besides, each set $F_n$ can be turned into a group, with $\nleftrightarrow $ as the binary law, so each $d^{p, n}_i$ is actually a group homomorphism. Hence $F_*^p := \langle \langle F_n, \nleftrightarrow , \bot \rangle , (d^{p, n}_i)_{0\leq i\leq n}, (s^n_j)_{0\leq j\leq n}\rangle _{n\in \mathbb {N}}$ is a simplicial group. Since, according to Moore’s theorem,Footnote ⁷ the underlying simplicial set of a simplicial group is fibrant, one concludes that $F_*^p$ is fibrant. ⊣

Proof From $\partial ^{p, n}(\phi ) := (((d^{p, n}_0(\phi )\nleftrightarrow d^{p, n}_1(\phi ))\nleftrightarrow \cdots )\nleftrightarrow d^{p, n}_n(\phi ))$ (for each $n\in \mathbb {N}$ and each $\phi \in F_n$ ), one gets a differentiation operator $\partial ^{p, \ast }$ : $\partial ^{p, n+1}\circ \partial ^{p, n}\equiv \bot $ for every $n\in \mathbb {N}$ . In other words, $\langle F^p_*, \partial ^{p, \ast }\rangle $ is a chain complex. ⊣

Proof Let us define a complex of M as a finite collection C of definable subsets of M (i.e., of definable subsets of Cartesian powers of $|M|$ ) which is closed under the face operator: for any definable subset $(\phi (v_0, \ldots , v_n, \overline {a_1}, \ldots , \overline {a_l}))^M\in D_n(M)$ (with parameters $a_1, \ldots , a_l$ ), $\phi ^M\in C$ implies both

• • $\exists _i^M(\phi ^M) = (\exists x\phi (v_0, \ldots , v_{i-1}, x, v_i, \ldots , v_{n-1}, \overline {a_1}, \ldots , \overline {a_l}))^M\in C$ and

• • $(\exists y\phi (v_0, \ldots , v_n, \overline {a_1}, \ldots , \overline {a_{j-1}}, y, \overline {a_{j+1}}, \ldots , \overline {a_l}))^M\in C$ ,

for any i with $0\leq i\leq n$ and any j with $1\leq j\leq l$ . A complex C of M is of dimension n if n is the largest integer k such that $D_k(M)\cap C\neq \emptyset $ . Given a collection $\Gamma $ of definable subsets of M, the complex generated by $\Gamma $ , written $\Gamma ^c$ , is the intersection of all complexes of M containing all members of $\Gamma $ . A complex generated by a single definable subset is called a principal complex. For each $n\in \mathbb {N}$ , the set of n-simplices of $M^*$ is defined as the set $K(M)_n$ of all complexes of M of dimension n. The maps $\exists ^{M}_i : D_n(M)\rightarrow D_{n-1}(M)$ and $E_j^{M} : D_n(M)\rightarrow D_{n+1}(M)$ , as defined earlier, are simply extended to collections of parametrically definable subsets. (Note that, given any definable subset $\phi ^M$ of M, $\exists _i(\{\phi ^M\}^c) = \{\exists _i(\phi ^M)\}^c$ and $E_j(\{\phi ^M\}^c) = \{E_j(\phi ^M)\}^c$ , so that $F_*^M$ can be identified with a simplicial subset of $M^*$ .) The distinguished n-simplices of $M^*$ are the principal complexes of M generated by a nonempty subset of $|M|^{n+1}$ defined by an atomic formula without parameters. Their set is written $K(M)^{\prime}_n$ .⊣

Proof Since f is an elementary embedding, $f^*$ obviously satisfies ${{\hspace {-0.0001pt}}}^0f(K_0(N))\subseteq K_0(M)$ , so it only remains to prove the second condition (ii) in the definition above. For the sake of simplicity, let us consider only the case $n = 1$ and let us suppose that the given simplices are principal complexes. The treatment of the general case is analogous, only more complicated. So, using ‘ $\alpha $ ’, ‘ $\beta $ ’ and ‘ $\gamma $ ’ to indicate arbitrary sequences of parameters, let $x_0 = \{(\phi _0(v_0, \overline {f(a_{\alpha })}, \overline {b_{\alpha }}))^N\}^c$ , $x_1 = \{(\phi _1(v_0, \overline {f(a_{\beta })}, \overline {b_{\beta }}))^N\}^c$ and $y = \{(\psi (v_0, v_1, \overline {c_{\gamma }}))^M\}^c$ be such that:

• • $M\vDash \exists x\phi _0(x, \overline {f(a_{\alpha })}, \overline {b_{\alpha }})\leftrightarrow \exists x\phi _1(x, \overline {f(a_{\beta })}, \overline {b_{\beta }})$ ,

• • $M\vDash \exists y\psi (y, v_0, \overline {c_{\gamma }})\leftrightarrow \exists x_{\alpha }\phi _0(v_0, \overline {a_{\alpha }}, x_{\alpha })$ ,

• • $M\vDash \exists z\psi (v_0, z, \overline {c_{\gamma }})\leftrightarrow \exists x_{\beta }\phi _1(v_0, \overline {a_{\beta }}, x_{\beta })$ .

Let x be $\{(\psi (v_0, v_1, \overline {f(c_{\gamma })}))^N, (\phi _0(v_1, \overline {f(a_{\alpha })}, \overline {b_{\alpha }}))^N, (\phi _1(v_0, \overline {f(a_{\beta })}, \overline {b_{\beta }}))^N\}^c$ . One has:

• • $p_n(x) = \{(\psi (v_0, v_1, \overline {c_{\gamma }}))^M, (\exists x_{\alpha }\phi _0(v_1, \overline {a_{\alpha }}, x_{\alpha }))^M, (\exists x_{\beta }\phi _1(v_0, \overline {a_{\beta }}, x_{\beta }))^M\}^c = \{(\psi (v_0, v_1, \overline {c_{\gamma }}))^M, (\exists y\psi (y, v_1, \overline {c_{\gamma }}))^M, (\exists z\psi (v_0, z, \overline {c_{\gamma }}))^M\}^c = y$

• • $\exists _0x = \{(\exists x\psi (x, v_0, \overline {f(c_{\gamma })}))^N, (\phi _0(v_0, \overline {f(a_{\alpha })}, \overline {b_{\alpha }}))^N, (\exists x\phi _1(x, \overline {f(a_{\beta })}, \overline {b_{\beta }}))^N\}^c = \{(\exists x_{\alpha }\phi _0(v_0, \overline {a_{\alpha }}, x_{\alpha }))^N, (\phi _0(v_0, \overline {f(a_{\alpha })}, \overline {b_{\alpha }}))^N, (\exists x\phi _0(x, \overline {f(a_{\alpha })}, \overline {b_{\alpha }}))^N\}^c = x_0$

• • $\exists _1x = x_1$ in the same way as just above.⊣

Proof The linear ordering of every $X_n$ is defined by induction. Let us suppose that a linear order $<_n$ has been defined on $X_n$ . For each $E\in X_{n+1}$ , let $s(E)$ be the sequence $(d_i(E))_{0\leq i\leq n+1}$ . An order $<_{n+1}$ is then defined on $X_{n+1}$ as follows: $E <_{n+1} E'$ iff $s(E) <^l_n s(E')$ , where $<^l_n$ is the lexicographic order induced by $<_n$ . Since the lexicographical order on a family of linearly ordered sets is a linear extension of their product order, by induction each $<_n$ is a linear order. ⊣

Proof Since $M^*$ is a d-simplicial set, it is only necessary to define a dense linear ordering of $D_0(M)$ . Each definable subset A of $|M|$ can be written $\bigcup _{i = 0}^{n_A} \overline {]}a_i, a_{i+1}\overline {[}$ for some $n_A\in \mathbb {N}$ , with $a_i\leq ^M a_{i+1}$ and the convention:

$$\begin{align*}\overline {]}a_i, a_{i+1}\overline {[} =\begin {cases} ]a_i, a_{i+1}[\ \ \text {if}\ a_i<^M a_{i+1},\\ \{a_i\}\ \ \text {if}\ a_i = a_{i+1}.\end {cases}\end{align*}$$

The sequence $(a_i)_{0\leq i\leq n_A}$ is called the sequence associated to A and written $\sigma (A)$ . Then $D_0(M)$ is ordered as follows: $A <^0 A'$ iff $\sigma (A) <^l \sigma (A')$ , where $<^l$ is the lexicographic order induced by $<^M$ . Finally $K(M)_0$ is ordered as follows: $C<_0 C'$ iff $C_0<^* {C^{\prime }}_0$ , where $C_0 = C\cap D_0(M)$ , ${C^{\prime }}_0 = C^{\prime }\cap D_0(M)$ and $<^*$ is the lexicographic order induced by $< ^0$ on $\wp _f(D_0(M))$ . The resulting ordering $<_0$ is a dense linear order. ⊣

Proof For each $n\in \mathbb {N}$ , the equality ${{\hspace {-0.0001pt}}}^nf\circ {{\hspace {-0.0001pt}}}_nf = \text {id}_{D_n(M)}$ and thus the equality ${{\hspace {-0.0001pt}}}^nf\circ {{\hspace {-0.0001pt}}}_nf = \text {id}_{K(M)_n}$ follow directly from the definitions of ${{\hspace {-0.0001pt}}}_nf$ and ${{\hspace {-0.0001pt}}}^nf$ . The uniqueness of $f_!$ follows from the hypothesis that f is an elementary embedding. ⊣

Proof Suppose $(y_1, \ldots , y_n)\in (R^{(n)}_k)^{\widehat {Y}} = (||Y||_n^k)^n$ . Each $y_i$ is of the form $\overline {(\beta _i, u_i)}$ with $\beta _i = Y_n^k$ . By definition of a dilo-simplicial map, $p_n\circ (i_p)_n = \text {id}_{Y_n}$ and thus $\widehat {p}(y_i) = \overline {(\alpha _i, u_i)}$ with $\alpha _i = (i_p)_n(\beta _i) = p_n^{-1}(\beta _i) = X_n^k$ , so $\widehat {p}(y_i)\in ||X||_n^k$ , and so $(\widehat {p}(y_1), \ldots , \widehat {p}(y_n))\in (R^{(n)}_k)^{\widehat {X}}$ . Suppose now that $||Y||\subseteq ||X||$ and that $\widehat {X}\vDash \phi (v_0, \overline {y_1}, \ldots , \overline {y_n}) [x]$ with $x\in ||X||$ and $y_1, \ldots , y_n\in ||Y||$ . Let C be $(\phi (v_0, \overline {y_1}, \ldots , \overline {y_n}))^{\widehat {X}}$ , so that $x\in C$ , and let $p'$ be the restriction of $||p||$ to C. Since $p'\circ x$ is a cellular inclusion and p is a trivial fibration, $||p||$ has the right lifting property w.r.t. $p'\circ x$ , so there exists a lifting h in the following diagram:

The map h satisfies $h\circ p'\circ x = i\circ x$ and $||p||\circ h = \text {id}_{||Y||}$ . The first condition ensures that there exists $y\in |\widehat {Y}|$ such that $h(y)\in C$ and, by the uniqueness of the section of p, the second ensures that $h(y) = y$ . This leads to the existence of $y\in |\widehat {Y}|$ such that $\widehat {X}\vDash \phi (v_0, \overline {y_1}, \ldots , \overline {y_n}) [y]$ . As a result, the Tarski–Vaught test is verified. ⊣

Proof The combination of Lemma 12.16 and Theorem 12.18 in [Reference Poizat10] shows that the proof can be confined to L-formulae $\phi (\vec {x}, \vec {y})$ where $|\vec {x}| = |\vec {y}| = 1$ . Now, an indiscernible sequence of elements in $\widehat {X}$ is any sequence of elements of some $||X_n^k||\setminus \bigcup _{0\leq i\leq n} ||d_i(X_n^k)||$ . So an element $b\in |\widehat {X}|$ can make a difference within an indiscernible sequence $(a_i)_{i\in I}$ only if $b = a_{i_0}$ for some $i_0\in I$ , so $I_0$ can be taken to be $\{i\in I : i>i_0\}$ . ⊣

Proof The set $\{(n, x, u) : n\in \mathbb {N}, x\in X_n, u\in ||\Delta ^n||\}$ can be naturally equipped with a linear order: for $n, n'\in \mathbb {N}$ , $x\in X_n$ , $x'\in X_{n^{\prime }}$ , $u = (t_0, \ldots , t_n)\in ||\Delta ^n||$ and $u^{\prime } = \{(t^{\prime}_0, \ldots , t^{\prime}_{n^{\prime }})\in ||\Delta ^{n^{\prime }}||$ , one states:

$$\begin{align*}(n, x, u)\prec (n', x', u')\quad \hbox{iff}\quad\begin{cases}n < n',\\\text{or}\ \ n = n'\ \text{and}\ x < x'\ \text{in}\ X_n,\\\text{or}\ \ n = n',\ x = x'\ \text{and}\ u < u'\ \text{in}\ ||\Delta ^n||,\end {cases}\end{align*}$$

$||\Delta ^n||$ being endowed with the lexicographical order.

Then, given $[x, u] := \text {inf}_{\prec }(\{(n_0, x_0, u_0) : x_0\in X_{n_0}$ and $(x_0, u_0)\in \overline {(x, u)}\})$ , $|\widehat {X}| = ||X||$ is simply ordered by:

$$\begin{align*}\overline {(x, u)} <_X \overline {(x', u')}\quad\hbox{iff}\quad [x, u]\prec [x', u'].\end{align*}$$

One checks that $<_X$ is a dense linear order which turns $\widehat {X}$ into an o-minimal structure. Indeed, because the interpretation $(R^{(1)}_k)^{\widehat {X}}$ of each predicate is a convex set, the structure $\langle \widehat {X}, <_X, (R^{(1)}_k)^{\widehat {X}}\rangle $ is weakly o-minimal, by a result given in [Reference Baisalov and Poizat1], and actually o-minimal, by construction of $<_X$ . Moreover, the n-ary relations for $n\geq 2$ are interpreted by trivial convex subsets (products), so instantiating a variable in an L-formula or quantifying over it simply shifts to another convex subset, and actually to a finite union of singletons and intervals. The same is true about connectives, so any L-formula in $F_0$ is interpreted in $\widehat {X}$ by a finite union of singletons and intervals.⊣

Proof For any vertex x of X, let us consider its realization $\{||x||\} := \{\overline {(x, 0)}\} = \{x\}\times ||\Delta _0||\subseteq ||X||$ , so that the set $X_0$ of the vertices of X corresponds to a subset of $||X||$ . In the same way, each $1$ -simplex $x\in X_1$ corresponds to an ordered pair of vertices, and thus $X_1$ to a binary relation on $||X||$ . More generally, each $x\in X_n$ corresponds to an $(n+1)$ -uple $(x_0, \ldots , x_n)$ of vertices (some of which possibly identical), hence to an $(n+1)$ -uple $(||x_0||, \ldots , ||x_n||)$ in $||X||$ . The substructure $Y = \langle ||X_0||, (R_k^{(n)})^{\widehat {X}}\cap ||X_0||^n\rangle _{k, n\in \mathbb {N}}$ of $\widehat {X}$ defined by restriction to $||X_0|| = \{||x|| : x\in X_0\}$ is actually an elementary substructure of $\widehat {X}$ because, by continuity, every L-formula (with parameters in Y) satisfiable in $\widehat {X}$ is satisfied by a tuple of vertices. Every definable subset $B\in D_n(Y)$ consists of a set of $(n+1)$ -tuples of vertices. For $C\in K(Y)_n$ , let $\lambda _n(C)$ be $x\in X_n$ if, for each $B\in C\cap D_n(Y)$ and for each $(e_0, e_1, \ldots , e_n)\in B$ , the barycenter of the convex hull of $\{e_0, e_1, \ldots , e_n\}$ belongs to $||x||$ , and x is the least n-simplex of X with that property; else some fixed n-simplex $x_{\star }$ of X. Since both the operations of taking the convex hull and the barycenter commute with the face operators, the maps $\lambda _n : K(Y)_n\rightarrow X_n$ ( $n\in \mathbb {N}$ ) make up a simplicial map $\lambda : Y^*\rightarrow X$ , which is easily seen to be a trivial fibration. The map $\varepsilon : (\widehat {X})^*\rightarrow X$ is then defined as $\lambda \circ r^*$ . Since trivial fibrations are stable under composition, $\varepsilon $ is a trivial fibration too. ⊣

Proof Let $C\in K(M)_0$ be nonprincipal. Without loss of generality one may assume that $C = \{(\phi _1(v_0))^M, (\phi _2(v_0))^M\}^c$ with $(\phi _1(v_0))^M\neq \emptyset $ , $(\phi _2(v_0))^M\neq \emptyset $ and $(\phi _1(v_0))^M\neq (\phi _2(v_0))^M$ . Let $\alpha := \{E_0((\phi _1(v_0))^M), E_1((\phi _2(v_0))^M)\}^c$ and $\beta := \{(\phi _1(v_0)\wedge \phi _2(v_1))^M, (\phi _1(v_1)\wedge \phi _2(v_0))^M\}^c$ . One has: $\exists _0\alpha = \exists _0\beta = \exists _1\alpha = \exists _1\beta = C$ . Let us now suppose that there exists $\gamma \in K(M)_2$ such that $\exists _1\gamma = \alpha $ and $\exists _2\gamma = \beta $ : then $\{(\phi _1(v_0))^M, (\phi _2(v_0))^M\}^c = \{(\phi _1(v_0)\wedge \exists x\phi _2(x))^M, (\exists x\phi _1(x)\wedge \phi _1(v_0))^M\}^c = \exists _1\beta = \exists _1\exists _2\gamma = \exists _1\exists _1\gamma = \exists _1\alpha = \{(\phi _1(v_0))^M\}^c$ , in contradiction with the hypothesis about $(\phi _1(v_0))^M$ and $(\phi _2(v_0))^M$ . ⊣

Proof The more specific statement of the theorem is that, for any objects M of ${\mathbf{oL}\hbox{-}\mathbf{Strs}}$ and X of ${\mathbf{dilo}\hbox{-}\mathbf{sSets}}$ , there is a map $\Phi _{M, X} : \text {Hom}_{{\mathbf {\scriptsize oL-Strs}}}(\widehat {X}, M)\rightarrow \text {Hom}_{{\mathbf {\scriptsize dilo-sSets}}}(M^*, X)$ with a homotopy inverse $\Psi _{M, X}$ satisfying not only $\Phi \circ \Psi \simeq \text {id}_{\textrm {\scriptsize Hom}(M^*, X)}$ and $\Psi \circ \Phi \simeq \text {id}_{\textrm {\scriptsize Hom}(\widehat {X}, M)}$ , but even $\Psi \circ \Phi = \text {id}_{\textrm {\scriptsize Hom}(\widehat {X}, M)}$ . Let $f : \widehat {X}\rightarrow M$ be a given elementary embedding in oL-Strs. Then $p_f : M^*\rightarrow X$ is defined as $\varepsilon \circ f^*$ , where $\varepsilon $ is the trivial fibration of Lemma 3.17. Since $f^*$ is a trivial fibration, so is $p_f$ too. And since $\varepsilon $ clearly preserves distinguished simplices and respects the ordering of n-simplices for each $n\in \mathbb {N}$ , as well as $f^*$ , so does $p_f$ too. Also, $p_f$ is a retraction with a unique section $f_!\circ r_!\circ s$ , where

is the retraction of the previous lemma and $s_n : X_n\rightarrow K(Y)_n$ sends each $x\in X_n$ to $\{(||x_0||, \ldots , ||x_n||)\}^c$ , $x_0, \ldots , x_n$ being the vertices corresponding to x in Lemma 3.17. Conversely, any trivial fibration $p : M^*\rightarrow X$ in dilo-sSets gives rise, for each $x\in |\widehat {X}|$ , to a lifting diagram:

where $\ast $ is (the simplicial set whose realization is) the point and $\{x\}^c$ represents $\{(v_0 = \overline {x})^{\widehat {X}}\}^c\in K(\widehat {X})_0$ . Indeed, since $p_0$ is surjective, there exists $C_x\in K(M)_0$ such that $p_0(C_x) = \varepsilon _0(\{x\}^c)$ . One has: $h_0(\{x\}^c) = C_x = i_p\circ \varepsilon \circ \{x\}^c$ . Because p and $\varepsilon $ are trivial fibrations, and thus weak equivalences, h is a weak equivalence too, i.e., a map between fibrant simplicial sets which induces isomorphisms on all homotopy groups.Footnote ¹⁶ In particular, $h_1 : \pi _1((\widehat {X})^*, \{x\}^c)\simeq \pi _1(M^*, C_x)$ . As a consequence, by Lemma 3.18, $C_x = \{(\phi _x(v_0))^M\}^c$ for some L-formula $\phi _x$ . For $a\in (\phi _x(v_0))^M$ , one has that $(M, a)\vDash \text {Th}(\widehat {X}, \overline {x})$ , a theory which (owing to Pillay and Steinhorn’s result) has a unique prime model $(P, \alpha )$ . Let $e_M : (P, \alpha )\rightarrow (M, a)$ and $e_{\widehat {X}} : (P, \alpha )\rightarrow (\widehat {X}, x)$ two corresponding elementary embeddings. Even though $e_M$ and $e_{\widehat {X}}$ are not unique themselves, $e_M(\alpha ) = a$ and $e_{\widehat {X}}(\alpha ) = x$ are ensured to hold. So a (and thus $C_x$ ) is uniquely determined. Stating $f_p(x) := a$ , one defines $f_p : \widehat {X}\rightarrow M$ . This is an elementary embedding: indeed, $f_p(|\widehat {X}|)\subseteq |M|$ and types of elements are preserved, since the definition of each is preserved by the corresponding h, which can taken to be $i_p\circ \epsilon $ for each $x \in|\widehat{X}|.$

The functoriality of $p\mapsto f_p$ and $f\mapsto p_f$ is clear, so it only remains to check that $p_{f_p}\simeq p$ and that $f_{p_f} = f$ . Let $p : M^*\rightarrow X$ be a given trivial fibration. Then $f_p : \widehat {X}\rightarrow M$ is defined by $\{f_p(x)\}^c = (i_p\circ \epsilon )_0(\{x\}^c)$ , and $p_{f_p}$ as the composite $\varepsilon \circ (f_p)^*$ . By construction of $f_p$ , $h = (f_p)_!$ , so $p_{f_p} = \varepsilon \circ (f_p)^* = p\circ (f_p)_!\circ (f_p)^*$ . And since $(f_p)_!\circ (f_p)^*\simeq \text {id}_{M^*}$ , one gets: $p_{f_p}\simeq p$ . Actually, as $(p_{f_p})_0(\{(v_0 = \overline {f_p(x)})^M\}^c) = (\varepsilon _0\circ {{\hspace {-0.0001pt}}}^0(f_p))(\{(v_0 = \overline {f_p(x)})^M\}^c) = \varepsilon _0(\{(v_0 = \overline {x})^{\widehat {X}}\}^c) = (p_0\circ h_0)(\{(v_0 = \overline {x})^{\widehat {X}}\}^c) = p_0(\{(v_0 = \overline {f_p(x)})^M\}^c)$ , p and $p_{f_p}$ coincide on $h_0(K(\widehat {X})_0)$ ( $\widehat {X}$ and M being o-minimal). The resulting stronger result is written: $p_{f_p}\simeq p\ (\text {rel}\ h_0(K(\widehat {X})_0))$ . On the other hand, let $f : \widehat {X}\rightarrow M$ be a given elementary embedding, and $x\in ||X||$ . By definition, $f_{p_f}(x)$ is the element b of $|M|$ such that $h_0(\{x\}^c) = \{b\}^c$ , where h is the lift of $\varepsilon $ along $p_f$ . Besides, $a := f(x)$ is such that ${{\hspace {-0.0001pt}}}^0f(\{a\}^c) = \{x\}^c$ , so $(p_f)_0(\{a\}^c) = \varepsilon _0(\{x\}^c) = (p_f)_0(h_0(\{x\}^c)) = (p_f)_0(\{b\}^c)$ . As a consequence, ${{\hspace {-0.0001pt}}}^0f(\{a\}^c) = {{\hspace {-0.0001pt}}}^0f(\{f(x)\}^c) = {{\hspace {-0.0001pt}}}^0f(\{b\}^c)$ . Hence $b = a$ , and this holds for each $x\in ||X||$ , so $f_{p_f} = f$ .⊣

Proof For each $\phi \in F_n$ and each L-structure M, let $[\phi ^M]_T = \{\psi ^M : T\vdash \phi \leftrightarrow \psi \}$ . It is straightforward to check that $[\phi ^M]_T\mapsto [(\exists _i\phi )^M]_T$ and $[\phi ^M]_T\mapsto [E_j(\phi ^M)]_T$ are well defined and satisfy the simplicial identities, so that ( $\mathcal{F}_T(M))_n := \{[\phi^M]_T : \phi \in F_n\}\ (n\in\mathbb{N}$ ) defines a simplicial set $\mathcal{F}_T(M)$ . In particular, $\mathcal {F}_T(M) = M_*$ iff $M\vDash T$ . For any elementary embedding $f : M \rightarrow N$ , the definition of $\mathcal{F}_T(f)$ is directly adapted from that of $f_*$ . ⊣