Quantifier completions, choice principles and applications

TL;DR

This paper explores the algebraic structure of quantifier completions using doctrines, analyzing their properties, preservation of lattice structures, and applications such as the dialectica construction, highlighting their relevance to choice principles.

Contribution

It provides a novel algebraic framework for understanding quantifier completions and their behavior, with applications to dialectica constructions and choice principles.

Findings

Quantifier completions preserve lattice and distributive lattice structures.

Applications to dialectica construction demonstrate the utility of these completions.

Free constructions maintain relevant choice principles.

Abstract

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.