A characterization of generalized existential completions (Q2683780)

This paper aims to provide an intrinsic characterization of the notion of \textit{generalized existential completion} of a conjunctive doctrine \(P\) relative to a suitable class \(\Lambda\) of morphisms of the base category of \(P\). The cornerstone of the result consists in an algebraic description of the logical concept of existential free formulae closely connected to the validity of some choice principles. The link between the characterization here and choice principles is emphasized by the fact that an existential doctrine \(P\) is the generalized existential completion of itself for all the projections of its base iff \(P\) is rigged out in Hilbert's epsilon operators. The synopsis of the paper goes as follows. \begin{itemize} \item[\S 2] recalls from [\textit{F. W. Lawvere}, Dialectica 23, 281--296 (1969; Zbl 0341.18002); Repr. Theory Appl. Categ. 2006, No. 16, 1--16 (2006; Zbl 1114.18002); Proc. Sympos. Pure Math. 17, 1--14 (1970; Zbl 0234.18002)] some definitions concerning hyperdoctrines. From a logical viewpoint, a conjunctive doctrine represents a model of the conjunctive logic over arbitrary sorts, and the generalized existential doctrine is the free construction of a model for conjunctive logic with existential quantifications formulated for arbitrary terms. \item[\S 3] recalls from [\textit{D. Trotta}, Theory Appl. Categ. 35, 1576--1607 (2020; Zbl 1446.18007)] how to complete a conjunctive doctrine to a generalized existential doctrine with respect to a class of morphisms of \(\mathcal{C}\) closed under composition, pullbacks and containing the identities, providing the definition of a \(\Lambda\)-\textit{existential doctrine} (Definition 3.4). \item[\S 4] presents the main contribution of the paper as a characterization of the generalized existential completion in logical terms (Theorem 4.16). To achieve this goal, the notion of \(\Lambda\)\textit{-existential-free} objects of a \(\Lambda\)-existential doctrine \(P\) is introduced to denote objects which are \textit{free from the left-adjoints} \(\exists_{f}\) along \(\Lambda\). The notion provides an \textit{algebraic counterpart} of the logical concept of \textit{existential-free formula}. The characterization is reminiscent of Carboni's characterization of the construction of the exact completion of a lex category [\textit{A. Carboni}, Rapp., Sémin. Math., Louvain, Nouv. Sér. 221--236, 55--98 (1993; Zbl 0838.18003); J. Pure Appl. Algebra 103, No. 2, 117--148 (1995; Zbl 0839.18002)] \item[\S 5] first recalls from [\textit{D. Trotta}, Theory Appl. Categ. 35, 1576--1607 (2020; Zbl 1446.18007)] that the assignment \[ P\mapsto\mathsf{pEx}(P) \] of a primary doctrine to its pure existential completion extends to a lax-idempotent \(2\)-monads \[ \mathrm{T}^{\mathrm{ex}}:\boldsymbol{PD}\rightarrow\boldsymbol{PD} \] on the \(2\)-category of primary doctrines, and that the \(2\)-category \(\mathrm{T}^{\mathrm{ex}}\)-\(\boldsymbol{Alg}\) of algebras is isomorphic to the \(2\)-category \(\boldsymbol{ExD}\) of pure existential doctrines. The authors focus on the \textit{idempotent} \(\mathrm{T}^{\mathrm{ex}}\)-\textit{algebras}, namely those pure existential doctrines with \(P\cong\mathsf{pEx}(P)\). It is shown that they coincide with the pure existential doctrines rigged out in Hilbert's epsilon operators, emphasizing the relationship between choice principles and the algebraic characterization of pure existential completions. \item[\S 6] shows that elementary pure existential completions must inherit their elementary structure from their generating conjunctive doctrine, while it was demonstrated in [\textit{D. Trotta}, Theory Appl. Categ. 35, 1576--1607 (2020; Zbl 1446.18007)] that the pure existential completion preserves the elementary structure. It is also shown that any generalized existential completion relative to a class \(\Lambda\) containing product projections which inherit its elementary structure from its generating conjunctive doctrine must be a pure existential completion. \item[\S 7] provides relevant examples of generalized existential completions, multifurcating into \begin{itemize} \item[1.] every subobjects doctrine of a lex category; \item[2.] every \(\mathcal{M}\)-subobjects doctrine relative to a \(\mathcal{M} \)-category [\textit{J. R. B. Cockett} and \textit{S. Lack}, Theor. Comput. Sci. 270, No. 1--2, 223--259 (2002; Zbl 0988.18003); \textit{G. Rosolini}, in: Atti degli incontri di logica matematica, Vol. 2, Siena/Italia 1983/84, 627--630 (1985; Zbl 0592.03033); \textit{G. Rosolini}, Riv. Mat. Univ. Parma, IV. Ser. 11, 387--397 (1985; Zbl 0606.03011)] (Theorem 7.11); \item[3.] every weak subobjects doctrine of a lex category (Theorem 7.3); \item[4.] every realizability tripos [\textit{J. M. E. Hyland} et al., Math. Proc. Camb. Philos. Soc. 88, 205--232 (1980; Zbl 0451.03027)] (Theorem 7.24); \item[5.] among localic triposes, exactly those associated with a supercoherent locale in the sense of [\textit{B. Banaschewski} and \textit{S. B. Niefield}, J. Pure Appl. Algebra 70, No. 1--2, 45--51 (1991; Zbl 0744.06006)] (Theorem 7.32). \end{itemize} \item[\S 8] is concerned with future work, suggesting that the authors intend to broaden the study of regular and exact competions of generalized existential completions initiated in [\textit{M. E. Maietti} and \textit{D. Trotta}, ``Generalized existential completions and their regular and exact completions'', Preprint, \url{arXiv:2111.03850}] by including dialectica triposes [\url{https://cs.au.dk/~birke/phd-students/BieringB-thesis.pdf}] and modified realizability triposes [\textit{P. J. W. Hofstra}, Math. Proc. Camb. Philos. Soc. 141, No. 2, 239--264 (2006; Zbl 1115.03093); \textit{J. van Oosten}, J. Pure Appl. Algebra 116, No. 1--3, 273--289 (1997; Zbl 0882.03059)]. \end{itemize}