A topological completeness theorem (Q1283128)

By definition, a geometric theory \(T\) is a theory such that all its axioms are equivalent to formulas of the form \(\forall \overline{y} (\psi_1(\overline{y})\to \psi_2(\overline{y}))\) for geometric formulas \(\psi_1\) and \(\psi_2\), where a geometric formula is built up by atomic formulas, finite conjunction, arbitrary disjunction, the truth values true and false, and existence quantification. A geometric theory \(T\) satisfies by definition the completeness theorem, if a given geometric sequent holds in all models of \(T\) in all Grothendieck toposes. A geometric morphism \(\varphi : \text{Sh}({\mathcal D}, J)\to \text{Sh}({\mathcal C},K)\) between Grothendieck toposes is a pair of functors \[ \varphi_*:\text{Sh}({\mathcal D},K)\to \text{Sh}({\mathcal C},K),\quad \text{Sh}({\mathcal D},J)\leftarrow \text{Sh}({\mathcal C},J) :\varphi^* \] such that \(\varphi^*\) is left adjoint to \(\varphi_*\) and \(\varphi^*\) is left exact. \(\varphi^*\) is called the inverse image and \(\varphi_*\) the direct image. The aim of the paper is to prove a topological completeness theorem as follows: There exist a topological space \(X\) and an \({\mathcal O}X\)-valued model \(\Phi\) of any geometric theory \(T\) satisfying the completeness theorem in \(\text{Sh}(X)\) corresponding to a geometric morphism \(\varphi:\text{Sh}(X)\to {\mathcal B}(T)\) such that the following statements are true: (i) The geometric morphism \(\varphi\) is an open surjection. (ii) Every map in \(\text{Sh}(X)\) between first-order definable sheaves is geometrically definable (functional completeness). (iii) The inverse image \(\varphi^*\) preserves function types of first order definable types. \({\mathcal B}(T)\) denotes in this connection the Grothendieck topos determined by \(T\) in a certain manner. Moreover, the inverse image \(\varphi^*\) preserves the interpretation of first-order formulas.