Model theory

The Interpolation Theorem

content/model-theory/interpolation/interpolation.tex

% Part: model-theory% Chapter: interpolation\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{mod}{int}{The Interpolation Theorem}\olimport{introduction}\olimport{separation}\olimport{interpolation-proof}\olimport{definability}\OLEndChapterHook\end{document}

content/model-theory/interpolation/introduction.tex

% Part: model-theory% Chapter: interpolation% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{int}{int}\olsection{Introduction}The interpolation theorem is the following result: Suppose$\Entails !A \lif !B$. Then there is !!a{sentence} $!C$ such that$\Entails !A \lif !C$ and $\Entails !C \lif !B$.  Moreover, every!!{constant}, !!{function}, and !!{predicate} (other than $\eq$) in$!C$ occurs both in $!A$ and~$!B$. The !!{sentence} $!C$ is called an\emph{interpolant} of $!A$ and~$!B$.The interpolation theorem is interesting in its own right, but itsmain importance lies in the fact that it can be used to prove resultsabout definability in a theory, and the conditions under whichcombining two consistent theories results in a consistent theory.  Thefirst result is known as the Beth definability theorem; the second,Robinson's joint consistency theorem.\end{document}

content/model-theory/interpolation/separation.tex

% Part: model-theory% Chapter: interpolation% Section: separation\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{int}{sep}\olsection{Separation of \printtoken{P}{sentence}}A bit of groundwork is needed before we can proceed with the proof ofthe interpolation theorem. An interpolant for $!A$ and $!B$ is!!a{sentence}~$!C$ such that $!A \Entails !C$ and $!C \Entails !B$.By contraposition, the latter is true iff $\lnot !B \Entails \lnot!C$. !!^a{sentence}~$!C$ with this property is said to \emph{separate}$!A$ and $\lnot !B$.  So finding an interpolant for $!A$ and $!B$amounts to finding !!a{sentence} that separates $!A$ and $\lnot !B$.As so often, it will be useful to consider a generalization: asentence that separates two \emph{sets} of !!{sentence}s.\begin{defn}A sentence $!C$ \emph{separates} sets of sentences $\Gamma$ and$\Delta$ if and only if $\Gamma \Entails !C$ and $\Delta \Entails\lnot !C$. If no such !!{sentence} exists, then $\Gamma$ and $\Delta$are \emph{inseparable}.\end{defn}The inclusion relations between the classes ofmodels of $\Gamma$, $\Delta$ and $!C$ are represented below:\begin{figure}[h]  \centering  \begin{tikzpicture}[node distance=2cm, auto, thick]    \draw [rounded corners] (0,0) -- (6,0) -- (6,3) -- (0,3) --  cycle;    \draw (1.5,1.5) circle (0.9cm);    \draw (4.5,1.5) circle (0.9cm);    \path node at (1.5,1.5) {\Large $\Gamma$};     \path node at (4.5,1.5) {\Large $\Delta$};     \path node at (0.4,2.6) {\Large $\formula{C}$};    \path node at (3.4,0.4) {\Large $\lnot \formula{C}$};    \draw (2.5,0) .. controls (2.5,1.5) and (3.5,1.5) .. (3.5,3);  \end{tikzpicture}  \caption{$!C$ separates $\Gamma$ and $\Delta$}  \ollabel{fig:sep}\end{figure}\begin{lem}\ollabel{lem:sep1}Suppose $\Lang{L}_0$ is the language containing every !!{constant},!!{function} and !!{predicate} (other than $\doteq$) that occurs in\emph{both} $\Gamma$ and $\Delta$, and let $\Lang{L}'_0$ be obtainedby the addition of infinitely many new !!{constant}s $\Obj c_n$ for $n\ge 0$. Then if $\Gamma$ and $\Delta$ are inseparable in $\Lang{L}_0$,they are also inseparable in $\Lang{L}'_0$.\end{lem}\begin{proof}We proceed indirectly: suppose by way of contradiction that $\Gamma$and $\Delta$ are separated in $\Lang{L}'_0$. Then $\Gamma \Entails\Subst{!C}{c}{x}$ and $\Delta \Entails \lnot \Subst{!C}{c}{x}$ for some $!C \in\Lang{L}_0$ (where $c$ is a new !!{constant}---the case where $!C$contains more than one such new !!{constant} is similar). Bycompactness, there are \emph{finite} subsets $\Gamma_0$ of $\Gamma$and $\Delta_0$ of $\Delta$ such that $\Gamma_0 \Entails \Subst{!C}{c}{x}$and $\Delta_0 \Entails \lnot \Subst{!C}{c}{x}$. Let $!G$ be theconjunction of all !!{formula}s in $\Gamma_0$ and $!H$ theconjunction of all !!{formula}s in $\Delta_0$. Then\begin{align*}  !G & \Entails \Subst{!C}{c}{x}, & !H  \Entails \lnot \Subst{!C}{c}{x}.\end{align*}From the former, by Generalization, we have $!G \Entails\lforall[x][!C]$, and from the latter by contraposition,$\Subst{!C}{c}{x} \Entails \lnot !H$, whence also $\lforall[x][!C]\Entails \lnot \delta$. Contraposition again gives $!H \Entails\lnot \lforall[x][!C]$. By monotonicity,\begin{align*}  \Gamma &\Entails \lforall[x][!C], &   \Delta & \Entails \lnot \lforall[x][!C],\end{align*}so that $\lforall[x][!C]$ separates $\Gamma$ and $\Delta$ in$\Lang{L}_0$. \end{proof}\begin{lem}\ollabel{lem:sep2}Suppose that $\Gamma \cup \{ \lexists[x][!S] \}$ and $\Delta$ areinseparable, and $c$ is a new !!{constant} not in $\Gamma$, $\Delta$,or $!S$. Then $\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$and $\Delta$ are also inseparable.\end{lem}\begin{proof}Suppose for contradiction that $!C$ separates $\Gamma \cup \{\lexists[x][!S], \Subst{!S}{c}{x}\}$ and $\Delta$, while at the sametime $\Gamma \cup \{\lexists[x]{!S} \}$ and $\Delta$ areinseparable. We distinguish two cases:\begin{enumerate}\item $c$ does not occur in $!C$: in this case $\Gamma \cup  \{\lexists[x][!S], \lnot!C \}$ is satisfiable (otherwise $!C$  separates $\Gamma \cup \{\lexists[x][!S] \}$ and $\Delta$). It  remains so if $\Subst{!S}{c}{x}$ is added, so $!C$ does not separate  $\Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$ and $\Delta$  after all.\item $c$ does occur in $!C$ so that $!C$ has the form  $\Subst{!C}{c}{x}$. Then we have that  \[  \Gamma \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}\} \Entails \Subst{!C}{c}{x},  \]  whence $\Gamma, \lexists[x][!S] \Entails \lforall[x][(!S \lif !C)]$  by the Deduction Theorem and Generalization, and finally $\Gamma  \cup \{ \lexists[x][!S] \} \Entails \lexists[x][!C]$. On the other  hand, $\Delta \Entails \lnot \Subst{!C}{c}{x}$ and hence by  Generalization $\Delta \Entails \lnot \lexists[x][!C]$. So $\Gamma  \cup \{\lexists[x][!S] \}$ and $\Delta$ are separable, a  contradiction.\end{enumerate}\end{proof}\end{document}

content/model-theory/interpolation/interpolation-proof.tex

% Part: model-theory% Chapter: interpolation% Section: interpolation-proof\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{int}{prf}\olsection{Craig's Interpolation Theorem}\begin{thm}[Craig's Interpolation Theorem]\ollabel{thm:interpol} If $\Entails !A \lif !B$, then there is !!a{sentence} $!C$ such that$\Entails !A \lif !C$ and $\Entails !C \lif !B$, and every!!{constant}, !!{function}, and !!{predicate} (other than $\eq$) in$!C$ occurs both in $!A$ and~$!B$. The !!{sentence} $!C$ is called an\emph{interpolant} of $!A$ and~$!B$.\end{thm}\begin{proof}Suppose $\Lang{L}_1$ is the language of $!A$ and $\Lang{L}_2$ is thelanguage of $!B$. Let $\Lang{L}_0 = \Lang{L}_1 \cap \Lang{L}_2$. Foreach $i \in \{0, 1, 2 \}$, let $\Lang{L}'_i$ be obtained from$\Lang{L}_i$ by adding the infinitely many new !!{constant}s $\Obj c_0,\Obj c_1, \Obj c_2, \dots$. If $!A$ is unsatisfiable, $\lexists[x][\eq/[x][x]]$ is aninterpolant. If $\lnot !B$ is unsatisfiable (and hence $!B$ is valid),$\lexists[x][\eq[x][x]]$ is an interpolant. So we may assume also thatboth $!A$ and $\lnot !B$ are satisfiable.In order to prove the contrapositive of the Interpolation Theorem,assume that there is no interpolant for $!A$ and $!B$. In other words,assume that $\{!A\}$ and $\{\lnot !B\}$ are inseparable in$\Lang{L}_0$.Our goal is to extend the pair $(\{ !A \}, \{\lnot!B\})$ to amaximally inseparable pair $(\Gamma^*, \Delta^*)$.  Let $!A_0$,$!A_1$, $!A_2$, \dots enumerate the !!{sentence}s of $\Lang{L}_1$, and$!B_0$, $!B_1$, $!B_2$, \dots enumerate the !!{sentence}sof~$\Lang{L}_2$. We define two increasing sequences of sets of!!{sentence}s $(\Gamma_n, \Delta_n)$, for $n \ge 0$, as follows. Put$\Gamma_0 = \{ !A\}$ and $\Delta_0 = \{\lnot !B \}$. Assuming$(\Gamma_n, \Delta_n)$ are already defined, define $\Gamma_{n+1}$ and$\Delta_{n+1}$ by:\begin{enumerate}\item If $\Gamma_n \cup \{!A_n \}$ and $\Delta_n$ are inseparable in  $\Lang{L}'_0$, put $!A_n$ in $\Gamma_{n+1}$. Moreover, if $!A_n$ is  an existential !!{formula} $\lexists[x][!S]$ then pick a new  !!{constant} $c$ not occurring in $\Gamma_n$, $\Delta_n$, $!A_n$ or  $!B_n$, and put $\Subst{!S}{c}{x}$ in $\Gamma_{n+1}$.\item If $\Gamma_{n+1}$ and $\Delta_n \cup \{!B_n \}$ are inseparable  in $\Lang{L}'_0$, put $!B_n$ in $\Delta_{n+1}$. Moreover, if $!B_n$  is an existential !!{formula} $\lexists[x][!S]$, then pick a new  !!{constant} $c$ not occurring in $\Gamma_{n+1}$, $\Delta_n$, $!A_n$  or $!B_n$, and put $\Subst{!S}{c}{x}$ in $\Delta_{n+1}$.\end{enumerate}Finally, define:\begin{align*}  \Gamma^* & = \bigcup_{n\ge 0} \Gamma_n, &   \Delta^* & = \bigcup_{n\ge 0} \Delta_n.\end{align*}By simultaneous induction on $n$ we can now prove:\begin{enumerate}\item\ollabel{part-a} $\Gamma_n$ and $\Delta_n$ are inseparable in  $\Lang{L}'_0$;\item\ollabel{part-b} $\Gamma_{n+1}$ and $\Delta_n$ are inseparable in    $\Lang{L}'_0$.\end{enumerate}The basis for \olref{part-a} is given by \olref[sep]{lem:sep1}. Forpart \olref{part-b}, we need to distinguish three cases:\begin{enumerate}\item If $\Gamma_0 \cup \{!A_0 \}$ and $\Delta_0$ are separable, then  $\Gamma_1 = \Gamma_0$ and \olref{part-b} is just \olref{part-a};\item If $\Gamma_1 = \Gamma_0 \cup\{ !A_0\}$, then $\Gamma_1$ and  $\Delta_0$ are inseparable by construction.\item It remains to consider the case where $!A_0$ is existential, so  that $\Gamma_1 = \Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x}  \}$. By construction, $\Gamma_0 \cup \{ \lexists[x][!S]\}$ and  $\Delta_0$ are inseparable, so that by \olref[sep]{lem:sep2} also  $\Gamma_0 \cup \{ \lexists[x][!S], \Subst{!S}{c}{x} \}$ and  $\Delta_0$ are inseparable.\end{enumerate}This completes the basis of the induction for \olref{part-a} and\olref{part-b} above. Now for the inductive step. For \olref{part-a}, if$\Delta_{n+1} = \Delta_n \cup \{ !B_n \}$ then $\Gamma_{n+1}$ and$\Delta_{n+1}$ are inseparable by construction (even when $!B_n$ isexistential, by \olref[sep]{lem:sep2}); if $\Delta_{n+1} = \Delta_n$(because $\Gamma_{n+1}$ and $\Delta_n \cup \{!B_n\}$ are separable),then we use the induction hypothesis on \olref{part-b}. For theinductive step for \olref{part-b}, if $\Gamma_{n+2} = \Gamma_{n+1} \cup\{!A_{n+1} \}$ then $\Gamma_{n+2}$ and $\Delta_{n+1}$ areinseparable by construction (even when $!A_{n+1}$ is existential,by \olref[sep]{lem:sep2}); and if  $\Gamma_{n+2} = \Gamma_{n+1}$ thenwe use the inductive case for \olref{part-a} just proved. Thisconcludes the induction on \olref{part-a} and \olref{part-b}. It follows that $\Gamma^*$ and $\Delta^*$ are inseparable; if not, bycompactness, there is $n \ge 0$ that separates $\Gamma_n$ and$\Delta_n$, against \olref{part-a}. In particular, $\Gamma^*$ and$\Delta^*$ are consistent: for if the former or the latter isinconsistent, then they are separated by $\lexists[x][\eq/[x][x]]$ or  $\lforall[x][\eq[x][x]]$, respectively.We now show that $\Gamma^*$ is maximally consistent in$\Lang{L}'_1$ and likewise $\Delta^*$ in $\Lang{L}'_2$. For theformer, suppose that $!A_n \notin \Gamma^*$ and $\lnot !A_n\notin \Gamma^*$, for some $n \ge 0$. If $!A_n \notin \Gamma^*$then $\Gamma_n \cup \{!A_n \}$ is separable from $\Delta_n$, andso there is $!C \in \Lang{L}'_0$ such that both:\begin{align*}  \Gamma^* & \Entails !A_n \lif !C, &   \Delta^* & \Entails \lnot !C.\end{align*}Likewise, if $\lnot !A_n \notin \Gamma^*$, there is $!C' \in\Lang{L}'_0$ such that both:\begin{align*}  \Gamma^* & \Entails \lnot !A_n \lif !C', &   \Delta^* & \Entails \lnot !C'.\end{align*}By propositional logic, $\Gamma^* \Entails !C \lor !C'$ and$\Delta^* \Entails \lnot (!C \lor !C')$, so $!C \lor!C'$ separates $\Gamma^*$and $\Delta^*$. A similar argumentestablishes that $\Delta^*$ is maximal. Finally, we show that $\Gamma^* \cap \Delta^*$ is maximally consistentin $\Lang{L}'_0$. It is obviously consistent, since it is theintersection of consistent sets. To show maximality, let $!S \in\Lang{L}'_0$. Now, $\Gamma^*$ is maximal in $\Lang{L'_1}\supseteq \Lang{L'_0}$, and similarly $\Delta^*$ is maximal in$\Lang{L'_2} \supseteq \Lang{L'_0}$. It follows that either$!S \in \Gamma^*$ or $\lnot !S \in \Gamma^*$, and either$!S \in \Delta^*$ or $\lnot !S \in \Delta^*$. If $!S \in\Gamma^*$ and $\lnot !S \in \Delta^*$ then $!S$ wouldseparate $\Gamma^*$ and $\Delta^*$; and if $\lnot !S \in\Gamma^*$ and $!S \in \Delta^*$ then $\Gamma^*$ and $\Delta^*$would be separated by $\lnot !S$. Hence, either $!S \in\Gamma^* \cap \Delta^*$ or $\lnot !S \in \Gamma^* \cap \Delta^*$,and $\Gamma^* \cap \Delta^*$ is maximal. Since $\Gamma^*$ is maximally consistent, it has a model$\Struct{M}'_1$ whose !!{domain} $\Domain{M'_1}$ comprises all andonly the elements $\Assign{c}{M'_1}$ interpreting the!!{constant}s---just like in the proof of the completeness theorem(\olref[fol][com][cth]{thm:completeness}). Similarly, $\Delta^*$ has amodel $\Struct{M}'_2$ whose !!{domain} $\Domain{M'_2}$ is given by theinterpretations $\Assign{c}{M'_2}$ of the !!{constant}s.Let $\Struct{M_1}$ be obtained from $\Struct{M'_1}$ by droppinginterpretations for !!{constant}s, !!{function}s, and !!{predicate}s in$\Lang{L'_1} \setminus \Lang{L'_0}$, and similarly for$\Struct{M_2}$. Then the map $h \colon M_1 \to M_2$ defined by$h(\Assign{c}{M'_1}) = \Assign{c}{M'_2}$ is anisomorphism in $\Lang{L}'_0$, because $\Gamma^* \cap \Delta^*$ ismaximally consistent in $\Lang{L}'_0$, as shown. This followsbecause any $\Lang{L}'_0$-!!{sentence} either belongs to both$\Gamma^*$ and $\Delta^*$, or to neither: so $\Assign{c}{M'_1} \in\Assign{P}{M'_1}$ if and only if $\Atom{P}{c} \in \Gamma^*$ if and only if$\Atom{P}{c} \in \Delta^*$ if and only if $\Assign{c}{M'_2} \in\Assign{P}{M'_2}$. The other conditions satisfied by isomorphismscan be established similarly.Let us now define a model $\Struct{M}$ for the !!{language}$\Lang{L_1} \cup \Lang{L_2}$ as follows:\begin{enumerate}\item The !!{domain} $\Domain{M}$ is just $\Domain{M_2}$, i.e., the  set of all elements $\Assign{c}{M'_2}$; \item If !!a{predicate}~$P$ is in $\Lang{L_2} \setminus  \Lang{L_1}$ then $\Assign{P}{M} = \Assign{P}{M'_2}$;\item If a predicate $P$ is in $\Lang{L}_1\setminus \Lang{L}_2$ then  $\Assign{P}{M} = h(\Assign{P}{M'_2})$, i.e.,  $\tuple{\Assign{c_1}{M'_2}, \dots, \Assign{c_n}{M'_2}} \in  \Assign{P}{M}$ if and only if $\tuple{\Assign{c_1}{M'_1}, \dots,  \Assign{c_n}{M'_1}} \in \Assign{P}{M'_1}$.\item If !!a{predicate} $P$ is in $\Lang{L}_0$ then $\Assign{P}{M} =  \Assign{P}{M'_2} = h(\Assign{P}{M'_1})$. \item !!^{function}s of $\Lang{L}_1 \cup \Lang{L}_2$, including  !!{constant}s, are handled similarly.\end{enumerate}Finally, one shows by induction on !!{formula}s that $\Struct{M}$ agreeswith $\Struct{M'_1}$ on all !!{formula}s of $\Lang{L'_1}$ and with$\Struct{M'_2}$ on all !!{formula}s of $\Lang{L'_2}$. In particular,$\Struct{M} \Entails \Gamma^* \cup \Delta^*$, whence $\Struct{M}\Entails !A$ and $\Struct{M} \Entails \lnot!B$, and$\not\Entails !A \lif !B$. This concludes the proof ofCraig's Interpolation Theorem.\end{proof}\end{document}

content/model-theory/interpolation/definability.tex

% Part: model-theory% Chapter: interpolation% Section: definability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{int}{def}\olsection{The Definability Theorem}One important application of the interpolation theorem is Beth'sdefinability theorem.  To define an $n$-place relation~$R$ we can give!!a{formula}~$!C$ with $n$ free !!{variable}s which does notinvolve~$R$. This would be an \emph{explicit} definition of~$R$ interms of~$!C$.  We can then say also that a theory~$\Sigma(P)$ in a!!{language} containing the $n$-place !!{predicate}~$P$ explicitlydefines~$P$ if it contains (or at least entails) a formalized explicitdefinition, i.e.,\[\Sigma(P) \Entails \lforall[x_1][\dots  \lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1, \dots,    x_n))]].\]But an explicit definition is only one way of defining---in the senseof determining completely---a relation.  A theory may also be suchthat the interpretation of~$P$ is fixed by the interpretation of therest of the !!{language} in any model.  The definability theoremstates that whenever a theory fixes the interpretation of~$P$ in thisway---whenever it \emph{implicitly defines}~$P$---then it alsoexplicitly defines it.\begin{defn}Suppose $\Lang{L}$ is !!a{language} not containing the!!{predicate}~$P$.  A set $\Sigma(P)$ of !!{sentence}s of $\Lang{L}\cup \{P\}$ \emph{explicitly defines}~$P$ if and only if there is!!a{formula}~$!C(x_1, \dots, x_n)$ of $\Lang{L}$ such that\[\Sigma(P) \Entails \lforall[x_1][\dots  \lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1, \dots,    x_n))]].\]\end{defn}\begin{defn}Suppose $\Lang{L}$ is !!a{language} not containing the!!{predicate}s~$P$ and~$P'$.  A set $\Sigma(P)$ of !!{sentence}s of$\Lang{L} \cup \{P\}$ \emph{implicitly defines} $P$ if and only if\[\Sigma(P) \cup \Sigma(P') \Entails \lforall[x_1][\dots  \lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff \Atom{P'}{x_1,\dots,      x_n})]],\]where $\Sigma(P')$ is the result of uniformly replacing $P$ with $P'$in $\Sigma(P)$.\end{defn}In other words, for any model $\Struct{M}$ and $R, R' \subseteq\Domain{M}^n$, if both $\Expan{M}{R} \Entails \Sigma(P)$ and$\Expan{M}{R'} \Entails \Sigma(P')$, then $R=R'$; where$\Expan{M}{R}$ is the !!{structure}~$\Struct{M'}$ for theexpansion of $\Lang{L}$ to $\Lang{L} \cup \{P\}$ such that$\Assign{P}{M'} = R$, and similarly for $\Expan{M}{R'}$.\begin{thm}[Beth Definability Theorem] A set $\Sigma(P)$ of $\Lang{L}  \cup\{P\}$-!!{formula}s implicitly defines $P$ if and only $\Sigma(P)$  explicitly defines $P$.\end{thm}\begin{proof}If $\Sigma(P)$ explicitly defines $P$ then both\begin{align*}  \Sigma(P) & \Entails & \lforall[x_1][\dots \lforall[x_n]    [(\Atom{P}{x_1,\dots, x_n} \liff !C(x_1,\dots,x_n))]]\\  \Sigma(P') & \Entails & \lforall[x_1][\dots \lforall[x_n]    [(\Atom{P'}{x_1,\dots, x_n} \liff !C(x_1,\dots,x_n))]]\end{align*}and the conclusion follows. For the converse: assume that $\Sigma(P)$implicitly defines $P$. First, we add !!{constant}s $c_1$, \dots,~$c_n$ to$\Lang{L}$. Then\[\Sigma(P) \cup \Sigma(P') \Entails\Atom{P}{c_1, \dots, c_n} \to  \Atom{P'}{c_1, \dots, c_n}.\]By compactness, there are finite sets $\Delta_0 \subseteq \Sigma(P)$and $\Delta_1 \subseteq \Sigma(P')$ such that\[\Delta_0 \cup \Delta_1 \Entails\Atom{P}{c_1, \dots, c_n} \to \Atom{P'}{c_1, \dots, c_n}.\]Let $!D(P)$ be the conjunction of all !!{sentence}s $!A(P)$ such thateither $!A(P) \in \Delta_0$ or $!A(P') \in \Delta_1$ and let $!D(P')$be the conjunction of all !!{sentence}s $!A(P')$ such that either$!A(P) \in \Delta_0$ or $!A(P') \in \Delta_1$. Then $!D(P) \land!D(P') \Entails \Atom{P}{c_1, \dots, c_n} \to P'c_1\dots c_n$. We canre-arrange this so that each !!{predicate} occurs on one side of$\Entails$:\[!D(P) \land \Atom{P}{c_1, \dots, c_n} \Entails!D(P') \to \Atom{P'}{c_1, \dots, c_n}.\]By Craig's Interpolation Theorem there is !!a{sentence} $!C(c_1,\dots, c_n)$not containing $P$ or $P'$ such that:\begin{align*}  !D(P) \land \Atom{P}{c_1, \dots, c_n} & \Entails !C(c_1,\dots, c_n); \\  !C(c_1,\dots, c_n) & \Entails !D(P') \to \Atom{P'}{c_1, \dots, c_n}.\end{align*}From the former of these two entailments we have: $!D(P) \Entails\Atom{P}{c_1,\dots, c_n} \lif !C(c_1,\dots, c_n)$. And from thelatter, since an $\Lang{L} \cup \{P\}$-model $\Expan{M}{R}\Entails !A(P)$ if and only if the corresponding $\Lang{L} \cup\{P'\}$-model $\Expan{M}{R} \models !A(P')$, we have$!C(c_1,\dots, c_n) \Entails !D(P) \lif \Atom{P}{c_1,\dots, c_n}$,from which:\[!D(P) \Entails !C(c_1,\dots,c_n) \to \Atom{P}{c_1,\dots, c_n}.\]Putting the two together, $!D(P) \Entails \Atom{P}{c_1,\dots, c_n}\liff !C(c_1, \dots, c_n)$, and by monotonicity and generalization also\[\Sigma(P) \Entails\lforall[x_1][\dots\lforall[x_n][(\Atom{P}{x_1,\dots, x_n} \liff    !C(x_1,\dots, x_n))]].\]\end{proof}\end{document}