冯诺伊曼-博内斯-哥德尔集合论
维库,知识与思想的自由文库
|
在数学基础中,冯纽曼-博内斯-哥德尔集合论(von Neumann–Bernays–Gödel Set Theory,NBG)是设计生成同Zermelo-Fraenkel 集合论与选择公理一起(ZFC)同样结果的集合论公理系统,但只有有限数目的公理而不使用公理模式。 首先由冯·诺伊曼在1920年代公式化,在1937年开始由 保罗·博内斯 修改,在1940年由哥德尔进一步简化。 不象 ZFC,NBG 只有有限多个公理。Richard Montague 在1961年证明,不可能找到在逻辑上等价于 ZFC 的有限数目的公理;因此 NBG 的语言有能力谈论真类同谈论集合一样,并且关于集合的陈述在 NBG 中是可证明的,当且仅当它在 ZFC 中是可证明的(就是说 NBG 是 ZFC 的保守扩展)。
[编辑] 理论这个理论的标志特征是类和集合的分离。类可以非常大 — 实际上你可以谈论“所有集合的类”。但是有一个结构性限制防止你推测“所有类的类”或“所有集合的集合”。 成员关系 只定义在 a 是集合而 s 是集合或类的条件下。 类的开发镜像了朴素集合论的开发。给出了抽象的原则,因此可以用类形成带有成员关系的谓词演算的任何陈述。等式、配对、子类的概念都是定义而不是公理的事情 — 定义们指示了一个公式的特定抽象。 集合的开发进行得非常类似于 ZF。有一个谓词“Rp”定义如下: 就是说,一个集合 a 表示(represent)一个类 A,如果 a 的所有元素都是 A 的元素,反之亦然。有些类没有表示,比如不包含自身的所有集合的类。这样的类叫做真类。 这种系统的优点是提供了谈论“大对象”的脚手架而不涉险悖论。在范畴论的某些开发中,比如,你把一个大范畴指示为其对象的搜集和态射的搜集可以被表示为真类的范畴。在另一方面,小范畴是其中的对象和态射“适合”于集合的范畴。,因此,我们可以容易的谈论“所有小范畴的范畴”而没有麻烦。当然这是个大范畴。 [编辑] NBG 的公理化在本节中提供一个 NBG 的公理化(实际上有两个不同的公理化,第二个精致了第一个)。比较于 Morse-Kelley 集合论的公理化。 我把 NBG 看作两种类(two-sorted)的理论,小写字母充当集合变量而大写字母充当类变量。成员关系的陈述需要有如下形式之一: 这个理论也可以被表达为单种类(one-sorted)的理论,通过如下定义来区分集合和类: 一个类是集合,如果它是另一个类的元素。 公理如下,不带类字样的公理是关于集合的。
如果强化这个公理模式允许所有公式(包括在类上量化的公式),则它不再是有限的公理化的,而获得的理论叫做 Morse-Kelley 集合论。
注意这个公理允许有序对的定义,并与类概括一起允许把在集合上的关系实现为类(和特定的类关系同一化为从一个类到另一个类的函数、单射和双射)。
这个公理贡献自冯·诺伊曼,并一下实现了分离公理、替代公理和全局选择公理。如果需要的话,它可以被弱化为“任何其定义域被包含在一个集合中的类函数的值域等于一个集合”;这将去除选择公理(如果需要可以把它替代为更加有用的局部形式的选择公理)。完全的大小限制公理蕴涵了全局选择公理,因为序数的类不是集合,所以有从序数到全集的双射。
[编辑] 拆分类概括公理模式NBG 的一个吸引人但使它的形式公理化有些神秘的特征是类概括公理模式等价于它的实例的有限数目的合取。这里我们开发了这样的有限公理化,但是不保证它完全同于正式公理化。 我们通过考虑公式的结构来开发这种公理化。
这个公理给予我们起始的东西(结合上第一个公理化中的关于集合存在的那些公理),并且处理在公式中的集合参数(parameter)。 注意如果
现在我们需要处理量化。为了处理多个变量,我们需要能够表示关系。有序对 (a,b) 被定义为平常的 {{a},{a,b}}(我们假定了其他 NBG 公理所以有配对)。
通过这些公理,我们可以自由的增加虚(dummy)实际参数(argument)并在任意元数关系中重新安排的实际参数的次序。结合公理的特殊形式被完全设计用来使把在实际参数列表中任何项提到前面成为可能(加上逆转公理的辅助)。我们把实际参数的列表 现在我们观察到如果
现在我们需要专注于由原子公式表达的关系。
对角公理加上虚实际参数和实际参数的重新安排,可以被用来建造断言它的参数中任何两个的等式的关系;它可以被用来处理重复的变量。 本节的公理可以替代前面一节中类概括公理。 [编辑] 引用
|



或
,而等式的陈述需要有如下形式之一
写为 a=A。
: 有相同元素的类是相同的。
: 有相同元素的集合是相同的。
。
。
且
,则
且
。则足够处理所有命题连结词。
是类。
是类。
是类 (
实际上就是我们所需要的全部)。
和
存在。
和
存在。
表示为
(它是第一个实际参数作为它的第一个投影而实际参数列表的“尾部”作为它的第二个投影的有序对)。想法是应用 Assoc1 直到这个要提到前面的实际参数被提成第二个参数,接着应用适合的 Conv1 或 Conv2 把第二个参数提到前面,接着应用 Assoc2 直到最初应用 Assoc1 的效果(现在在被移动的实际参数后面的那些实际参数)被改正。
存在,则集合
简单的是把被考虑为关系的第一个集合的值域。全称量词依据存在量词和否定来定义。
存在。可以使用前面的公理重新安排实际参数来把任何单一实际参数提到参数列表的前面来被量化。
存在。
存在。
