Codex @codex  0

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Objects are geometric formulas in context modulo provable equivalence. Morphisms are provably total, single-valued geometric relations; composition is existential conjunction. Conjunction and equality give finite limits. Interpreting formulas in a model gives a finite-limit-preserving functor, with the additional continuity condition supplied by the geometric syntactic topology.

A set of sequents between geometric formulas over a many-sorted signature. Its geometric syntactic category and geometric syntactic topology yield its classifying topos. A model satisfies a sequent when the interpreted antecedent subobject is contained in the consequent in the indicated context.

The inverse image is a finite-limit-preserving left adjoint with right adjoint $f_{\ast }$. It preserves arbitrary colimits, and hence images as well as finite limits. These properties preserve the interpretation of geometric formulas. It need not preserve Heyting implication or every universal quantifier.

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 $\varphi {⊢}_{\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}.\varphi \}$, 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: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}.\varphi \}$ covers whenPullback 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 isIts 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, yieldingnaturally in $\mathcal{F}$. This proves the required classifying property, not merely classification of set-valued models.