Abstract

In universal Boolean doctrines, by design, there is no structure that allows one to identify the quantifier depth of formulas, i.e. the level of nesting of quantifiers. For example, we don’t have any information about what formulas are considered to be quantifier-free. In response to an invitation by M. Gehrke at the conference Category Theory 20->21, we introduce the notion of a quantifier-stratified universal Boolean doctrine. This notion requires additional structure on a universal Boolean doctrine, accounting for the quantifier alternation depth of formulas. This is motivated by the extensive usage of induction on the quantifier depth in applications related to first-order logic.

After proving that every Boolean doctrine over a small base category admits a quantifier completion, we show how to freely add the first layer of quantifier alternation depth to one such doctrine. This amounts to a doctrinal generalization of Herbrand’s theorem in classical first-order logic. To achieve this version of Herbrand’s theorem, we characterize, within the doctrinal setting, the classes of quantifier-free formulas whose universal closure is valid in some common model.