7 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-…
Left adjoint to precomposition in elementary doctrines
Francesca Guffanti
It is well-known in universal algebra that adding structure and equational axioms generates forgetful functors between varieties, and such functors all have left adjoints. The cate…
Rich doctrines and Henkin's Theorem
Francesca Guffanti
We find a possible interpretation of Henkin's Theorem in the language of existential implicational doctrines. Under some smallness assumption, starting from an implicational existe…
Adding a constant and an axiom to a doctrine
Francesca Guffanti
We study the meaning of "adding a constant to a language" for any doctrine, and "adding an axiom to a theory" for a primary doctrine, by showing how these are actually two instance…