4 papers
The doctrinal Gödel's completeness theorem and the type space functor
Marco Abbadini, Francesca Guffanti
We give a self-contained proof of Gödel's completeness theorem entirely within the formalism of first-order Boolean doctrines (an algebraic approach to classical many-sorted first…
On the Beck--Chevalley condition
Marco Abbadini, Francesca Guffanti
Boolean hyperdoctrines provide an algebraic semantics for classical first-order logic with equality. In the definition of a Boolean hyperdoctrine, the Beck--Chevalley condition cap…
Freely adding one layer of quantifiers to a Boolean doctrine
Marco Abbadini, Francesca Guffanti
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 H…
Quantifier-free formulas and quantifier alternation depth in doctrines
Marco Abbadini, Francesca Guffanti
This paper aims to incorporate the notion of quantifier-free formulas modulo a first-order theory and the stratification of formulas by quantifier alternation depth modulo a first-…