Freely adding one layer of quantifiers to a Boolean doctrine

TL;DR

This paper introduces a new layer of quantifiers for Boolean doctrines, providing a doctrinal version of Herbrand's theorem for formulas with limited quantifier complexity, and characterizes models for these formulas.

Contribution

It defines the free QA-one-step Boolean doctrine with a universal property, extending Herbrand's theorem to a categorical setting with quantifier depth at most one.

Findings

Characterizes classes of quantifier-free formulas with models.

Establishes a universal property for the free QA-one-step Boolean doctrine.

Provides a doctrinal version of Herbrand's theorem.

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