= Solution
A <geometric formula> is built from atomic formulas, including equality, using finite conjunctions, arbitrary set-indexed disjunctions and existential quantification in a finite variable context. Truth is the empty conjunction and falsity the empty disjunction. A <geometric theory> is a set of sequents $\phi\vdash_{\vec x}\psi$ between such formulas over a many-sorted signature. The context supplies the universal force of an axiom; unrestricted universal quantification, implication and negation are not formula constructors in this fragment.
These choices are exactly suited to <inverse image functors of geometric morphisms>. Finite-limit preservation handles equality and conjunction; <colimit> and image preservation handle disjunction and existential quantification. Therefore an inverse image carries an internal model of a <geometric theory> to another model.
Construct the <geometric syntactic category> $\mathcal C_{\mathbb T}$ as follows. Objects are formulas in context $\{\vec x.\phi\}$, modulo provable renaming and equivalence. A morphism to $\{\vec y.\psi\}$ is an equivalence class of formulas $\theta(\vec x,\vec y)$ that are provably total and single-valued:
$$
\theta\vdash\phi\wedge\psi,\qquad
\phi\vdash_{\vec x}\exists\vec y\,\theta,\qquad
\theta(\vec x,\vec y)\wedge\theta(\vec x,\vec y')
\vdash_{\vec x,\vec y,\vec y'}\vec y=\vec y'.
$$
The last notation abbreviates componentwise equality. Identity is equality of the context variables; composition is existential conjunction over the intermediate tuple. The category has <finite limits>, formed through conjunction and equality.
Give it the <geometric syntactic topology> $J_{\mathbb T}$. A family of arrows represented by $\theta_i(\vec y_i,\vec x)$ into $\{\vec x.\phi\}$ covers when
$$
\mathbb T\vdash_{\vec x}
\phi\ \Longrightarrow\ \bigvee_i\exists\vec y_i\,\theta_i(\vec y_i,\vec x).
$$
Pullback stability is substitution, and transitivity comes from distributing existential conjunction through the covering disjunctions. Thus the generated sieves define a <Grothendieck topology>. Empty covers impose the interpretation of falsity as the <initial object>.
The <classifying topos> is
$$
\boxed{\mathbf{Set}[\mathbb T]=
\mathbf{Sh}(\mathcal C_{\mathbb T},J_{\mathbb T}).}
$$
Its universal model $U_{\mathbb T}$ assigns a sort $A$ the sheafified representable of $\{x^A.\top\}$, functions their definable graph morphisms and relations their definable <subobjects>. The syntactic covering conditions make the axioms valid in this model.
For the universal property, interpreting formulas in a model $M$ in a <Grothendieck topos> $\mathcal F$ gives a finite-limit-preserving, $J_{\mathbb T}$-continuous <functor> $\mathcal C_{\mathbb T}\to\mathcal F$: covers go to jointly epimorphic families precisely because the relevant sequents hold. The <Diaconescu equivalence for geometric morphisms> associates to this <functor> a <geometric morphism> $\mathcal F\to\mathbf{Set}[\mathbb T]$. Conversely, pulling $U_{\mathbb T}$ back along a <geometric morphism> gives a model. The constructions on models and their homomorphisms are inverse up to <natural isomorphism>, yielding
$$
\boxed{\operatorname{Geom}(\mathcal F,\mathbf{Set}[\mathbb T])
\simeq\mathbb T\operatorname{-Mod}(\mathcal F)}
$$
naturally in $\mathcal F$. This proves the required classifying property, not merely classification of set-valued models.
Back to article page
