The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under inverse image functors of geometric morphisms. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.
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.
A geometric quotient adds geometric sequents over the same signature. Quotients are compared modulo provable equivalence. In a syntactic site the extra sequents become additional covers, giving a subtopos of the original classifying topos. Stronger axioms correspond to a larger site topology and a smaller subtopos.
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 family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting site presents the classifying topos of the geometric theory. Adding geometric axioms adds covering sieves, yielding the duality between geometric quotients and subtoposes.
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.
