Freely adding one layer of quantifiers to a Boolean doctrine
Marco Abbadini, Francesca Guffanti
TL;DR
The paper addresses how to freely add a single layer of quantifiers to a Boolean doctrine over a small category, formalizing a doctrinal version of Herbrand's theorem modulo a universal theory $\mathcal{T}$. It develops a quantifier-completion framework $\mathbf{P}^{\forall\exists}$ and identifies the depth-1 subdoctrine $\mathbf{P}^{\forall\exists}_1$ as the free QA-one-step Boolean doctrine over $\mathbf{P}$ via a generator-relations construction, ultimately proving $\mathbf{P}^{\forall\exists}_1 \cong \mathrm{Free}_1^{\mathbf{P}}$. A key technical advance is the semantic characterization of universally valid formulas through universal ultrafilters, along with the universal ultrafilter lemma and richness notion, which together enable doctrinal Herbrand-type reductions. The results yield a canonical, order-theoretic pathway to the first quantifier layer, with potential extensions to higher layers and connections to syntactic/doctrinal interpretations. Overall, the work provides a rigorous, categorical route to translating existential-quantifier gymnastics into a free, algebraic doctrine, with implications for how quantifier structure is managed in categorical logic and related semantic frameworks.
Abstract
We describe the layer of quantifier alternation depth at most one of the quantifier completion of a Boolean doctrine over a small category. This amounts to a doctrinal version of Herbrand's theorem for formulas with quantifier alternation depth at most one modulo a universal theory. The resulting construction satisfies a universal property that makes it the free QA-one-step Boolean doctrine. To achieve this version of Herbrand's theorem, we characterize, within the doctrinal setting, the classes $A$ of quantifier-free formulas for which there is a model $M$ such that $A$ is precisely the class of formulas whose universal closure is valid in $M$.