Francesca Guffanti

Freely adding one layer of quantifiers to a Boolean doctrine

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 theo...