On the Beck--Chevalley condition

Abstract

Boolean hyperdoctrines provide an algebraic semantics for classical first-order logic with equality. In the definition of a Boolean hyperdoctrine, the Beck--Chevalley condition captures the commutativity of substitutions with quantifiers and with equality. Often, a generalization of these conditions is considered, which requires the commutativity of an appropriate square for every pullback square in the base category. A Boolean hyperdoctrine satisfying this condition is called full. Our contribution is twofold. On the negative side, we exhibit a non-full Boolean hyperdoctrine. On the positive side, we show that every Boolean hyperdoctrine $\mathsf{FinSet}\to \mathsf{BA}$ over ${\mathsf{FinSet}}^{\mathrm{op}}$ is full.