A characterization of generalized existential completions

被引：3

作者：

Maietti, Maria Emilia ^{[1
]}

Trotta, Davide ^{[2
]}

机构：

[1] Univ Padua, Dept Math, Padua, Italy

[2] Univ Pisa, Dept Comp Sci, Pisa, Italy

来源：

ANNALS OF PURE AND APPLIED LOGIC | 2023年 / 174卷 / 04期

基金：

欧盟地平线“2020”;

关键词：

Existential doctrine; Existential free element; Tripos; Exact completion; Contents; REALIZABILITY; CATEGORIES;

D O I：

10.1016/j.apal.2022.103234

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

This paper aims to provide an intrinsic characterization of the notion of generalized existential completion of a conjunctive doctrine P for a class Lambda of morphisms of the base category of P. The cornerstone of this result consists of an algebraic description of the logical concept of existential free formulas closely connected to the validity of some choice principles. The link between our characterization 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 if and only if P is equipped with Hilbert's epsilon operators. Our characterization provides a useful tool to recognize a wide variety of examples of doctrines arising as generalized existential completions. These include the subobjects doctrine and the weak subobjects doctrine of a category with finite limits as well all realizability triposes and among localic triposes only the supercoherent ones.(c) 2022 Elsevier B.V. All rights reserved.

引用

页数：37