Quantifier-free formulas and quantifier alternation depth in doctrines

This paper aims at providing a first step towards a doctrinal approach to quantifier-free formulas and quantifier alternation depth modulo a first-order theory. The set of quantifier-free formulas modulo a first-order theory is axiomatized by what we call a quantifier-free fragment of a Boolean doctrine with quantifiers. Rather than being an intrinsic notion, a quantifier-free fragment is an additional structure on a Boolean doctrine with quantifiers. Under a smallness assumption, the structures occurring as quantifier-free fragments of some Boolean doctrines with quantifiers are precisely the Boolean doctrines (without quantifiers). To obtain this characterization, we prove that every Boolean doctrine over a small base category admits a quantifier completion, of which it is a quantifier-free fragment. Furthermore, the stratification by quantifier alternation depth of first-order formulas motivates the introduction of quantifier alternation stratified Boolean doctrines. While quantifier-free fragments are defined in relation to an "ambient" Boolean doctrine with quantifiers, a quantifier alternation stratified Boolean doctrine requires no such ambient doctrine. Indeed, it consists of a sequence of Boolean doctrines (without quantifiers) with connecting axioms. We show such sequences to be in one-to-one correspondence with pairs consisting of a Boolean doctrine with quantifiers and a quantifier-free fragment of it.
Comment: Comments are welcome! (This is the second version of a much longer manuscript. For better readability, we extracted and expanded the first part of the previous version. In this version we left out Section 5-6 and both Appendices of the original manuscript, which we plan to ripropose in some new form in the future.)