Proof. As \(p\land q \le q\) always holds, adjunction shows \(q\le p\mathop{\parbox{.5cm}{\rightarrowfill}}q\). Taking the meet (\(\land\)) with \(p\) on both sides gives \(p\land q \le p \land (p\mathop{\parbox{.5cm}{\rightarrowfill}}q)\).

Conversely, as \(p\mathop{\parbox{.5cm}{\rightarrowfill}}q \le p\mathop{\parbox{.5cm}{\rightarrowfill}}q\) holds, adjunction gives \(p\land (p\mathop{\parbox{.5cm}{\rightarrowfill}}q) \le q\). Taking the meet with \(p\) on both sides gives \(p\land (p\mathop{\parbox{.5cm}{\rightarrowfill}}q) \le p\land q\) ◻

Proof. If \(p = p \land ( q \leftrightarrow r )\) then \(p\le ( q \leftrightarrow r )\) and, by adjunction (Lemma (1), \(p\land q \le r\) and \(p\land r \le q\). Thus \(p\land q \le p\land r\) and \(p\land r \le p \land q\). Conversely, if \(p \land q = p \land r\) then \(p \land q \le r\) and \(p\land r \le q\), and so by adjunction \(p\le q \mathop{\parbox{.5cm}{\rightarrowfill}}r\) and \(p\le r\mathop{\parbox{.5cm}{\rightarrowfill}}q\). ◻

Proof. (1). By Lemma (3), \(p = p \land ( q \leftrightarrow d )\) holds if and only if \(p \land q = p \land d\) does. However, \(p \land d = p \land (p\mathop{\parbox{.5cm}{\rightarrowfill}}q) = p \land q\) by modus ponens. Thus \(p \land q = p \land d\) always holds.

(2). Similarly, by Lemma (3), \(p = p \land ( p \leftrightarrow d )\) holds if and only if \(p = p\land p = p\land d\) does. However, as in the proof of (1), \(p\land d = p \land (p\mathop{\parbox{.5cm}{\rightarrowfill}}q) = p \land q\), so \(p = p \land ( p \leftrightarrow d )\) holds if and only if \(p = p\land q\), that is, if and only if \(p\le q\). ◻

Proof. Immediate from the definition of \([a=b]_M\). ◻

Proof. By definition we have \[\begin{align} [a=b]_M \land [b=c]_M & = \bigvee \{\hskip 1ptE(b\upharpoonright p) \hskip 2pt:\hskip 2ptp\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\} \\ &\land \bigvee \{\hskip 1ptE(b\upharpoonright q) \hskip 2pt:\hskip 2ptq\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2ptc\upharpoonright q = b\upharpoonright q\hskip 1pt\}. \end{align}\] By distributivity of \(\land\) over \(\bigvee\) twice this gives \[\begin{align} [a=b]_M \land [b=c]_M = & \bigvee \{\hskip 1ptE(b\upharpoonright p) \land E(b\upharpoonright q)\hskip 2pt:\hskip 2pt p,\hskip 2ptq\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2pta\upharpoonright p = b\upharpoonright p \\ & \qquad \quad \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2ptb\upharpoonright q = c\upharpoonright q \hskip 1pt\} \\ = & \bigvee \{\hskip 1ptE(b\upharpoonright p\land q)\hskip 2pt:\hskip 2pt p,\hskip 2ptq\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2pta\upharpoonright p\land q = \\ & \qquad \quad b\upharpoonright p\land q \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2ptb\upharpoonright p\land q = c\upharpoonright p\land q \hskip 1pt\} = [a=c]_M \end{align}\] ◻

Proof. In one direction, suppose \(M\) is extensional and let \(a\), \(b\in |M|\) be such that \(([a=b]_M = Ea = Eb\). By Definition (9) we have \[\begin{align} [a=b]_M = & \bigvee \{\hskip 1ptE(a\upharpoonright p) \hskip 2pt:\hskip 2ptp\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\}\\ = & \bigvee \{\hskip 1ptp \hskip 2pt:\hskip 2ptp\in \Omega \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2ptp \le Ea \hskip 2pt\hskip 2pt\& \hskip 2pt\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\} . \end{align}\]

Define \(D= \{\hskip 1ptp\in \Omega\hskip 2pt:\hskip 2ptp \le Ea \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\}\). Then \([a=b]_M = \bigvee D\). By entensionality we thus have \(a=b\).

Conversely, let \(a\), \(b\in |M|\). By Lemma (5), \([a=b]_M \le Ea\), \(b\). Let \(D\subseteq \Omega\) be such that for all \(p\in D\) we have \(a\upharpoonright p = b\upharpoonright p\) and \(Ea=Eb=\bigvee D\). We thus have \[\begin{align} Ea= Eb =\bigvee D & = \bigvee\{\hskip 1ptp \in D\hskip 2pt:\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\} \\ & \le \bigvee\{\hskip 1ptp \le \bigvee D\hskip 2pt:\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\} = [a=b]_M. \end{align}\] Consequently \([a=b]_M = Ea = Eb\), and so by hypothesis \(a=b\). ◻

Proof. Define \(\upharpoonright^\Omega\) and \(E^\Omega\) by setting \(q \upharpoonright^\Omega p = q \wedge p\) and \(E^\Omega q =q\), for \(p\), \(q\in\Omega\). Then it is immediate to check that \((\Omega,\upharpoonright^\Omega,E^\Omega)\in\mathop{\mathrm{pSh}}({(})\Omega)\) satisfies Definition (7). Furthermore, if \(M \in \mathop{\mathrm{pSh}}({\Omega})\) then, by Definition (7) and Definition (13), \(E^M\) is a presheaf morphism from \(M\) to \((\Omega,\upharpoonright^\Omega,E^\Omega)\). ◻

Proof. If \(p\in \Omega\) and \(a\upharpoonright^M p = b\upharpoonright^M p\) then \(f(a) \upharpoonright^N p = f(a\upharpoonright^M p) = f(b\upharpoonright^M p)=f(b)\upharpoonright^N p\) and \(E^N f(a)\upharpoonright^N p = E^N f(a\upharpoonright^M p) = E^M a\upharpoonright^M p\). So the set over which we take the disjunction in the definition of \([a=b]_M\) is a subset of that over which we take the disjunction to evaluate \([f(a)=f(b)]_N\). ◻

Proof. Suppose \(a \in |M|\) and \(p\in \Omega\). We want to show \(f(a\upharpoonright p)= f(a)\upharpoonright p\). By extensionality, it suffices to show \[[f(a\upharpoonright p)= f(a)\upharpoonright p]_M = E^Nf(a\upharpoonright p) = E^Nf(a)\upharpoonright p.\]

However, \(E^Nf(a)\upharpoonright p = p\land E^Nf(a) = p\land E^Ma = E^Ma\upharpoonright p = E^Nf(a\upharpoonright p)\). Also, \(p\land E^Ma = [a\upharpoonright p = a]_M \le [f(a\upharpoonright p) = f(a)]_N \le E^Nf(a\upharpoonright p) = p\land E^Ma\). ◻

Proof. If \(f\upharpoonright|A|\) is a presheaf monomorphism then for all \(a\), \(b\in A\) and \(p\in\Omega\), \(a\upharpoonright p\), \(b\upharpoonright p\in |A|\) and we have \(f(a\upharpoonright p) = f(b\upharpoonright p)\) if and only if \(a\upharpoonright p=b\upharpoonright p\), so the disjunctions in the definitions of \([a=b]_A\) and \([f(a)=f(b)]_B\) are taken over the same set.

Conversely, suppose \(a\), \(b\in |A|\) and \(f(a)=f(b)\). Then for all \(p\in\Omega\) we have \(f(a\upharpoonright p)= f(a)\upharpoonright p = f(b)\upharpoonright p=f(b\upharpoonright p)\), since \(f\) is a presheaf morphism, and so \([f(a)=f(b)]_B = Ef(a)=Ef(b)\), by the definition of \([.=.]_B\). Moreover, \(Ef(a)=Ef(b)= Ea=Eb\), since \(f\) is a presheaf morphism. Thus, if \([a=b]_A=[f(a)=f(b)]_B\) we have \([a=b]_A = Ea=Eb\), and so \(a=b\) by the extensionality of \(M\). ◻

Proof. For left-to-right, suppose \(b\) is a glueing of \(C\) and \(a\in C\). We have \[[b\upharpoonright Ea = a]_M = Ea \land [b=a]_M = Ea \land Ea = Ea .\] However we also have \(E(b\upharpoonright Ea) = Eb\land Ea = Ea\). Thus, by extensionality, \(b\upharpoonright Ea = a\).

For right-to-left, suppose \(a\in C\) and \(b\upharpoonright Ea = a\). Then \[Ea = E(b\upharpoonright a) = Eb\land Ea = [b\upharpoonright Ea = a]_M = Ea\land [b=a]_M,\] so \(Ea\le [ a=b]_M\). By Lemma (5), we also have \([a=b]_M \le Ea\), and thus have \([a=b]_M = Ea\). ◻

Proof. By the definition of \([.=.]_M\) we have that \([a=b]_M = \bigvee X\) where \(X=\{\hskip 1ptp\le Ea\wedge Eb\hskip 2pt:\hskip 2pta\upharpoonright p = b\upharpoonright p\hskip 1pt\}\). However for each \(i\in I\) we have that \(p_i\le Ea\wedge Eb = Ea = Eb\) and \(a\upharpoonright{p_i}=d_i\upharpoonright p_i = b\upharpoonright p_i\), so \(p_i\in X\). Thus \[Ea=Eb\ge [a=b]_M = \bigvee X \ge \bigvee_{i\in I}p_i = Ea = Eb.\] Hence \(Ea=Eb=[a=b]_M\). By extensionality this gives that \(a=b\) ◻

Proof. In each case \(M\) is amongst the ’\(Q\)’s whose intersections are taken in the definition of \(\lcurvyangle A \rcurvyangle^N\) and \(\lcurvyangle A \rcurvyangle_s^N\) respectively in Definition (22). ◻

Proof. Clearly if \(A\subseteq |Q|\), where \(Q\) is a subsheaf of \(M\), \(a\in A\) and \(p\in \Omega\), then \(a\upharpoonright p \in Q\) by the closure of \(Q\) under restriction. However, if we equip \(P = \{\hskip 1pta\upharpoonright p\hskip 2pt:\hskip 2pta\in A \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptp \in \Omega\hskip 1pt\}\) with the operators \(E^P\) and \(\upharpoonright^P\) given by \(E^Pa\upharpoonright p = E^Ma \land p\) and \((a\upharpoonright p) \upharpoonright^P q= a \upharpoonright p\land q\), then \((P,E^P,\upharpoonright^P)\) is a subpresheaf of \(M\) with \(A\subseteq P\). Thus \(P=\lcurvyangle A \rcurvyangle\).

If \(M\) is a sheaf and \(Q\) is a subsheaf of \(M\) with \(A\subseteq |Q|\) then since \(Q\) is a subpresheaf of \(M\) we have \(|\lcurvyangle A \rcurvyangle|\subseteq |Q|\) and the glueing of every compatible set of elements of \(\lcurvyangle A \rcurvyangle\) is an element of \(Q\). However, clearly the set of glueings of a set of compatible elements of \(|\lcurvyangle A \rcurvyangle|\) is closed under further glueings. ◻

Proof. Immediate from the uniqueness of glueings in \(M\). ◻

Proof. For the left-to-right direction, suppose \(a\in A\) and \(\{\hskip 1pt(d_i,p_i)\hskip 2pt:\hskip 2ptd_i\in D\hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptp_i\in \Omega \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pti\in I\hskip 1pt\}\) is such that \(Ea=\bigvee_{i\in I} p_i\) and for all \(i\in I\) we have \(a\upharpoonright p_i = d_i \upharpoonright p_i\). Since for all \(d\in D\) we have \([a=d]_M\le Ea\) (by Lemma (5) we have \(\bigvee \{\hskip 1pt[a=d]_M\hskip 2pt:\hskip 2ptd \in D\hskip 1pt\}\le Ea\).

However, for \(i\in I\), since \(a\upharpoonright pi = d_i\upharpoonright p_i\) and \(Ea = \bigvee \{\hskip 1ptp_i\hskip 2pt:\hskip 2pti\in I\hskip 1pt\}\), we also have \[p_i\land [a = d_i]_M = [a\upharpoonright p_i=d_i\upharpoonright p_i]_M = p_i\land Ea = p_i\land Ed_i = p_i .\] Thus for every \(i\in I\) we have \(p_i\le [a=d_i]_M\) and hence \[Ea = \bigvee\{\hskip 1ptp_i\hskip 2pt:\hskip 2pti\in I\hskip 1pt\} \le \bigvee\{\hskip 1pt[a=d_i]_M\hskip 2pt:\hskip 2pti\in I\hskip 1pt\} \le \bigvee \{\hskip 1pt[a=d_i]_M\hskip 2pt:\hskip 2ptd\in D\hskip 1pt\}.\]

Thus we must have \(Ea = \bigvee \{\hskip 1pt[a=d]_M\hskip 2pt:\hskip 2ptd\in D\hskip 1pt\}\) as claimed.

For the right-to-left direction, if \(a\in D\) and \(Ea = \bigvee \{\hskip 1pt[a=d])M\hskip 2pt:\hskip 2ptd\in D\hskip 1pt\}\), then simply enumerate \(D\) as \(\{\hskip 1ptd_i\hskip 2pt:\hskip 2pti\in I\hskip 1pt\}\) and for \(i\in I\) set \(p_i\) to be \([a=d_i]_M\). Then the family \(S= \{\hskip 1pt(d_i,p_i)\hskip 2pt:\hskip 2pti \in I\hskip 1pt\}\) is as required. ◻

Proof. Immediate from Lemma (17) and the definition of dense. ◻

Proof. This is immediate from Lemma (13). For each \(a\in M\) and \(\{\hskip 1pt(d_i,p_i)\hskip 2pt:\hskip 2ptd_i\in D\hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptp_i\in \Omega \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pti\in I\hskip 1pt\}\) such that \(Ea=\bigvee_{i\in I} p_i\) and for all \(i\in I\) we have \(a\upharpoonright p_i = d_i \upharpoonright p_i\), let \(D_a=\{\hskip 1ptd_i\hskip 2pt:\hskip 2pti\in I\hskip 1pt\}\) and define \(p^a:D\longrightarrow \Omega\) by \(p^a(d) = p_i\) if \(d\in D_a\) and \(d=d_i\) and \(p^a(d)=\bot\) otherwise. Then \(Ea=\bigvee_{d\in D} p^a(d)\) and for all \(d\in D\) we have \(a\upharpoonright p^a(d) = d\upharpoonright p^a(d)\). Lemma (13) shows that \(p^a=p^b\) implies \(a=b\), so the function \(p^{.}:M\longrightarrow {{^D}\Omega}\) is injective. ◻

Proof. We do the simplest thing possible: take the amalgamation of the underlying sets and impose the obvious restriction and extent functions by carrying over those from \(M_0\) and \(M_1\). We give the easy, but somewhat lengthy, details as we did not see them elsewhere in the literature.

Let \(|P|=\{\hskip 1pt(a,i)_{/{\sim}}\hskip 2pt:\hskip 2pti\in \{\hskip 1pt0,1\hskip 1pt\} \hskip 2pt\hskip 2pt\;\&\hskip 2pt\hskip 2pta \in |M_i|\hskip 1pt\}\) where \((a,i)\sim (b,j)\) if and only if \((a,i)=(b,j)\) or \(i\ne j\) and there is some \(c\in A\) such that \(a=f_i(c)\) and \(b=f_j(c)\).

For \((a,i)_{/{\sim}} \in |P|\) set \(E^P (a,i)_{/{\sim}} =E^{M_i} a\). This is a good definition, since if \(c\in A\) we have, since \(f_0\) and \(f_1\) are morphisms, that \(E^{M_0} f_0(c) = E^A a = E^{M_1} f_1(c)\).

For \((a,i)_{/{\sim}} \in |P|\) and \(p\in \Omega\) set \((a,i)_{/{\sim}} \upharpoonright^P p = (a \upharpoonright^{M_i} p,i)_{/{\sim}}\). If \(a\in |A|\) and \(p\in \Omega\) then since \(A\) is a presheaf we have \(a\upharpoonright^A p\in |A|\). Since \(f_0\) and \(f_1\) are morphisms we have, for each \(i\in \{\hskip 1pt0,1\hskip 1pt\}\), that \(f_i(a)\upharpoonright p =f_i(a\upharpoonright p)\). Consequently,\[\begin{gather} (f_0(a),0)_{/{\sim}} \upharpoonright^{P} p = (f_0(a)\upharpoonright^{M_0} p,0)_{/{\sim}} = (f_0(a\upharpoonright^A p),0)_{/{\sim}} = \\ (f_1(a\upharpoonright^A p),1)_{/{\sim}} = (f_1(a)\upharpoonright^{M_1} p,1)_{/{\sim}} = (f_1(a),1)_{/{\sim}} \upharpoonright^{P} p , \end{gather}\] and we have shown that \(\upharpoonright^P\) is well defined.

We have to check \(E^P\) and \(\upharpoonright^P\) satisfy the three presheaf-defining properties. Let \((a,i)_{/{\sim}} \in |P|\).

First of all, if \(p\in \Omega\) we have \(E^P((a,i)\upharpoonright p) = E^{M_i}(a\upharpoonright p) = E^{M_i} a\wedge p = {E^P (a,i)_{/{\sim}}} \wedge p\), where the second equality holds because \(M_i\) is a presheaf and the third by the definition of \(E^P\).

We also have \((a,i)_{/{\sim}} \upharpoonright E^P (a,i)_{/{\sim}} = (a \upharpoonright^{M_i} E^{M_i} a,i)_{/{\sim}} = (a,i)_{/{\sim}}\), where the first equality holds by the definition of \(E^P\) and the second holds since \(M_i\) is a sheaf and hence \(a \upharpoonright^{M_i} E^{M_i} a = a\).

Thirdly, if \(p\), \(q\in \Omega\) then \[\begin{gather} ((a,i)_{/{\sim}} \upharpoonright^P p)\upharpoonright^P q = ((a \upharpoonright^{M_i} p,i)_{/{\sim}} )\upharpoonright^P q = ((a \upharpoonright^{M_i} p)\upharpoonright^{M_i} q,i)_{/{\sim}} = \\ ((a \upharpoonright^{M_i} p\wedge q,i)_{/{\sim}} = ((a,i)_{/{\sim}}) \upharpoonright^P p\wedge q . \end{gather}\]

For \(i\in \{\hskip 1pt0,1\hskip 1pt\}\) and \(a\in |M_i|\) set \(g_i(a) = (a,i)_{/{\sim}}\).

We also have to check for \(i\in \{\hskip 1pt0,1\hskip 1pt\}\) that \(g_i\) is a monomorphism. However, if \(a\in |M_i|\) and \(p\in \Omega\) then \(E^P g_i(a) = E^P (a,i)_{/{\sim}} = E^{M_i} a\) by the definition of \(E^P\), and \(g_i(a \upharpoonright^{M_i} p)= (a\upharpoonright^{M_i} p,i)_{/{\sim}} = (a,i)_{/{\sim}} \upharpoonright^P p = g_i(a) \upharpoonright^P p\). Furthermore, if \(a\), \(b\in |M_i|\) and \((a,i)\sim (b,i)\) then \(a=b\).

The commuativity property holds since if \(a\in |A|\) then \[g_0\cdot f_0(a) = (f_0(a),0)_{/{\sim}} = (f_1(a),1)_{/{\sim}} = g_1\cdot f_1(a).\]

Finally, if \(M_0\) and \(M_1\) are sheaves one can simply sheafify the resultant presheaf \(P\) to obtain a sheaf \(S\) with a sheafification presheaf morphism \(P\xlongrightarrow{c} S\) and for \(i\in\{\hskip 1pt0,1\hskip 1pt\}\) take \(h_i = c\cdot g_i\). ◻

Proof. We have \(h(\bar{a}\upharpoonright E\bar{a}) \land \bigwedge_{j<n} [a_j = a_j\upharpoonright E\bar{a}]_M = h(\bar{a}) \land \bigwedge_{j<n} [a_j = a_j\upharpoonright E\bar{a}]_M\). Recall that for any \(b\in |M|\) and \(p\in \Omega\) we have \([b=(b\upharpoonright p)]_M = p\wedge [b=b]_M = p\land Eb\). Thus \[\begin{align} h(\bar{a}\upharpoonright E\bar{a}) & = h(\bar{a}\upharpoonright E\bar{a}) \land \bigwedge_{j<n} (E (a_j) \wedge E\bar{a}) = h(\bar{a}\upharpoonright E\bar{a}) \land \bigwedge_{j<n} [a_j = a_j\upharpoonright E\bar{a}]_M \\ & = h(\bar{a}) \land \bigwedge_{j<n} [a_j = a_j\upharpoonright E\bar{a}]_M = h(\bar{a}) \land \bigwedge_{j<n} (E (a_j) \wedge E\bar{a}) \\ & = h(\bar{a}) \land E\bar{a} = h(\bar{a}). \end{align}\] ◻

Proof. It suffices to prove the lemma when \(\langle\hskip 1ptp_1,\dots,p_{n-1}\hskip 1pt\rangle = \langle\hskip 1ptEa_1,\dots,Ea_{n-1}\hskip 1pt\rangle\) and use induction to prove the lemma in the generality stated. Let \(\bar{b} = a_0\upharpoonright p_0 \kern-.25pt\raise 4pt\frown\kern-.25pt\langle\hskip 1pta_1,\dots,a_{n-1}\hskip 1pt\rangle\). Then \[h(\bar{a}) \land \bigwedge_{i<n} [a_i = b_i ]_M \le h(\bar{b})\] by the second defining property of being a characteristic function. \[\begin{align} h(\bar{a}) \land p_0 = h(\bar{a}) \land p_0 \land E\bar{a} = & h(\bar{a}) \land \bigwedge_{i<n} [a_i = b_i ]_M = \\ & h(\bar{b}) \land \bigwedge_{i<n} [a_i = b_i ]_M = h(\bar{b}) \land E\bar{b}= h(\bar{b}). \end{align}\] ◻

Proof. For any \(L\)-structure \(M\) in \(\mathop{\mathrm{pSh}}({\Omega})\) with \(d(M)=\kappa\), by Proposition (20), the size of \(M\) is at most \(\vbox{\ialign{##\crcr \cleaders\hrule height.2pt\hfill\crcr\noalign{\kern 1pt\nointerlineskip} \hfil\displaystyle{\vbox{\ialign{##\crcr \cleaders\hrule height.2pt\hfill\crcr\noalign{\kern 1pt\nointerlineskip} \hfil\displaystyle{\Omega}\hfil\crcr}}}\hfil\crcr}}^\kappa\). The possible isomorphism types now depends on the ways of assigning the appropriate structure to the set. This depends on \(L\) and \(\Omega\), but there is some cardinal bound on the number of ways of doing so. ◻

Proof. Immediate, since, by Proposition (20), if \(M\in \mathop{\mathrm{pSh}}({\Omega})\) then \(d(M)<\lambda\) if and only if \(\vbox{\ialign{##\crcr \cleaders\hrule height.2pt\hfill\crcr\noalign{\kern 1pt\nointerlineskip} \hfil\displaystyle{\vbox{\ialign{##\crcr \cleaders\hrule height.2pt\hfill\crcr\noalign{\kern 1pt\nointerlineskip} \hfil\displaystyle{M}\hfil\crcr}}}\hfil\crcr}}<\lambda\). ◻

Proof. This is immediate from the three clause definition for the presheaf morphism \(\tau^M:M^{k(\tau)}\upharpoonright E\tau\longrightarrow M\upharpoonright E\tau\). ◻

Proof. The proof is by induction on the complexity of formulae. We start with atomic formulae. If \(\tau_0\) and \(\tau_1\) are terms and \(\phi\) is the formula \(\tau_0=\tau_1\) and we set \(p=E\tau_0\wedge E\tau_1\) and note that \(p = E(\tau_0 = \tau_1)\) by definition, we have \[\begin{align} & [(\tau_0 = \tau_1)(\bar{a})]_M = [\tau_0^M(\bar{a}\upharpoonright p) = \tau_1^M(\bar{a}\upharpoonright p)]_M = [\tau_0^M(\bar{a})\upharpoonright p = \tau_1^M(\bar{a})\upharpoonright p]_M \\ & \hskip 2pt\hskip 2pt= \bigvee \{\hskip 1ptE(\tau^M_0(\bar{a} \upharpoonright p \wedge q) )\hskip 2pt:\hskip 2ptq\in \Omega \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pt \tau^M_0(\bar{a}) \upharpoonright p \wedge q = \tau^M_1(\bar{a}) \upharpoonright p \wedge q\hskip 1pt\} \\ & \hskip 2pt\hskip 2pt= \bigvee \{\hskip 1ptE\bar{a}\wedge p \wedge q \hskip 2pt:\hskip 2pt \tau^M_0(\bar{a}) \upharpoonright p \wedge q = \tau^M_1(\bar{a}) \upharpoonright p \wedge q\hskip 1pt\} \le E\bar{a},\hskip 2pt\hskip 2ptp \end{align}\]where the final equality holds because the \(\tau_i^M\) are presheaf morphisms.

Similarly, if \(R\) is a relation and \(\tau_0\), …\(\tau_{m-1}\) are terms with \(q = \bigwedge_{i<m} E\tau_i\), \(= E(R(\tau_0,\dots,\tau_{m-1}))\), since \([R(.)]_M\) is a characteristic function we have \[\begin{align} & [R(\tau_0^M(\bar{a}\upharpoonright q),\dots,\tau_{m-1}^M(\bar{a}\upharpoonright q))]_M \le E\bar{a}\upharpoonright q = Ea \wedge q. \end{align}\]

The inductive steps for the binary connectives, negation and universal quantification are all immediate as the required result is explicit in the definition of interpretation of formulae.

Finally, for the inductive step for existential quantification we have \[[\exists x\phi(x, \bar{a})]_M = \bigvee_{t\in |M|} [\phi(t, \bar{a})]_M \le \bigvee_{t\in |M|} Et \wedge E\phi \wedge E\bar{a} \le E\phi \wedge E\bar{a},\] where the first inequality is given by applying the inductive hypothesis to \(\phi\) and \(t\kern-.25pt\raise 4pt\frown\kern-.25pt\bar{a}\). ◻

Proof. Set \(q= [\bar{a} = \bar{b}]_M\) and \(\bar{a} \upharpoonright q\) for \(\langle\hskip 1pta_0 \upharpoonright q, \ldots, a_{n-1} \upharpoonright q\hskip 1pt\rangle\). For all \(i <n\) we have \(a_i \upharpoonright[a_i = b_i]_M = b_i \upharpoonright[a_i = b_i]_M\), so a fortiori we also have \(a_i \upharpoonright q = b_i \upharpoonright q\). Using this fact in the third equality and Lemma (26) in the second equality in the displayed equations following we have \[\begin{align} [\bar{a} = \bar{b}]_M \wedge [ \sigma^M (\bar{a}) = & \tau^M (\bar{a})]_M = [ \sigma^M (\bar{a}) = \tau^M (\bar{a}) \upharpoonright q]_M = \\ & [ \sigma^M (\bar{a}) = \tau^M (\bar{a} \upharpoonright q) ]_M = [ \sigma^M (\bar{b}) = \tau^M (\bar{b} \upharpoonright q) ]_M = \\ & [\bar{a} = \bar{b}]_M \wedge [ \sigma^M (\bar{b}) = \tau^M (\bar{b})]_M . \end{align}\] ◻

Proof. Note, first of all, by Definition (35), we have \(E(\phi\land\psi) = E(\phi\lor \psi) = E\phi \wedge E\psi\). By the definition of interpretation, for \(\diamondsuit \in \{\hskip 1pt\land,\lor\hskip 1pt\}\), and letting \(q = E\phi \wedge E\psi\), we have \[[(\phi \hskip 2pt\diamondsuit\hskip 1pt\psi)(\bar{a})]_M = E\phi\wedge E\psi \wedge E\bar{a} \wedge ( [\phi(\bar{a}_\phi\upharpoonright q )]_M \hskip 2pt\hskip 2pt\diamondsuit\hskip 2pt\hskip 2pt[\psi(\bar{a}_\psi\upharpoonright q )]_M .\] By the definition of forcing we have \([\phi(\bar{a}_\phi)]_M = E\phi\wedge E\bar{a}_\phi\) and \([\psi(\bar{a}_\psi)]_M = E\psi\wedge E\bar{a}_\psi\).

For “\(\lor\)” we have \[\begin{align} [(\phi \hskip 2pt\lor\hskip 1pt\psi)(\bar{a})]_M & = E\phi\wedge E\psi \wedge E\bar{a} \wedge (E\phi\wedge E\bar{a}_\phi \lor E\psi\wedge E\bar{a}_\psi) \\ & = ( E\phi\wedge E\psi \wedge E\bar{a} \wedge (E\phi\wedge E\bar{a}_\phi)) \lor \\ & \qquad\qquad ( E\phi\wedge E\psi \wedge E\bar{a} \wedge (E\psi\wedge E\bar{a}_\psi )) \\ & = ( E\phi\wedge E\psi \wedge E\bar{a} ) \lor ( E\phi\wedge E\psi \wedge E\bar{a} ) \\ & = E\phi\wedge E\psi \wedge E\bar{a} = E(\phi\lor \psi) \wedge E\bar{a} \end{align}\]

Similarly, but more simply, for “\(\land\)” we have \[\begin{align} [(\phi \hskip 2pt\land\hskip 1pt\psi)(\bar{a})]_M & = E\phi\wedge E\psi \wedge E\bar{a} \wedge E\phi\wedge E\bar{a}_\phi \wedge E\psi\wedge E\bar{a}_\psi \\ & = E\phi\wedge E\psi \wedge E\bar{a} = E(\phi\wedge \psi) \wedge E\bar{a} . \end{align}\] ◻

Proof. \(N\Vdash\forall \bar{x}\hskip 2pt\phi(\bar{x},\bar{a})\) if and only if \([\forall \bar{x}\hskip 2pt\phi(\bar{x},\bar{a})]_N = E\phi \land E\bar{a}\), by the definition of \(\Vdash\), where, \(E\phi = \bigwedge\{\hskip 1ptE^{C}c\hskip 2pt:\hskip 2ptc\in C \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptc appears in \phi\hskip 1pt\}\), by Definition (35).

Applying the inductive definition of interpretation of formulae we have \[[\forall \bar{x}\hskip 2pt\phi(\bar{x},\bar{a})]_N = E\phi \wedge E\bar{a}\wedge \bigwedge_{\bar{b}\in |N|^n} (E\bar{b} \longrightarrow [\phi(\bar{b},\bar{a})]_N) .\] Thus \(N\Vdash\forall \bar{x}\hskip 2pt\phi(\bar{x},\bar{a})\) if and only if \(\hskip 2pt\forall\bar{b}\in |N|^n \hskip 2pt(E\phi \wedge E\bar{a} \le E\bar{b} \longrightarrow [\phi(\bar{b},\bar{a})]_N )\). The latter holds if and only if \(\hskip 2pt\forall\bar{b}\in |N|^n \hskip 2pt(E\phi \wedge E\bar{a} \wedge E\bar{b} \le [\phi(\bar{b},\bar{a})]_N )\), by Lemma (1). ◻

Proof. The map given by \(\underaccent{\bar}{a} \mapsto \underaccent{\bar}{a}^{\tilde{N}}\) is a presheaf morphism by the definition of \(\tilde{N}\) being an \(L_M\)-structure, and the map given by \(\underaccent{\bar}{a}^{\tilde{M}} \mapsto \underaccent{\bar}{a}\) is a presheaf isomorphism by Definition (48). By the same definition, for all \(a\in |M|\) we have \(a = \underaccent{\bar}{a}^{\tilde{M}}\). Thus composing the morphisms gives a presheaf morphism from \(M\) to \(N\). ◻

Proof. In each case \(M\) is amongst the ’\(Q\)’s whose intersections are taken in the definition of \(\lcurvyangle A \rcurvyangle^N\) and \(\lcurvyangle A \rcurvyangle_s^N\) respectively in Definition (51). ◻

Proof. Clearly if \(A\subseteq |Q|\), where \(Q\) is an \(L\)-substructure in \(\mathop{\mathrm{pSh}}({\Omega})\) of \(M\), then \(P = \{\hskip 1pt\tau^M(\bar{a}\upharpoonright p)\hskip 2pt:\hskip 2pta\in {^nA} \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptp \in \Omega \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pt\tau is a term\hskip 1pt\} \subseteq |Q|\). Since the \(\tau^M\) are presheaf morphisms for each \(\bar{a}\in {^nA}\), \(p\), \(q\in \Omega\) and term \(\tau\) we have \(\tau^M(\bar{a}\upharpoonright p)\upharpoonright q = \tau^M(\bar{a}\upharpoonright p\land q)\in P\). Moreover, \(P\) is the underlying set of an \(L\)-structure in \(\mathop{\mathrm{pSh}}({\Omega})\). Thus \(P=\lcurvyangle A \rcurvyangle\).

If \(M\) is a sheaf and \(Q\) is a subsheaf of \(M\) with \(A\subseteq |Q|\) then since \(Q\) is a subpresheaf of \(M\) we have \(|\lcurvyangle A \rcurvyangle|\subseteq |Q|\) and the glueing of every compatible set of elements of \(\lcurvyangle A \rcurvyangle\) is an element of \(Q\). However, clearly the set of glueings of a set of compatible elements of \(|\lcurvyangle A \rcurvyangle|\) is closed under further glueings.

We check that this set is closed under instantiation of terms.

Let \(\tau\) be a term. Suppose for each \(i<n\) that \({b_i}\) is the glueing of a compatible set \(C_i\) of elements of \(|\lcurvyangle A \rcurvyangle|\) and for all \(i<j<n\) we have \(Eb_i=Eb_j\), \(=p\), say, with \(p\le E\tau\). Since \(\bigvee_{a\in C_i} Ea = Eb_i = Eb_j = \bigvee_{a\in C_i} Eb_j\land Ea\) we may assume that for all \(i<j< n\) we have \(C_i=C_j\), \(=C\), say. Write \(\bar{b}\) for \(\langle\hskip 1ptb_0,\dots,b_{n-1}\hskip 1pt\rangle\). Now for \(a\) \(a'\in C\) we have \(E\tau^M(\bar{b})\upharpoonright Ea \land E\tau^M(\bar{b})\upharpoonright Ea' = p\land Ea \land p \land Ea' = Ea\land Ea'\). Moreover \[\begin{align} [\tau^M(\bar{b})\upharpoonright Ea = E\tau^M(\bar{b})\upharpoonright Ea'] = & Ea\land Ea'\land [\tau^M(\bar{b}) = E\tau^M(\bar{b})] \\ = & Ea\land Ea'\land p = Ea\land Ea'. \end{align}\] Thus \(\tau^M(\bar{b})\in \lcurvyangle A \rcurvyangle_s\). ◻

Proof. First of all, suppose the inclusions \(M\hookrightarrow P\) and \(N\hookrightarrow P\) are a presheaf morphisms. Let \(a\in |M|\) and \(p\in \Omega\). By the former hypothesis we have \(E^Ma=E^Pa\) and \(a\upharpoonright^M p = a\upharpoonright^P p\); by the latter, since \(|N|\subseteq |P|\), \(E^Pa=E^Na\) and \(a\upharpoonright^P p = a\upharpoonright^N p\). Hence \(E^Ma=E^Na\) and \(a\upharpoonright^M p = a\upharpoonright^N p\), and thus the inclusion \(M\hookrightarrow N\) is also a presheaf morphism.

Now suppose \(N\hookrightarrow P\) is an \(L\)-monomorphism and \(M\hookrightarrow P\) is an \(L\)-morphism, a weak \(L\)-monomorphism or an \(L\)-monomorphism.

For the interpretation of constants and function symbols there is little to be proved. If \(c\) is a constant symbol in \(L\) then, since both inclusions into \(P\) are \(L\)-morphisms, we have \({\mathfrak c}^M = {\mathfrak c}^P = {\mathfrak c}^N\). If \(f\) is an \(n\)-ary function symbol in \(L\) and \(\bar{a}\in |M|^n\) then, again since both inclusions into \(P\) are \(L\)-morphisms, \(f^M(\bar{a}\upharpoonright E\bar{a}) = f^P(\bar{a}\upharpoonright E\bar{a}) = f^N(\bar{a}\upharpoonright E\bar{a})\).

Now suppose \(R\) is an \(n\)-ary relation symbol in \(L\) and \(\bar{a}\in |M|^n\). Since \(|M|^n\subseteq |N|^n\), we have \(\bar{a}\in |N|^n\) and so, since the inclusion of \(N\) into \(P\) is an \(L\)-monomorphism, \([R(\bar{a})]_N = [R(\bar{a}\upharpoonright E\bar{a})]_P\). Moreover, \([R(\bar{a})]_N = {[R(\bar{a}\upharpoonright E\bar{a})]_N}\), and \([R(\bar{a})]_P = [R(\bar{a}\upharpoonright E\bar{a})]_P\), by Lemma (22).

However, we also have \([R(\bar{a})]_M \le [R(\bar{a}\upharpoonright E\bar{a})]_P\), hence \([R(\bar{a})]_M \le [R(\bar{a})]_N = [R(\bar{a}\upharpoonright E\bar{a})]_N\). So \(M\hookrightarrow N\) is an \(L\)-morphism.

If \(\bar{a}\in |M|^n\), we may also have either \(\neg\neg [R(\bar{a})]_M = \neg\neg [R(\bar{a}\upharpoonright E\bar{a})]_P\) or \([R(\bar{a})]_M = [R(\bar{a}\upharpoonright E\bar{a})]_P\), depending on the case. In the first case we have \(\neg\neg [R(\bar{a})]_M = \neg\neg [R(\bar{a})]_N = \neg\neg [R(\bar{a}\upharpoonright E\bar{a})]_N\), and in the second \([R(\bar{a})]_M = [R(\bar{a})]_N = [R(\bar{a}\upharpoonright E\bar{a})]_N\). Hence, \(M\hookrightarrow N\) is a weak \(L\)-monomorphism or an \(L\)-monomorphism if \(M\hookrightarrow P\), respectively, is.

Lastly, suppose \(\Gamma\) is a class of \(L_M\)-formulae and \(M\hookrightarrow P\), \(N\hookrightarrow P\) are \(\Gamma\)-\(L\)-embeddings. Let \(\phi(\underaccent{\bar}{a}_0,\dots,\underaccent{\bar}{a}_{n-1})\in \Gamma\).

Since \(|M|\subseteq |N|\) and \(N\hookrightarrow P\) is an elementary, we have \([\phi(\bar{a})]_N = [\phi(\bar{a})]_P\).

By the hypotheses on \(M\hookrightarrow P\) we have \([\phi(\bar{a})]_M = [\phi(\bar{a})]_P\). Hence \([\phi(\bar{a})]_M = [\phi(\bar{a})]_N\), and we have \(M\hookrightarrow N\) is a \(\Gamma\)-\(L\)-monomorphism. ◻

Proof. We work by induction on the structure of \(\tau\) and so there are five cases to consider.

First of all, suppose \(\tau = v_i\) for some \(i\). Then we have \(\tau^N(f``\bar{a}) =f(a_i) = f(\tau^M(\bar{a}))\).

Secondly, suppose \(c\in |C|\). We have \(c^M(\bar{a}) = {\mathfrak c}^M\upharpoonright E\bar{a}\), \(c^N(\bar{a}) = {\mathfrak c}^N\upharpoonright E\bar{a}\) and by definition, since \(f\) is an \(L\)-morphism, \({\mathfrak c}^N = f({\mathfrak c}^M)\) and \(Ef``\bar{a}=E\bar{a}\). Hence \({\mathfrak c}^N\upharpoonright Ef``\bar{a} = f({\mathfrak c}^M)\upharpoonright Ef``\bar{a} = f({\mathfrak c}^M\upharpoonright E\bar{a})\).

Furthermore, if \(p\le Ec\) we have \(c^M(p) = {\mathfrak c}^M \upharpoonright p\), \(c^N(p) = {\mathfrak c}^N\upharpoonright p\) and \({\mathfrak c}^N\upharpoonright p = f({\mathfrak c}^M)\upharpoonright p = f({\mathfrak c}^M\upharpoonright p)\).

Fourthly, if \(\tau = g(\tau_0,\dots, \tau_{m-1})\) then, since \(f\) is an \(L\)-morphism, we have \[f(\tau^M(\bar{a})) = f( g^M(\tau_0^M(\bar{a}), \dots , \tau_{m-1}^M(\bar{a}) )) = g^N(f(\tau_0^M(\bar{a})), \dots, f(\tau_{m-1}^M(\bar{a}))).\] However, inductively, we have for each \(j<m\) that \(f(\tau_j^M(\bar{a})) = \tau_j^N(f``\bar{a})\), and hence we have that \(f(\tau^M(\bar{a})) = g^N(\tau_0^N(f``\bar{a}), \dots, \tau_{m-1}^M(f``\bar{a})) = \tau^N(f``\bar{a})\).

Finally, if the \(\tau_i\) are all closed terms then for \(p\le E\tau\) we have \(\tau^N (p) = g^N(\tau_0^N(p), \dots , \tau_{m-1}^N(p))\). Yet, for each \(j<m\) we have \(\tau^N_j(p) = f(\tau_j^M(p))\). So we have \[\begin{align} \tau^N (p)& = g^N(\tau_0^N(p), \dots , \tau_{m-1}^N(p)) = g^N(f(\tau_0^M(p),\dots,f(\tau_{m-1}^M(p))\\ & = f(g^M(\tau_0^M(p),\dots,\tau_{m-1}^M(p))) = f(\tau^M(p). \end{align}\] ◻

Proof. First of all we deal with the atomic formulae of the form \(\tau_0 = \tau_1\) where \(\tau_0\), \(\tau_1\) are terms over \(L\). There are six separate cases. In each case the property of \(f\) used in the proof is that it is a presheaf morphism and hence Lemma (9) can be applied.

Case 1. \(\tau_0 = v_i\), \(\tau_1 = v_j\) for some \(i\), \(j\), with \(i\) and \(j\) not necessarily different.

We have \[\begin{align} [\phi(\bar{a})]_M = [(v_i = v_j)(\bar{a})]_M & = [v_i^M(\bar{a}\upharpoonright Ev_i \wedge Ev_j) = v_j^M(\bar{a}\upharpoonright Ev_i \wedge Ev_j) ]_M \\ & = [v_i^M(\bar{a}) = v_j^M(\bar{a})]_M = [a_i = a_j]_M. \end{align}\]Similarly, \([\phi(f``\bar{a})]_N = [f(a_i) = f(a_j)]_N\). Finally, \[[a_i = a_j]_M \le [f(a_i) = f(a_j)]_N , since f is an presheaf morphism.\]

Case 2. \(\tau_0 = v_i\), \(\tau_1 = c\) for some \(i\) and some \(c\in |C|\).

We have \[\begin{align} [\phi(\bar{a})]_M & = [(v_i = c)(\bar{a})]_M = [v_i^M(\bar{a}\upharpoonright Ev_i \wedge Ec) = c^M(\bar{a}\upharpoonright Ev_i \wedge Ec) ]_M \\ & = [v_i^M(\bar{a}\upharpoonright Ec) = {\mathfrak c}^M\upharpoonright E\bar{a}]_M = [a_i\upharpoonright Ec = {\mathfrak c}^M\upharpoonright E\bar{a}]_M. \end{align}\]Similarly, since \(Ef``\bar{a} = E\bar{a}\), we have \[[\phi(f``\bar{a})]_N = [f(a_i)\upharpoonright Ec = {\mathfrak c}^N\upharpoonright E\bar{a}]_N = [f(a_i\upharpoonright Ec) = f({\mathfrak c}^M\upharpoonright E\bar{a})]_N,\] since \(f\) is a presheaf morphism and an \(L\)-morphism. Finally, since \(f\) is an presheaf morphism, by Lemma (9) we have \[[a_i\upharpoonright Ec = {\mathfrak c}^M\upharpoonright E\bar{a}]_M \le [f(a_i\upharpoonright Ec) = f({\mathfrak c}^M\upharpoonright E\bar{a})]_N\]

Case 3. \(\tau_0 = d\), \(\tau_1 = c\) for some \(c\), \(d \in |C|\). Let \(p = Ec\wedge Ed\).

We have \[\begin{align} [\phi]_M & = [c=d]_M = [{\mathfrak c}^M \upharpoonright p = {\mathfrak d}^M \upharpoonright p]_M \\ & \le [f({\mathfrak c}^M \upharpoonright p) = f({\mathfrak d}^M \upharpoonright p)]_M ,by Lemma (\ref{psh95morphism95push95up95equality}),\\ & = [{\mathfrak c}^N\upharpoonright p = {\mathfrak d}^N\upharpoonright p]_N = [c=d]_N = [\phi]_N. \end{align}\]

Case 4. \(\tau_0 = v_i\) and there are \(\sigma_0\), …, \(\sigma_{m-1}\) and a function \(g\) such that \(\tau_1 = g(\sigma_0,\dots,\sigma_{m-1})\). Note \(E\tau_1 = E\sigma_0\wedge\dots\wedge E\sigma_{n-1}\).

We have \[\begin{align} [\phi(\bar{a})]_M & = [(v_i = g(\sigma_0,\dots,\sigma_{m-1}))(\bar{a})]_M \\ & = [a_i\upharpoonright E\tau_1 = g^M(\sigma_0^M(\bar{a}\upharpoonright E\tau_1),\dots,\sigma_{m-1}^M(\bar{a}\upharpoonright E\tau_1))]_M \\ & \le [f(a_i \upharpoonright E\tau_1) = f( g^M(\sigma_0^M(\bar{a}\upharpoonright E\tau_1),\dots,\sigma_{m-1}^M(\bar{a}\upharpoonright E\tau_1)) )]_N \\ & = [f(a_i) \upharpoonright E\tau_1 = g^N ( f(\sigma_0^M(\bar{a}\upharpoonright E\tau_1)),\dots,f(\sigma_{m-1}^M(\bar{a}\upharpoonright E\tau_1))) ]_N \\ & = [f(a_i) \upharpoonright E\tau_1 = g^N ( \sigma_0^N(f``\bar{a}\upharpoonright E\tau_1),\dots,\sigma_{m-1}^N(f``\bar{a})\upharpoonright E\tau_1) ]_N \\ & \qquad \qquad \qquad\qquad \qquad\qquad \qquad \qquad\qquad \qquad (by Lemma (\ref{pres95interp95of95terms})) \\ & = [v_i = g(\sigma_0,\dots,\sigma_{m-1}))(f``\bar{a})]_N = [\phi(f``\bar{a})]_N \end{align}\]

Case 5. \(\tau_0 = c\in |C|\) and there are \(\sigma_0\), …, \(\sigma_{m-1}\) and a function \(g\) such that \(\tau_1 = g(\sigma_0,\dots,\sigma_{m-1})\). Let \(p = E\tau_0\wedge E\tau_1\), \(= Ec\wedge E\sigma_0\wedge\dots\wedge E\sigma_{n-1}\).

We have \[\begin{align} [\phi(\bar{a})]_M & = [(c = g(\sigma_0,\dots,\sigma_{m-1}))(\bar{a})]_M \\ & = [{\mathfrak c}^M \upharpoonright p = g^M(\sigma_0^M(\bar{a}\upharpoonright p),\dots,\sigma_{m-1}^M(\bar{a}\upharpoonright p))]_M \\ & \le [f({\mathfrak c}^M \upharpoonright p) = f( g^M(\sigma_0^M(\bar{a}\upharpoonright p),\dots,\sigma_{m-1}^M(\bar{a}\upharpoonright p))))]_N \\ & = [f({\mathfrak c}^M ) \upharpoonright p = g^N ( f(\sigma_0^M(\bar{a}\upharpoonright p)),\dots,f(\sigma_{m-1}^M(\bar{a}\upharpoonright p))) ]_N \\ & = [{\mathfrak c}^N \upharpoonright p) = g^N ( \sigma_0^N(f``\bar{a}\upharpoonright p),\dots,\sigma_{m-1}^N(f``\bar{a}\upharpoonright p))]_N \\ & \qquad \qquad \qquad\qquad \qquad\qquad \qquad (by Lemma (\ref{pres95interp95of95terms}))\\ & = [(c = g(\sigma_0,\dots,\sigma_{m-1}))(f``\bar{a})]_N = [\phi(f``\bar{a})]_N \end{align}\]

Similarly, if all the \(\sigma_j\) for \(j<m\) are closed terms and then we have \[\begin{align} [\phi]_M & = [c = g(\sigma_0,\dots,\sigma_{m-1})]_M \\ & = [{\mathfrak c}^M \upharpoonright p = g^M(\sigma_0^M ,\dots,\sigma_{m-1}^M) \upharpoonright p ]_M \\ & \le [f({\mathfrak c}^M \upharpoonright p) = f( g^M(\sigma_0^M(p),\dots,\sigma_{m-1}^M(p)))]_N \\ & = [f({\mathfrak c}^M ) \upharpoonright p = g^N ( f(\sigma_0^M(p)),\dots,f(\sigma_{m-1}^M(p))) ]_N \\ & = [{\mathfrak c}^N \upharpoonright p = g^N ( \sigma_0^N(p),\dots,\sigma_{m-1}^N(p))]_N \\ & = [(c = g(\sigma_0,\dots,\sigma_{m-1}))]_N = [\phi]_N \end{align}\]

Case 6. \(\tau_0 = \tau_1\) and there are \(\sigma_0\), …, \(\sigma_{m-1}\), \(\rho_0\), …\(\rho_{k-1}\) and functions \(g\) and \(h\) such that \(\tau_0 = h(\rho_0,\dots,\rho_{k-1})\) and \(\tau_1 = g(\sigma_0,\dots,\sigma_{m-1})\). Let \(p = E\tau_0\wedge E\tau_1\), \(= E\rho_0\wedge\dots\wedge E\rho_{k-1}\wedge E\sigma_0\wedge\dots\wedge E\sigma_{m-1}\).

We have \[\begin{align} [\phi(\bar{a})]_M & =[(h(\rho_0,\dots,\rho_{k-1}) = g(\sigma_0,\dots,\sigma_{m-1}))(\bar{a})]_M \\ & = [h^M(\rho_0^M(\bar{a}),\dots,\rho_{k-1}^M(\bar{a})) \upharpoonright p = g^M(\sigma_0^M(\bar{a}),\dots,\sigma_{m-1}^M(\bar{a})) \upharpoonright p ]_M \\ & \le [f( h^M(\rho_0^M(\bar{a}),\dots,\rho_{k-1}^M(\bar{a})) \upharpoonright p ) = \\ & \qquad f( g^M(\sigma_0^M(\bar{a}),\dots,\sigma_{m-1}^M(\bar{a}))\upharpoonright p )]_N \\ & = [h^N ( f(\rho_0^M(\bar{a})),\dots,f(\rho_{k-1}^M(\bar{a}))) \upharpoonright p = \\ & \qquad g^N ( f(\sigma_0^M(\bar{a})),\dots,f(\sigma_{m-1}^M(\bar{a}))) \upharpoonright p)]_N \\ & = [g^N ( \rho_0^N(f``\bar{a}),\dots,\rho_{k-1}^N(f``\bar{a})) \upharpoonright p = \\ & \qquad g^N ( \sigma_0^N(f``\bar{a}),\dots,\sigma_{m-1}^N(f``\bar{a})) \upharpoonright p]_N , by Lemma (\ref{pres95interp95of95terms}), \\ & = [(g(\rho_0,\dots,\rho_{k-1}) = g(\sigma_0,\dots,\sigma_{m-1}))(f``\bar{a})]_N = [\phi(f``\bar{a})]_N . \end{align}\]

Similarly, if all the \(\sigma_j\) for \(j<m\) and all the \(\rho_e\) for \(e<k\) are closed terms, \[\begin{align} [\phi]_M & = [h(\rho_0,\dots,\rho_{k-1}) = g(\sigma_0,\dots,\sigma_{m-1})]_M \\ & = [h^M(\rho_0^M(p),\dots,\rho_{k-1}^M(p)) = \\ & \qquad g^M(\sigma_0^M (p),\dots,\sigma_{m-1}^M(p)) ]_M \\ & \le [f( h^M(\rho_0^M(p),\dots,\rho_{k-1}^M(p)) ) = \\ & \qquad f( g^M(\sigma_0^M(p),\dots,\sigma_{m-1}^M(p)) )]_N \\ & = [h^N ( f(\rho_0^M(p)),\dots,f(\rho_{k-1}^M(p))) = \\ & \qquad g^N ( f(\sigma_0^M(p)),\dots,f(\sigma_{m-1}^M(p))) )]_N \\ & = [h^N ( \rho_0^N(p),\dots,\rho_{k-1}^N(p)) = \\ & \qquad g^N ( \sigma_0^N(p),\dots,\sigma_{m-1}^N(p)) ]_N, by Lemma (\ref{pres95interp95of95terms}), \\ & = [(h(\rho_0,\dots,\rho_{k-1}) = g(\sigma_0,\dots,\sigma_{m-1}))]_N = [\phi]_N . \end{align}\]

This completes the proof for atomic formulae of the form \(\tau_0=\tau_1\).

Now suppose \(R\) is a relation symbol in \(L\). We need to consider atomic formulae of the form \(R(\tau_0,\dots,\tau_{n-1})\) where for \(i<n\) the \(\tau_i\) are terms. Here we also need that \(f\) is an \(L\)-morphism.

By definition we have \[[R(\tau_0,\dots,\tau_{n-1})(\bar{a})]_M = [R(\tau_0^M(\bar{a}\upharpoonright q) , \dots, \tau_{m-1}^M(\bar{a}\upharpoonright q))]_M,\] where \(q= E\tau_0\wedge\dots\wedge E\tau_{m-1}\).

Since \(f\) is an \(L\)-morphism we have that \[\begin{align} & \; [R(\tau_0^M(\bar{a}\upharpoonright q) , \dots, \tau_{m-1}^M(\bar{a}\upharpoonright q))]_M \\ \le & \; [R(f(\tau_0^M(\bar{a}\upharpoonright q)) , \dots, f(\tau_{m-1}^M(\bar{a}\upharpoonright q)) )]_N \\ = & \; [R(f(\tau_0^M(\bar{a})\upharpoonright q) , \dots, f(\tau_{m-1}^M(\bar{a})\upharpoonright q) )]_N \\ = & \; [R(\tau_0^N(f``\bar{a})\upharpoonright q) , \dots, \tau_{m-1}^N(f``\bar{a})\upharpoonright q) )]_N , using Lemma (\ref{pres95interp95of95terms}),\\ = & \; [R(\tau_0,\dots,\tau_{n-1})(f``\bar{a})]_N . \end{align}\] ◻

Proof. The proof is almost identical to the proof of the previous lemma (Lemma (39), except that in the six cases concerning equality between terms we use the fact that \(f\) is a presheaf monomorphism and so Proposition (11) is applicable, where previously we applied Lemma (9), and in dealing with relations we use the defining property regarding relations of \(L\)-monomorphism rather than that of \(L\)-morphisms. The result is that we preserve equality throughout. ◻

Proof. By hypothesis \([\phi(\bar{a})]_M \le [\phi(f``\bar{a})]_N\), so \(\neg [\phi(\bar{a})]_M \ge \neg [\phi(f``\bar{a})]_N\). Using the two clauses of the definition of presheaf morphism, we also have \(E(f``\bar{a}\upharpoonright E\phi) = E(\bar{a}\upharpoonright E\phi)\). Hence \[\begin{align} [\neg \phi(f``\bar{a})]_N & = E(f``\bar{a}\upharpoonright E\phi) \land \neg [\phi(f``\bar{a}\upharpoonright E\phi)]_N \\ & \le E(\bar{a}\upharpoonright E\phi) \land \neg [\phi(\bar{a})]_M = [\neg \phi(\bar{a})]_M . \end{align}\] ◻

Proof. The proof is similar to that of the previous lemma, but with inequality replaced by equality. By hypothesis \([\phi(\bar{a})]_M = [\phi(f``\bar{a})]_N\), so \(\neg [\phi(\bar{a})]_M = \neg [\phi(f``\bar{a})]_N\). Using the two clauses of the definition of presheaf morphism, we also have \(E(f``\bar{a}\upharpoonright E\phi) = E(\bar{a}\upharpoonright E\phi)\). Hence \[\begin{align} [\neg \phi(f``\bar{a})]_N & = E(f``\bar{a}\upharpoonright E\phi) \land \neg [\phi(f``\bar{a}\upharpoonright E\phi)]_N \\ & = E(\bar{a}\upharpoonright E\phi) \land \neg [\phi(\bar{a})]_M = [\neg \phi(\bar{a})]_M . \end{align}\] ◻

Proof. Let \(q=E\phi \land E\psi\). Then, again using the definition of a presheaf morphism, \(E(f``\bar{a} \upharpoonright q) = E(\bar{a} \upharpoonright q)\), \(=r\), say. Then we have \[\begin{align} [\phi \diamond \psi(f``\bar{a})]_N & = r \land ([\phi(f``\bar{a}\upharpoonright q)]_N \diamond [\psi(f``\bar{a}\upharpoonright q)]_N ) \\ & = (r \land [\phi(f``\bar{a}\upharpoonright q)]_N) \diamond (r\land [\psi(f``\bar{a}\upharpoonright q)]_N) \\ & \ge (r \land [\phi(\bar{a}\upharpoonright q)]_M) \diamond (r \land [\psi(\bar{a}\upharpoonright q)]_M)) \\ & = r \land ([\phi(\bar{a}\upharpoonright q)]_M \diamond [\psi(\bar{a}\upharpoonright q)]_M) = [(\phi \diamond \psi)(\bar{a})]_M . \end{align}\] ◻

Proof. Let \(q=E\phi \land E\psi\). Then, once more using the definition of a presheaf morphism, \[\begin{align} [\phi \diamond \psi(f``\bar{a})]_N & = E(f``\bar{a} \upharpoonright q) \land [\phi(f``\bar{a}\upharpoonright q)]_N \diamond [\psi(f``\bar{a}\upharpoonright q)]_N = \\ & E(\bar{a} \upharpoonright q) \land [\phi(\bar{a}\upharpoonright q)]_M \diamond [\psi(\bar{a}\upharpoonright q)]_M = [(\phi \diamond \psi)(\bar{a})]_M . \end{align}\] ◻

Proof. The proof is by induction on the structure of \(\phi\). Lemma (40) deals with atomic formulae. Since \(f\) is an \(L\)-morphism inductive steps involving the binary connectives (\({\lor, \land,\mathop{\parbox{.5cm}{\rightarrowfill}}}\)) can be handled by Lemma (44) and those involving negation can be handled by Lemma (42). ◻

Proof. By the proposition, \([\phi(\bar{a})]_M = [\phi(f``\bar{a})]_N\), whilst \(Ef``\bar{a}=E\bar{a}\) since \(f\) is a presheaf morphism. So \([\phi(\bar{a})]_M = E\phi \wedge E\bar{a}\) if and only if \([\phi(f``\bar{a})]_N = E\phi \wedge Ef``\bar{a}\), as required. ◻

Proof. For the first statement, using the hypothesis for the first inequality and that \(f``|M| \subseteq |N|\) for the second, we have \[\begin{align} [\exists t \hskip 2pt\phi(t,\bar{a})]_M & = \bigvee_{b\in |M|} [\phi(b,\bar{a})]_M \le \bigvee_{b\in |M|} [\phi(f(b),f``\bar{a})]_N \\ & \le \bigvee_{d\in |N|} [\phi(d,f``\bar{a})]_N = [\exists t\hskip 2pt\phi(t,f``\bar{a})]_N . \end{align}\] For the second statement, using the hypothesis for the second equality and that \(f``|M| = |N|\) for the third, we have \[\begin{align} [\exists t \hskip 2pt\phi(t,\bar{a})]_M & = \bigvee_{b\in |M|} [\phi(b,\bar{a})]_M = \bigvee_{b\in |M|} [\phi(f(b),f``\bar{a})]_N \\ & = \bigvee_{d\in |N|} [\phi(d,f``\bar{a})]_N = [\exists t\hskip 2pt\phi(t,f``\bar{a})]_N . \end{align}\] ◻

Proof. The proof is by induction on the structure of \(\phi\). Lemma (39)) deals with atomic formulae and the previous lemma (Lemma (47)) deals with existential quantification.

Finally, suppose \(\diamond \in\{\hskip 1pt\lor, \land\hskip 1pt\}\). Let \(\chi(\bar{v})\), \(\psi(\bar{v})\) be formulae in \({\mathcal{E}}^+_1\) and \(\bar{a}\in |M|^n\). Suppose, by induction, \([\chi(\bar{a})]_M \le [\chi(f``\bar{a})]_N\) and \([\psi(\bar{a})]_M \le [\psi(f``\bar{a})]_N\). Then by Lemma (43) we have \([\chi \diamond \psi(f``\bar{a})]_N \le [(\chi \diamond \psi)(\bar{a})]_M\). ◻

Proof. This is immediate from Proposition (45), since again existential quantification can again be handled by Lemma (47) and conjunction and disjunction can be handled by Lemma (43). ◻

Proof. By Proposition (49), \([\phi(\bar{a})]_M \le [\phi(f``\bar{a})]_N\). However, by hypothesis \(M\Vdash\phi(\bar{a})\), so we have \([\phi(\bar{a})]_M = E\phi \wedge E\bar{a}\), and hence \(E\phi \wedge E\bar{a} \le [\phi(f``\bar{a})]_N\). However, by Lemma (29), \([\phi(f``\bar{a})]_N \le E\phi \wedge Ef``\bar{a} =E\phi \wedge E\bar{a}\), so we also have \([\phi(f``\bar{a})]_N = E\phi \wedge Ef``\bar{a}\), and thus \(N\Vdash\phi(f``\bar{a})\). ◻

Proof. (1) implies (2). Let \(f:M \longrightarrow N\) be a \(\Gamma\)-\(L\)-monomorphism. Thus, if \(\phi(\underaccent{\bar}{a}_0,\dots,\underaccent{\bar}{a}_{n-1})\in\Gamma\) we have \([\phi(\bar{a})]_M = [\phi(f``\bar{a})]_N\). Let \(\tilde{M} = (M,a)_{a\in |M|}\) and \(\tilde{N} = (N,f(a))_{a\in |M|}\). We also have \([\phi(\bar{a})]_M = [\phi(\underaccent{\bar}{\bar{a}}^{\tilde{M}})]_M\) and \([\phi(f``\bar{a})]_N = [\phi(\underaccent{\bar}{\bar{a}}^{\tilde{N}})]_N\). Thus \([\phi(\underaccent{\bar}{\bar{a}}^{\tilde{M}})]_M = [\phi(\underaccent{\bar}{\bar{a}}^{\tilde{N}})]_N\). Hence, \(\tilde{N}\) is an expansion of \(N\) to and \(L_M\)-structure with \([.]_{\tilde{N} } \upharpoonright\Gamma = [.]_{\tilde{M}} \upharpoonright\Gamma\).

(2) implies (1). Define \(f:M \longrightarrow N\) by \(f(a) = \underaccent{\bar}{a}^{\tilde{N}}\). By Lemma (33), \(f\) is a presheaf morphism. If \(\phi(\underaccent{\bar}{a}_0,\dots,\underaccent{\bar}{a}_{n-1}) \in \Gamma\) then \([\phi(\underaccent{\bar}{a}_0^{\tilde{M}},\dots,\underaccent{\bar}{a}_{n-1}^{\tilde{M}})]_{\tilde{M} }= [\phi(\underaccent{\bar}{a}_0^{\tilde{N}},\dots,\underaccent{\bar}{a}_{n-1}^{\tilde{N}})]_{\tilde{N} }\), and so \([\phi({a}_0,\dots,{a}_{n-1})]_{{M} } = [\phi(f({a}_0),\dots,f({a}_{n-1}))]_{{N} }\). Thus \(f\) is a \(\Gamma\)-\(L\)-monomorphism. ◻

Proof. Immediate from Proposition (51), using Proposition (49) to show 1(c) implies 1(b). ◻

Proof. (See also the proof of [1], Theorem (5.8).)

(1). We have \([\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}}\upharpoonright q)]_{\tilde{M}} = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \land [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}}\). However, we also have \([\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \le E\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})\), by Lemma (29), while \(E\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}}\upharpoonright q) = E\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}}) \land q\le q = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}}\).

(2). If \(\tilde{N} \Vdash\phi(\bar{\underaccent{\bar}{a}}\upharpoonright q)\) then \(q = E\bar{\underaccent{\bar}{a}}\upharpoonright q \land E\phi = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}}\upharpoonright q)]_{\tilde{N}} = q \land [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\). If \([\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \le [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\) then \([\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})\upharpoonright q)] = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}} \land q = q = q\land q = [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}}\upharpoonright q)]_{\tilde{M}} = E\bar{\underaccent{\bar}{a}}^{\tilde{M}}\upharpoonright q \land E\phi = E\bar{\underaccent{\bar}{a}}^{\tilde{N}}\upharpoonright q \land E\phi\), where the penultimate equality holds by (1).

(3). By (2) one immediately has \(\neg\neg [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \le \neg\neg [\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\).

Applying (2) for \(\neg\phi\) in place of \(\phi\), one also has \([\neg\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \le [\neg\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\), that is \(E\bar{a} \land \neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \le E\bar{a}\land \neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\). Taking the \(\land\) with \(\neg\neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}}\) on both sides give \(E\bar{a} \land \neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}} \land \neg\neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}} =\bot\), and hence one has \(E\bar{a} \land \neg\neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}} \le \neg\neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}}\). However, \([\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}} \le E\bar{a}\), so \(\neg\neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{N}})]_{\tilde{N}} \le \neg \neg[\phi(\bar{\underaccent{\bar}{a}}^{\tilde{M}})]_{\tilde{M}}\).

(4.) Using modus ponens (Lemma 2) for the second equality, the hypothesis that \(q\le p\) for the third and penultimate equalities, and (1) for the fourth equality, we have \[\begin{align} (E\bar{a}\upharpoonright p ) \land d & = E\bar{a}\upharpoonright(p\land d) = E\bar{a}\upharpoonright(p\land q) = E\bar{a} \upharpoonright q = [\phi(\bar{a}\upharpoonright q)]_M\\ & = [\phi(\bar{a})]_M \land q = q \land q = q = q\land p = [\phi(\bar{a}\upharpoonright p)]_M. \end{align}\] ◻

Proof. The equivalence of (2) and (3) is follows from Corollary (48). The proof that (3) implies (1) follows immediately from Lemma (53(2)). To see that (1) implies (3) note that if \(\phi(\bar{\underaccent{\bar}{a}}) \in \Delta^+_M\) then \([\phi(\bar{a})] = E\bar{a}\land E\phi\), as \(f\) is an \(L\)-morphism we have \([\phi(\bar{a})]\le [\phi(f``\bar{a})]\), and \(E\bar{a}\land E\phi = Ef``\bar{a}\land E\phi\). ◻

Proof. This theorem is similarly immediate from the proof of (1) implies (3) in the corresponding result [1], Proposition (4.7), which follows directly from Lemma (53(3)), using Lemma (43) and Lemma (48). ◻

Proof. Throughout we write \([. = .]_i\) for \([.=.]_{M_i}\), where the latter is as defined in Definition (9).

We start by defining the underlying set of the colimit and showing this is a good definition. We then show how to equip the set with the structure of a presheaf and show the resulting presheaf is extensional. As a final step in the presheaf part of the construction define morphisms from the \((A_i,M_i)\) into the colimit and show these are presheaf morphisms or presheaf monomorpisms, respectively if the morphisms in directed system have the corresponding property.

Let \(|M^*| = \bigcup (|M_i| \times \{\hskip 1pti\hskip 1pt\})\) be the disjoint union of the underlying sets of the \(M_i\)s. Also, let \(|A^*| = \bigcup (|A_i| \times \{\hskip 1pti\hskip 1pt\})\).

We define an equivalence relation on \(|M^*|\) by \((x,i) \sim (y,j)\) if there is some \(l\in I\) with \(i\), \(j\hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\) and \(g_{il}(x)=g_{jl}(y)\).

It is immediate that \(\sim\) is reflexive and symmetric. The transitivity of \(\sim\) follows rapidly from directedness. If \((x,i) \sim (y,j) \sim (z,k)\) with \(l\), \(m\) such that \(i\), \(j\hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\) and \(j\), \(k\hskip 2pt\mathrel{\triangleleft}\hskip 2ptm\), while \(g_{il}(x)=g_{jl}(y)\) and \(g_{jm}(y)=g_{km}(z)\) we can take \(n\in I\) with \(l\), \(m\hskip 2pt\mathrel{\triangleleft}\hskip 2ptn\). We then have \(i\), \(j\), \(k\hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\) and \[g_{in}(x) = g_{ln}\cdot g_{il}(x) = g_{ln}\cdot g_{jl}(y) = g_{mn}\cdot g_{jm}(y) = g_{mn}\cdot g_{km}(z) = g_{kn}(z),\] and hence \((x,i)\sim (z,k)\).

For \((x,i)\in |M^*|\) write \((x,i)_{\sim}\) for its equivalence class under \(\sim\). We set \(|M| = \{\hskip 1pt (x,i)_{\sim}\hskip 2pt:\hskip 2pt(x,i) \in |M^*|\hskip 1pt\}\), the quotient of \(|M^*|\) under \(\sim\). We set \(|A| = \{\hskip 1pt (x,i)_{\sim}\hskip 2pt:\hskip 2pt(x,i) \in |M^*| \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2ptx\in |A_i|\hskip 1pt\}\).

We will define \(\upharpoonright^M : |M| \times\Omega \longrightarrow |M|\) and \(E^M : |M| \longrightarrow \omega\). For \((x,i)_{\sim} \in |M|\) and \(p\in\Omega\) define \(((x,i)_{\sim} ) \upharpoonright^M p\) to be \((x\upharpoonright^{M_i} p,i)_{\sim}\) and \(E^M ((x,i)_{\sim}) = E^{M_i}x\). We set \(M = (|M|,\upharpoonright^M,E^M)\).

We define \(\upharpoonright^A\) and \(E^A\) similarly: for \((x,i)_{\sim} \in |A|\) and \(p\in\Omega\) define \(((x,i)_{\sim} ) \upharpoonright^A p\) to be \((x\upharpoonright^{A_i} p,i)_{\sim}\) and \(E^A ((x,i)_{\sim}) = E^{A_i}x\). We set \(M = (|A|,\upharpoonright^A,E^A)\).

We need to check these are good definitions. So suppose \((x,i)\sim (y,j)\) and let \(k\in I\) be such that \(i\), \(j\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) and \(g_{ik}(x)=g_{jk}(y)\). Let \(p\in\Omega\).

By the first clause in the definition of presheaf morphisms we have that \(E^{M_i} x = E^{M_k} g_{ik}(x)= E^{M_k} g_{jk}(y) = E^{M_j} y\). Hence, \(E^M\) is well defined.

By the second clause in the definition of presheaf morphism we have that \(g_{ik}(x\upharpoonright p) = g_{ik}(x) \upharpoonright p = g_{jk}(y) \upharpoonright p = g_{jk}(y\upharpoonright p)\). Consequently we have that \((x\upharpoonright p,i)\sim (y\upharpoonright p,i)\). This shows that \(\upharpoonright^M\) is well defined.

The same proofs verbatim with \(M_i\), \(M_j\), \(M_k\) and \(M\) replaced by \(A_i\), \(A_j\), \(A_k\) and \(A\) respectively show that \(E^A\) and \(\upharpoonright^A\) are also well defined.

We next check that \(M=(|M|,\upharpoonright^M,E^M)\) is indeed a presheaf over \(\Omega\). Let \(a = (x,i)_{\sim} \in |M|\) and \(p\), \(q\in \Omega\).

We have \(a\upharpoonright^M (p\wedge q) = (x\upharpoonright^{M_i} (p\wedge q),i)_{\sim} = ( (x\upharpoonright^{M_i} p)\upharpoonright^{M_i} q,i)_{\sim} = {((x\upharpoonright^{M_i} p),i)_{\sim} \upharpoonright^M q} = ((x,i)_{\sim} \upharpoonright^M p) \upharpoonright^M q = (a \upharpoonright^M p)\upharpoonright^M q,\) as required.

We also have that \(a \upharpoonright^M E^Ma = ((x,i)_{\sim}) \upharpoonright^M (E^{M_i} x) = (x\upharpoonright(E^{M_i}x,i)_{\sim} = (x,i)_{\sim}=a\), as required.

We, finally, have \(E^M (a\upharpoonright^M p) = E^M((x\upharpoonright^{M_i} p,i)_{\sim}) = E^{M_i}( x\upharpoonright^{M_i} p) = (E^{M_i}x)\wedge p = (E^M ((x,i)_{\sim})) \wedge p = E^Ma \wedge p\), again, as required.

Again, the same proofs verbatim with \(M_i\) and \(M\) replaced by \(A_i\) and \(A\) show that \(A\) is a presheaf and hence is a subpresheaf of \(M\).

We also show that \(M\) is extensional. So suppose \(a\), \(b\in |M|\) with \(a= (x,i)_{\sim}\) and \(b= (y,i)_{\sim}\) (where we may take the second coordinate of the representative of each equivalence class to be the same by directedness), and suppose that \(D\subseteq \Omega\) is such that for all \(p\in D\) we have \(a\upharpoonright^M p=b\upharpoonright^M p\) and \(E^Ma=E^Mb=\bigvee D\). (The latter is long-hand for \(E^Ma=E^Mb = [a=b]_M\).)

We have \(E^{M_i}x = E^{M_i}y =\bigvee D\) and \(x\upharpoonright^{M_i} p =y\upharpoonright^{M_i} p\). By the extensionality of \(M_i\) this gives that \(x=y\). Hence \(a=b\).

Once more, the same proofs with \(M_i\) and \(M\) replaced by \(A_i\) and \(A\) show that \(A\) is extensional.

Finally, as far as the pure presheaf side of things goes, we define presheaf morphisms from the \(M_i\) to \(M\) and show they are monomorphisms if the maps witnessing the directed system are.

For each \(i\in I\) we define \((A_i,M_i) \xlongrightarrow{g_{i}} (A,M)\) by for each \(x\in M_i\) setting \(g_i(x) = (x,i)_{\sim}\). Note that if \(x\in |A_i|\) then \(g_i(x)\in |A|\).

If \(x\in M_i\) and \(p\in\Omega\) then \(E^{M} g_i(x) = E^{M_i}x\), by the definition of \(E^M\) and, further, \(g_i(x \upharpoonright^{M_i} p) = (x \upharpoonright^{M_i} p,i)_{\sim} = (x,i)_{\sim}\upharpoonright^M p\), by the definition of \(\upharpoonright^M\). Hence for \(i\in I\) we have that \(g_i\) is a presheaf morphism.

Now, suppose \(g_{ij}\) is an presheaf monomorphism for all \(i\), \(j\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptj\).

Let \(i\in I\). Suppose \(x\), \(y\in M_i\) and \(g_i(x) = g_i(y)\). Thus \((x,i)_{\sim} = (y,i)_{\sim}\). However, by the definition of \((x,i)_{\sim}\), the latter implies there is some \(k\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) and \(g_{ik}(x)=g_{ik}(y)\). Since \(g_{ik}\upharpoonright M_i\) is injective this gives \(x=y\). Hence, we’ve shown \(g_i\upharpoonright M_i\) is also injective and that \(g_i\) is a presheaf monomorphism.

We suppose from here on that for each \(i\in I\) we have \(M_i\in\mathop{\mathrm{pSh}}({\Omega,L})\) and for \(i\), \(j \in I\) such that \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptj\) we have \(g_{ij}\) is an \(L\)-morphisms. This assumption on the morphisms is necessary in order to equip the whole of \(M\) as an \(L\)-structure.

We will next equip \(M\) with structure so that \(M\in \mathop{\mathrm{pSh}}({\Omega,L})\). We have to define the interpretation of constants, relations and functions and show these definitions are good. (Note “\(=\)” is also one of the relations we need to check is interpreted correctly.) We will then check the morphisms are of the appropriate type if the ones in the directed system are of that type.

We have a presheaf of constants \(C\) and need to define a presheaf morphism \(\cdot^M:C\longrightarrow M\) given by \(c\mapsto {\mathfrak c}^{M}\) for \(c\in |C|\).

We already have the interpretations in the \(M_i\), given by the morphisms \(\cdot^{M_i}\). We also have for all \(i\), \(j\in\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptj\) and \(c\in C\) that \(g_{ij}({\mathfrak c}^{M_i})={\mathfrak c}^{M_j}\).

So we define \(\cdot^M\) by choosing \(i\in I\) and setting \({\mathfrak c}^{M} = ({\mathfrak c}^{M_i},i)_{\sim}\). The usual argument using directedness shows this definition is independent of the choice of \(i\). For any \(j\in I\) then there is \(k\in I\) such that \(i\), \(j\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) and we have \(g_{ik}({\mathfrak c}^{M_i})={\mathfrak c}^{M_k} = g_{jk}({\mathfrak c}^{M_j})\), thus \(({\mathfrak c}^{M_i},i) \sim ({\mathfrak c}^{M_j},j)\).

Recall from Definition (11) that \[|M^n| = \{\hskip 1pt\langle\hskip 1pta_0,\dots,a_{n-1}\hskip 1pt\rangle \hskip 2pt:\hskip 2pt\forall i < n \; a_i \in |M| \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pt\forall i,\hskip 1ptj < n\; E^{M}a_i = E^{M}a_j\hskip 1pt\}.\]

For every function symbol \(\omega\), we define \(\omega^M : |M^n| \longrightarrow |M|\), a presheaf morphism, given by \(\bar{a} \mapsto \omega^M(\bar{a})\) as follows.

Suppose \(\bar{a} = \langle\hskip 1pta_0,\dots,a_{n-1}\hskip 1pt\rangle = \langle\hskip 1pt(x_0,i_0)_\sim,\dots,(x_{n-1},i_{n-1})_\sim\hskip 1pt\rangle\). Exploiting directedness once more, let \(k\in I\) be such that for all \(j<n\) we have \(i_j \hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) and for \(j<n\) write \(y_j\) for \(g_{i_j k}(x_j)\). Then \(\bar{a} = \langle\hskip 1pt(y_0,k)_\sim,\dots,(y_{n-1},k)_\sim)\hskip 1pt\rangle\). We set \[\omega^M(\bar{a}) = (\omega^{M_k}(y_0,\dots,y_{n-1}),k)_\sim.\]

We must check this definition is independent of the choice of representatives of \(a_0\), …, \(a_{n-1}\) and of the choice of \(k\). So, for \(j<n\) let \((x'_j,i'_j)\) be such that \((x_j,i_j) \sim (x'_j,i'_j)\) and let \(k'\in I\) be such that for all \(j<n\) we have \(i'_j \hskip 2pt\mathrel{\triangleleft}\hskip 2ptk'\); for \(j<n\) write \(y'_j\) for \(g_{i_j k'}(x'_j)\).

Let \(l\in I\) be such that \(k\), \(k'\hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\). For all \(j<n\) we have \(g_{kl}(y_j)=g_{k'l}(y'_j)\), \(=z_j\), say, and, since \(g_{kl}\), \(g_{k'l}\) are \(L\)-morphisms, \[\omega^{M_k}(y_0,\dots,y_{n-1}) = \omega^{M_l}(z_0,\dots,z_{n-1}) = \omega^{M_{k'}}(y'_0,\dots,y'_{n-1}),\] as required.

It is clear from the definition of \(g_i\) that if \(\bar{a}=\langle\hskip 1pta_0,\dots,a_{n-1}\hskip 1pt\rangle\in M_i^n\) then \[\omega^M(\langle\hskip 1ptg_i(a_0),\dots,g_i(a_{n-1})\hskip 1pt\rangle)= g_i(\omega^{M_i}(\bar{a})).\]

Now we define the interpretation of relation symbols (including equality). Let \(R\) be an \(n\)-ary relation symbol in \(L\) and \(\bar{a} = \langle\hskip 1pta_0,\dots,a_{n-1}\hskip 1pt\rangle \in |M|^n\). (Note, here, in contrast to the function symbol case just treated, \(\bar{a}\in |M|^n\), and not \(|M^n|\).)

Set \[\begin{align} [R^M(\bar{a})]_M = & \bigvee \{\hskip 1pt[R^{M_k}(g_{i_0k}(x_0),\dots,g_{i_{n-1}k}(x_{n-1}) ) ]_{M_k} \hskip 1pt: \\ & \hskip 1pt\;\;\; (x_0,i_0)\in a_0 , \dots , (x_{n-1},i_{n-1}) \in a_{n-1} \hskip 2pt\hskip 2pt and \hskip 2pt\hskip 2pt i_0,\dots,i_{n-1}\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk \hskip 1pt\} . \end{align}\] If \((x_0,\dots,x_{n-1})\in |M_i|^n\) it is immediate from the definition of \(R^M\) that \([ R^{M_i}(x_0,\dots,x_{n-1}) ]_{M_i} \le [ R^M(g_i(x_0),\dots,g_i(x_{n-1})) ]_M\).

So once we have shown that each \([R(.)]_M\) is a characteristic function we will have shown that for \(i\in I\) we have that \(g_i\) is an \(L\)-morphism.

We next give an alternative characterization, in the general situation where the \(g_{ij}\) for \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptj\) are simply \(L\)-morphisms, of the interpretation of relation symbols in \(M\). This simplifies some of the proofs below.

That is, there is no need to take the supremum over all representatives of \(\bar{a}\) in the definition of \([R(\bar{a})]_M\), we can simply fix some representatives and take the appropriate supremum with respect to their upwards images as in the right hand side of the equation of this paragraph.

We next show that each \([R(.)]_M\) is a characteristic function. So, suppose \(R\) is an \(n\)-ary relation symbol in \(L\). For \(\bar{a}\in |M|^n\) let \[\begin{align} X = \{\hskip 1pt(\langle\hskip 1pt(x_0,i_0)_\sim,\dots,(x_{n-1},i_{n-1})_\sim\hskip 1pt\rangle,k) \hskip 1pt: \hskip 1pt\forall & j < n \; ( x_j\in |M_{i_j}|\hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pt\\ & (x_j,i_j)\in a_j \hskip 2pt\hskip 2pt\&\hskip 2pt\hskip 2pti_0\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk ) \} \end{align}\]

Let \(\tilde{x}=(\langle\hskip 1pt(x_0,i_0)_\sim,\dots,(x_{n-1},i_{n-1})_\sim\hskip 1pt\rangle,k) \in X\). For \(j<n\) set \(z_j=g_{i_jk}(x_j)\). Set \(\bar{z}=\bar{z}_{\tilde{x}} = \langle\hskip 1ptz_0,\dots,z_{n-1}\hskip 1pt\rangle\). Since \([R(.)]_{M_k}\) is a characteristic function, we have \([R(\bar{z})]_{M_k} \le E^{M_k}\bar{z}\). Further, since \(g_k\) is a presheaf morphism we have \(E^M\bar{a} = E^{M_k}\bar{z}\).

Thus, \([R(\bar{a})]_M = \bigvee\{\hskip 1pt[R(\bar{z}_{\tilde{x}})]_{M_k}\hskip 2pt:\hskip 2pt\tilde{x} \in X\hskip 1pt\} \le E^Ma\).

Now suppose \(\bar{a}\), \(\bar{b}\in |M|^n\). By directedness choose \(k\in I\) and \(\bar{x}\), \(\bar{y}\in |M_k|^n\) such that for all \(j<n\) we have \(g_k(x_j)=a_j\) and \(g_k(y_j)=b_j\).

By Lemma (57), for the first equality, the distributivity of \(\wedge\) over \(\bigvee\) twice, for the second equality, the fact that the \([R(.)]_{M_l}\) are characteristic functions for all \(l\in I\) for the inequality and Lemma (57), again, for the final equality, we have \[\begin{align} [\bar{a}=\bar{b}]_M & \wedge [R(\bar{b})]_M \\ & = \bigvee\{\hskip 1pt [g_{kl}``\bar{x} = g_{kl}``\bar{y}]_{M_l}\hskip 2pt:\hskip 2ptk \hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\hskip 1pt\} \wedge \bigvee\{\hskip 1pt [R(g_{kl}``\bar{y})]_{M_l}\hskip 2pt:\hskip 2ptk \hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\hskip 1pt\} \\ & = \bigvee\{\hskip 1pt [g_{kl}``\bar{x} = g_{kl}``\bar{y}]_{M_l} \wedge [R(g_{kl}``\bar{y})]_{M_l}\hskip 2pt:\hskip 2ptk \hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\hskip 1pt\} \\ & \le \bigvee\{\hskip 1pt[R(g_{kl}``\bar{x})]_{M_l}\hskip 2pt:\hskip 2ptk \hskip 2pt\mathrel{\triangleleft}\hskip 2ptl\hskip 1pt\} = [R(\bar{a})]_M . \end{align}\]

Thus we have shown that \([R(.)]_M\) is a characteristic function.

We now need to address the cases where the \(g_{ij}\) have further preservation properties.

First of all, let us suppose that for all \(i\), \(k\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) we have that \(g_{ij}\) is a weak \(L\)-monomorpism. We shall show for each \(i\in I\) that \(g_i\) is also a weak \(L\)-monomorphism.

Suppose \(\bar{x}\in |M_i|^n\) and \(\bar{a}=(x_0,i),\dots,x_{n-1},i)_\sim\).

For each \(k\) such that \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) we have \[[R(g_{ik}``\bar{x})]_{M_k} \le \neg\neg [R(g_{ik}``\bar{x})]_{M_k} = \neg\neg [R(\bar{x})]_{M_i} .\] Thus, by Lemma (57) above, we have \[\begin{align} [R(\bar{a})]_{M} = \bigvee& \{\hskip 1pt[R(g_{ik}``\bar{x})]_{M_k} \hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\hskip 1pt\} \le \\ & \bigvee\{\hskip 1pt\neg\neg [R(g_{ik}``\bar{x})]_{M_k} \hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\hskip 1pt\} = \neg\neg [R(\bar{x})]_{M_i} \end{align}\]

However, since, as just shown above \(g_i\) is an \(L\)-morphism, we also have \([R(\bar{x})]_{M_i} \le [R(\bar{a})]_M\), and hence \(\neg\neg [R(\bar{x})]_{M_i} \le \neg \neg [R(\bar{a})]_M\).

Thus we have shown \(\neg\neg [R(\bar{x})]_{M_i} = \neg \neg [R(\bar{a})]_M\), as required.

Now, suppose let us suppose that for all \(i\), \(k\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) we have that \(g_{ij}\) is an \(L\)-monomorpism. We shall show for each \(i\in I\) that \(g_i\) is also an \(L\)-monomorphism.

Let \(i\in I\) and \(\bar{x}\in |M_i|^n\) and \(\bar{a}=g_i``\bar{x}\). By Lemma (57) we have that \([R(g_i``\bar{x})]_M = \bigvee\{\hskip 1pt [R(g_{i_0k}(x_0),\dots,g_{i_{n-1}k}(x_{n-1}) )]_{M_k}\hskip 2pt:\hskip 2pti_0,\dots, i_k \hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\hskip 1pt\}\).

However, by the hypothesis that for each \(k\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) we have \(g_{ik}\) is an restricted \(L\)-monomorphism, we have for each such \(k\) that \([R(\bar{x})]_{M_i} = [R(g_{ik} ``\bar{x})]_{M_{k}}\).

Hence \([R(g_i``\bar{x})]_M = [R(\bar{x})]_{M_i}\).

We remark that, by Proposition (11), for equality, “\(=\)”, we simply need the \(g_{ik}\) to be presheaf monomorphisms.

Penultimately, suppose for all \(i\), \(k\in I\) with \(i\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\) we have \(g_{ij}\) is an elementary \(L\)-embedding. We will show that for all \(i\in I\) we have \(g_i\) is an elementary \(L\)-embedding. We prove this by induction on the complexity of formulae.

By Lemma (45) we only need to consider the quantifiers.

Suppose \(\phi(t,v_0,\dots,v_n )\) is an \(L\)-formula with free variables shown. Let \(i\in I\) and \(\bar{x}\in |M_i|^n\), and for \(j<n\) let \(a_j = (x_j,i)_{\sim}\). Then \[\begin{align} [ \exists t \;\phi(t,\bar{a})]_M & = \bigvee\{\hskip 1pt[\phi(b,\bar{a})]_M \hskip 2pt:\hskip 2ptb\in |M|\hskip 1pt\}\\ & = \bigvee\{\hskip 1pt [\phi(y,g_{ik}``\bar{x})]_{M_k} \hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk \hskip 1pt\hskip 1pt\&\hskip 1pt\hskip 1pty\in |M_k|\hskip 1pt\}\\ & =\bigvee\{\hskip 1pt[\exists t \; \phi(t,g_{ik}``\bar{x})]_{M_k}\hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\hskip 1pt\} \\ & = [\exists t \;\phi(t,\bar{x})]_{M_i}. \end{align}\]Here the first and third equality are given by the definition of interpretation of existential quantification in \(M\) and the \(M_k\) respectively, while the second equality is given by the inductive hypothesis and the final equality is given by the elementarity of the \(g_{ik}\).

Sentences with a leading universal quantifier are handled similarly.

\[\begin{align} [ \forall t \;\phi(t,\bar{a})]_M & = E\bar{a} \land E\phi \land \bigwedge \{\hskip 1ptEb \longrightarrow [\phi(b,\bar{a})]_M \hskip 2pt:\hskip 2ptb\in |M|\hskip 1pt\}\\ & = E\bar{x} \land E\phi \land \bigwedge \{\hskip 1ptEy \longrightarrow [\phi(y,g_{ik}``\bar{x})]_M \hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk \hskip 1pt\hskip 1pt\& \hskip 1pt\hskip 1pty\in |M_k|\hskip 1pt\}\\ & = \bigwedge \{\hskip 1pt [ \forall t \;\phi(t,g_{ik}``\bar{x})]_{M_k}\hskip 2pt:\hskip 2pti\hskip 2pt\mathrel{\triangleleft}\hskip 2ptk\hskip 1pt\} \\ & = [\forall t \;\phi(t,\bar{x})]_{M_i}, \end{align}\]

We now address sheafification.

By [1], Theorem 2.15, which summarizes [76], Theorem 27.9, Theorem 37.8 and Corollary 37.9, if we apply the sheafification process to both \(A\) and \(M\) (separately), obtaining \(cA\) and \(cM\) there is a unique morphism \(d\) from \(cA\) to \(cM\) such that we get a commutative square

\[\begin{tikzcd} A \arrow{r}{c^A} \arrow{d}{id} & cA \arrow{d}{d} \\ M \arrow{r}{c^M} & cM \end{tikzcd}\]

By the construction (see [76], Example 27.12) we have that \(g\) is a presheaf monomorphism. Specifically, for \(a\in |A|\) we have that \(c^A(a) \in ^{|A|}\Omega\) is the function taking each \(y\in |A|\) to \([a=y]_A\) and \(c^M(a) \in ^{|M|}\Omega\) is the function taking each \(y\in |M|\) to \([a=y]_M\), and, moreover, for all such \(a\) and \(y\) we have \([a=y]_A = [a=y]_M\). Thus \(c^A(a) = c^M(a) \upharpoonright|A|\), where here ‘\(\upharpoonright\)’ is used in the sense of the restriction of a function between two sets to a subset of its domain. Thus for all \(a\in |A|\) we have \(d(c^A(a)) = c^M(a)\).

It is immediate from what we have already shown that for all \(a\in |M|\) that we have \(Ea = \bigvee_{i\in I} \bigvee_{b\in |M|_i} [g_i(b) = a]_M\).

We thus have that \((d``cA,cM)\) is the directed colimit. ◻

Proof. By Proposition (32) it suffices to show that for all \(\bar{b}\in |M|^n\) we have \(E\phi \wedge E\bar{a} \wedge E\bar{b} \hskip 2pt\hskip 2pt\le [\phi(\bar{t},\bar{a})]_M\). So let \(\bar{b}\in |M|^n\) and let \(i\in I\) be such that \(\bar{b}\), \(\bar{a} \subseteq \mathop{\mathrm{rge}}(g_i)\). Let \(\bar{b}_i\) be such that \(g_i``\bar{b}_i = \bar{b}\).

By the hypothesis on \(M_i\) we have \(E\phi \wedge E\bar{a}_i \wedge E\bar{b}_i \hskip 2pt\hskip 2pt\le [\phi(\bar{b}_i,\bar{a}_i)]_{M_i}\) (again using Proposition (32)).

As \(g_i\) is a presheaf morphism \(E\bar{a} = E\bar{a}_i\) and \(E\bar{b}=E\bar{b}_i\). As \(g_i\) is an \(L\)-monomorphism, by Lemma (49) we have \([\phi(\bar{b}_i,\bar{a}_i)]_{M_i} \le [\phi(\bar{b},\bar{a})]_M\). Thus \(E\phi \wedge E\bar{a} \wedge E\bar{b} = E\phi \wedge E\bar{a}_i \wedge E\bar{b}_i \hskip 2pt\hskip 2pt\le [\phi(\bar{b},\bar{a}_i)]_{M_i} \le [\phi(\bar{b},\bar{a})]_M\), as required. ◻

Proof. Immediate from Proposition (56), the definition of elementary \(L\)-embedding and Theorem (58). ◻

Proof. See [2], Theorem 3.1 and Corollary 3.1. The proof given there is for complete Heyting algebras with countable character, countable languages and countable subsets of the model, but the alterations required for the general case (already envisaged in [2] and stated here) are trivial.

The clauses in the second paragraph of the statement are all immediate from Lemma (14) and Lemma (15). ◻

Proof.

The next lemma is where in the proof of Theorem (60) we have need of the constraint on \({\mathfrak C}\)-objects which are pairs consisting of a sheaf and a subsheaf that the subsheaves are of density no larger than the that of the larger sheaves.

Here we need also that the maps in the diagram, and hence the morphisms in the category, are in fact of the form required for Proposition (36). This is what restricts our results to categories whose morphisms are \(L\)-monomorphisms or elementary \(L\)-embeddings.

This completes the proof of the main two parts of the theorems.

The final paragraph of the theorem is now immediate from Lemma (65), or Lemma (66), and Lemma (67). ◻

Proof. The propositions are immediate from Corollary (68) and Corollary (69), respectively, by [3], Theorems (1.2) and (1.1). ◻