Inaccessible set axions may have little consistency strength
Inaccessible set axions may have little consistency strength
复制标题
不可接近的设定轴子可能具有很小的一致性强度
DOI：
10.1016/s0168-0072(01)00083-5
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
M. Rathjen
中科院分区：
文献类型：
--
作者：
Laura Crosilla;M. Rathjen
本文研究了构造集合论中不可达集公理及其相容性强度。在ZFC中，不可达集的形式是Vκ，其中κ是强不可达基数，Vκ表示冯诺依曼层次的第κ层。不可达集在范畴论中作为格罗滕迪克宇宙（Grothendieck universe）占有重要地位，并与类型论中的宇宙有关。本文的目的是表明不可达集公理的一致性强度在很大程度上取决于它们所嵌入的上下文。这里的上下文将是理论CZF−的建设Zermelo-Fraenkel集理论，但没有∈ -归纳（基础）。CZF− + INAC是一个数学上丰富的理论，在其中人们可以很容易地形式化Bishop风格的构造性数学和大量的范畴理论。CZF−+ INAC在类型论中也有一个可实现性解释，这使其定理具有直接的计算意义。这里给出的主要结果是CZF−+ INAC的证明论序数是一个小序数，称为费曼-舒特序数Γ0。
The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκwhere κ is a strongly inaccessible cardinal and Vκdenotes the κ th level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the context in which they are embedded. The context here will be the theory CZF−of constructive Zermelo–Fraenkel set theory but without ∈ -Induction (foundation). Let INAC be the statement that for every set there is an inaccessible set containing it. CZF−+ INAC is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. CZF−+ INAC also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of CZF−+ INAC is a small ordinal known as the Feferman–Schütte ordinal Γ0.