This talk aims to describe a first step toward 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 use the fact 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. Such sequences are in one-to-one correspondence with pairs consisting of a Boolean doctrine with quantifiers and a quantifier-free fragment of it.

This talk is based on a joint work with Marco Abbadini [1].

[1] M. Abbadini, F. Guffanti. Quantifier-free formulas and quantifier alternation depth in doctrines. Journal of Pure and Applied Algebra, Volume 229, Issue 8, 2025.