首页/论文/0710.3077

arXiv 0710.30772007-10-16math.LOmath.CT

谓词代数集理论的若干问题I：精确完备化

Aspects of Predicative Algebraic Set Theory I: Exact Completion

Benno van den Berg, Ieke Moerdijk

备注：: Submitted to Ann. Pure Appl. Logic

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

这是第一次在一系列的三篇论文的代数集理论。其主要目的是为后面的两个部分，即代数集理论中的可实现性和层模型奠定必要的基础。

英文摘要：

This is the first in a series of three papers on Algebraic Set Theory. Its main purpose is to lay the necessary groundwork for the next two parts, one on Realisability and the other on Sheaf Models in Algebraic Set Theory.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

谓词代数集论II的几个方面：可实现性

Aspects of Predicative Algebraic Set Theory II: Realizability

这是第二次在一系列文件之间的关系代数集合论和谓词形式系统。在第一部分中，我们引入了小映射的谓词范畴的概念，并得到了这样的范畴总是包含一个集合论模型的结果。在本文中，我们表明，熟悉的可实现性模型的建设性集合论CZF和IZF可以得到作为一个应用程序的这一结果。为了这个目的，我们表明，谓词范畴与小地图是封闭的内部概念的可实现性。

2008-01-15math.CTmath.LO

谓词代数集论III的几个方面：层

Aspects of Predicative Algebraic Set Theory III: Sheaves

这是第三批在一系列文件的代数集合论。在它，我们开发了一个统一的方法，层模型的建设性集合论的基础上的想法，从范畴逻辑。关键的概念是“带有小映射的谓词范畴”，它公理化了类和类态射的范畴的概念，以及纤维是集合的选定的映射类（在某些公理化集合论中）。本文的主要结果是，这类具有小映射的谓词范畴在内层下是稳定的。我们讨论了层模型的建设性集合论，这导致，以及未来的工作思路。

2011-11-16math.CTmath.LO

Hyland的Effective Topos的一个谓词变体

A predicative variant of Hyland's Effective Topos

在这里，我们提出了一个子类pEff的Hyland的有效地形Eff，可以被认为是一个谓词的变体Eff本身。pEff的构造是出于提供一个“谓词性”的实现者范畴论域的愿望，以模拟第一作者与G. Sambin于2005年完成，并于2009年由第一作者完成为两级正式系统。pEff是一个“谓词的”范畴论域，因为它的对象和态射可以在Feferman的归纳定义的谓词弱理论ID1^中形式化。此外，由于以下原因，它是有效拓扑的谓词变体。首先，pEff是dID 1中可定义对象的列表算术局部carbohydrate封闭的pretopos，具有pEff上的小对象的分类器和小子对象的（非小）分类器。第二，它恰好与在ID1^中定义为递归定义的Eff子范畴的谓词化的lex范畴上的精确完成相一致。因此，它验证了形式教会的论文，它嵌入在EFF通过保持列表算术局部carbohydrate封闭的pretopos结构。

2018-06-22math.LO

构造和谓词单价基础中的域理论

Domain Theory in Constructive and Predicative Univalent Foundations

我们在没有Voevodsky公理的构造性单叶基础上发展域理论。在以前的工作中，在这个方向上，我们构建了PCF的斯科特模型，并证明了其计算充分性，基于有向完备偏序集（dcpos）。在这里，我们进一步考虑代数和连续dcpos，并建立斯科特的$D_\infty$模型的无类型的$λ$ -演算。在谓词基础中处理大小问题的一种常见方法是使用信息系统或抽象基或形式拓扑而不是dcpos，以及近似关系而不是Scott连续函数。在这里，我们接受dcpos可能很大，并与类型宇宙一起工作来解释这一点。例如，在PCF的Scott模型中，dcpo在第二论域$\mathcal{U}_1$中具有载体，在第一论域$\mathcal{U}_0$中具有索引类型的有向族的上确界。把偏序集看作是一个范畴，我们可以说这些dcpos是大的，但局部很小，并且有小的滤子余极限。在代数dcpos的情况下，为了处理大小问题，我们继续模仿可及范畴的定义。有了这样的定义，我们的斯科特的$D_\infty$的建设再次给出了一个大的，局部小，代数dcpo小有向上确界。

2022-06-15cs.LOmath.LO

构造性测度论中的集合族

Families of Sets in Constructive Measure Theory

我们提出的第一个步骤的建设性主教-程测度论的预测重建。工作在一个半正式的阐述主教的集合论和调用的概念集索引家庭的子集（一个给定的集合），我们到达的概念，一个前集成空间和一个前测度空间。然后构造了与预测度空间相关联的简单函数的预积分空间和预积分空间的$L^1$ -完备化。与Bishop-Cheng测度论的标准表述不同，我们的发展完全是预测性的，避免了可数选择公理。

2022-07-08math.LO

代数集理论的统一方法

A Unified Approach to Algebraic Set Theory

本文介绍了代数集理论（AST）。AST是一个灵活的范畴框架，用于研究不同类型的集合论：经典的和构造的，谓词的和非谓词的。我们讨论了在这方面的基本成果，特别强调应用建设性的集合论IZF和CZF。(This这篇论文是第二位署名作者在2006年奈梅亨逻辑学术讨论会上所作的关于范畴逻辑的教程的摘要。）

2007-10-16math.CTmath.LO

更多相关论文收起更多论文

直谓Bishop-Cheng测度论中的前测度空间与前积分空间

Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory

针对Bishop-Cheng测度论的非直谓性问题，研究者在Bishop集合论框架下提出前测度空间与前积分空间的直谓概念，完成相关构造与验证，实现直谓框架下的测度积分理论构建。

2024-10-03math.FAmath.LO

初等理论完备化的代数方法

An algebraic approach to the completions of elementary doctrines

我们提供了一个彻底的代数分析三个已知的完成有一个核心作用，在确切的完成Lawvere的理论：一个全面的对角线（即强制平等的条款，以符合平等谓词），一个增加充分的理解和一个添加concierents。我们证明了所有这些2-对偶都是2-单子的，并且由这些对偶产生的2-单子都是类属性的。这意味着全面的对角线，充分的理解和双元数是一个基本理论的代数性质。最后，我们讨论并给出了这些2-单子之间的分配律。

2021-08-07math.CTmath.LO

路范畴的精确完备化与代数集合论--第一部分：路范畴的精确完备化

Exact completion of path categories and algebraic set theory -- Part I: Exact completion of path categories

我们引入的概念，“类与路径对象”，作为一个轻微的加强肯尼斯布朗的经典概念的“类的不确定性对象”。我们发展了这样一个范畴及其相关同伦范畴的基本性质。随后，我们展示了如何准确完成这个同伦范畴可以获得作为同伦范畴关联到一个更大的类别与路径对象，获得自由邻接某些同伦同伦。在本文的第二部分，我们将提出一个应用模型的建设性集合论。虽然我们的工作部分是由同伦类型理论的最新发展的动机，这篇论文是纯粹的同伦理论和范畴论的语言写的，我们不预设任何熟悉的类型理论的一方的读者。

2017-06-20math.CTmath.LO

p-adic半代数集的标度格和co-Heyting代数的模型完备化

Model completion of scaled lattices and co-Heyting algebras of p-adic semi-algebraic sets

设p是素数，K是p-代数闭域，X $\subseteq$ K^m是定义在K上的半代数集，L（X）是X的闭于X的半代数子集的格.我们证明了L（X）的完备理论消除了某种语言LASC中的量词，L（X）上的LASC-结构是格结构定义的推广。而且它是可判定的，这与在实封闭的场上发生的情况相反。我们将这些LASC结构分类为初等等价，特别是得到L（K^m）的完整理论只依赖于m，不依赖于K，甚至不依赖于p。作为应用，我们得到了可数p-代数闭域上的半代数集的分类，直到所谓的“前代数”同胚。

2018-10-29math.LO

比例格的模型完备化

Model-completion of scaled lattices

从Grzegorczyk的论文\cite{grze-1951}可知，${\mathbb R}^n$的实半代数闭子集的格对每个整数$n\geq 2$都是不可判定的。更一般地说，如果$X$是实域或代数闭域$K$上的任何可定义集，则$X$闭于$X$中的所有可定义子集的格$L(X)$无论何时$\dim X\geq 2$都是不可判定的。然而，我们在本文中研究类${\rm SC\_{def}}(K,d)$的模型理论的所有这样的格$L(X)$与$\dim X\leq d$和$K$如上或一个亨塞尔值域的特征零。<p>我们表明，通用理论的${\rm SC\_{def}}(K,d)$，在一个自然的扩展定义的格语言，是相同的，每个这样的领域$K$。我们给出了它的一个有限公理化，证明了它是局部有限的，并允许一个模型完备化，它变成可判定的以及它的所有完备化。我们期望$L({\mathbb Q}\_p^d)$成为这个模型完成的一个模型（一个小变体）。这导致我们在$p$ -进半代数几何的一个新的猜想，结合本文的结果，将给予可判定性（通过一个自然的递归公理化）和消除量词的完整理论的$L({\mathbb R}\_p^d)$，一致$p$。

2006-06-30math.LO

$Π_2$的可容许性-推理规则：插值、模型完备和接触代数

Admissibility of $Π_2$-Inference Rules: interpolation, model completion, and contact algebras

我们设计了三种策略来识别非标准推理规则的容许性，通过插值，均匀插值和模型完成。我们将我们的机器应用于对称蕴涵演算$\mathsf{S^2IC}$的情况，其中我们还通过接触代数的等价理论提供了其代数对应物的模型完备化的有限公理化。利用这一结果，我们得到了一个有限基的容许$Π_2$ -规则。

2022-01-16math.LO

非阿基米德域上algebraic varieties的上同调

Cohomology of algebraic varieties over non-archimedean fields

基于Hrushovski-Loeser的稳定完备化，建立了代数闭非平凡值非阿基米德域$K$上代数簇的层上同调理论.在平行，我们开发了一个层上同调的热带半群$Γ_\infty$，其中$Γ$表示$K$的值群的O-最小扩展的可定义子集。对于拟射影簇，这两个上同调强烈相关的变形形变收缩的稳定完成同胚的一个可定义的子集$Γ_\infty$。在这两种情况下，我们表明，相应的上同调理论满足Eilenberg-Steenrod公理，有限性和不变性，我们提供自然界的上同调维数在每种情况下。作为应用，我们证明了可定义族中上同调群有许多同构类型。此外，由于代数簇的稳定完备化与其在V. Berkovich意义下的解析化之间的强关系，我们恢复并推广了代数簇的解析化的拓扑上同调的有限性和不变性结果.

2021-04-14math.AGmath.ATmath.LO

赋值域上曲线的纳什结构与驯服亨塞尔有理性

Nash structure of curves over a valued field and tame henselian rationality

Sorbonne Université, Université Paris-Diderot, CNRS, Institut de Mathématiques de Jussieu-Paris Rive Gauche, IMJ-PRG（索邦大学，巴黎第七大学，法国国家科学研究中心，儒勒·让苏-巴黎左岸数学研究所）；Sorbonne Université, Institut de Mathématiques de Jussieu-Paris Rive Gauche, CNRS（索邦大学，儒勒·让苏-巴黎左岸数学研究所，法国国家科学研究中心）

该研究针对Kuhlmann的驯服亨塞尔有理性定理，借助赋值域上代数簇稳定完备化的框架，通过证明代数曲线稳定完备化的纳什结构定理与抽象多圆盘的驯服下降定理，给出了兼具模型论与几何性质的新证明。

2026-09-16math.ACmath.AGmath.LO