arXiv subjects

Davide Trotta

Publications and source records attributed to Davide Trotta.

22 records · Page 2Linked to original sources

arXiv2021

An algebraic approach to the completions of elementary doctrines

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.e. forcing equality on terms to coincide with the equality predicate), the one adding full comprehensions and the one adding quotients. We show that all these 2-adjunctions are 2-monadic and that the 2-monads arising from these adjunctions are all property-like. This entails that comprehensive diagonals, full comprehensions and quotients are algebraic properties of an elementary doctrine. Finally, we discuss and present the distributive laws between these 2-monads.

math.CT↗

arXiv2021

The existential completion

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 isomorphic to the 2-category of algebras for this 2-monad. We also show that the existential completion of an elementary doctrine is again elementary. Finally we extend the notion of exact completion of an elementary existential doctrine to an arbitrary elementary doctrine.

math.CT↗

arXiv2021

The Gödel Fibration

We introduce the notion of a Gödel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the existence of a prenex normal form presentation for every logical formula. Building up from Hofstra's earlier fibrational characterization of the de Paiva's categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a Gödel fibration. This result establishes an internal presentation of the dialectica construction. Then we provide a deep structural analysis of the Dialectica construction producing a full description of which categorical structure behaves well with respect to this construction, focusing on (weak) finite products and coproducts. We conclude describing the applications we envisage for this generalized fibrational version of the Dialectica construction.

math.CT↗

arXiv2021

Quantifier completions, choice principles and applications

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 the behaviour of the existential and universal quantifiers. We wish to convey the following points: the first is that these completions preserve the lattice structure and the distributive lattice structure of the fibres under opportune hypotheses which turn out to be preserved as well; the second regards the applications, in particular to the dialectica construction; the third is that these free constructions carry on some relevant choice principles.

math.CT↗