Abstract
Hyperdoctrines were introduced by F.W. Lawvere to synthesize the structural properties of logical systems [1, 2]. The intuition is that a hyperdoctrine determines an appropriate categorical structure to abstract both notions of first-order theory and interpretation. In some recent works [3], Maietti and Rosolini generalized the notion of hyperdoctrine, introducing that of elementary and existential doctrine, which allows specifying that of quotients.
The main goal of this talk is to present the existential completion of an elementary doctrine [4], its connections with some choice principles and applications [5]. In particular, employing choice principles, we characterize those existential doctrines which arise as an existential completion of an elementary one. Moreover, it turns out that an existential doctrine satisfies Hilbert’s epsilon rule if and only if it is an idempotent algebra for the 2-monad arising from the existential completion.
Finally, we present various examples of existential completions, including the doctrine of variations on a finite product category with weak equalizers, the subobject doctrine on a finitely complete category, and the doctrine of formal monomorphisms associated with an M-category.
References
[1] Lawvere, F. (1969). Adjointness in foundations. Dialectica, 23:281–296.
[2] Lawvere, F. (1970). Equality in hyperdoctrines and comprehension schema as an ad- joint functor. In Heller, A., editor, New York Symposium on Application of Categorical Algebra, volume 2, pages 1–14. American Mathematical Society.
[3] Maietti, M. and Rosolini, G. (2013). Quotient completion for the foundation of constructive mathematics. Log. Univers., 7(3):371–402.
[4] Trotta, D. (2020). The existential completion. Theory and Applications of Categories, 35(43).
[5] Trotta, D., Maietti, M., and Zorzi, M. (2020). Choice principles via completions. \
Davide Trotta
Assistant professor (RTDA)
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.