2026/07/23 by Marco Abbadini, Francesca Guffanti
#math.LO #math.CT
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-order logic). Moreover, we show that Gödel's completeness theorem entails that the fiberwise Stone dual of a first-order Boolean doctrine is its type space functor; roughly speaking, this means that the Stone dual of the Boolean algebra of formulas in context X is the Stone space of X-pointed models modulo elementary equivalence.