5 papers
Generalized existential completions and their regular and exact completions
Maria Emilia Maietti, Davide Trotta
This paper aims to apply the tool of generalized existential completions of conjunctive doctrines, concerning a class of morphisms of their base category, to deepen the study o…
Dialectica Logical Principles
Davide Trotta, Matteo Spadetto, Valeria de Paiva
Gödel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to o…
The existential completion
Davide Trotta
We determine the existential completion of a primary doctrine, and we prove that the 2-monad obtained from it is lax-idempotent, and that the 2-category of existential doctrines is…
An algebraic approach to the completions of elementary doctrines
Davide Trotta
We provide a thorough algebraic analysis of three known completions having a central role in the exact completions of Lawvere's doctrines: the one adding comprehensive diagonals (i…
Quantifier completions, choice principles and applications
Davide Trotta, Matteo Spadetto
We contribute to the knowledge of the quantifier completions and their applications by using the language of doctrines. This algebraic presentation allows us to properly analyse th…