新基础集合论

维基百科,自由的百科全书
跳转至: 导航搜索

数理逻辑中,新基础集合論NF)是公理化集合論的一種,由蒯因构想出來作为对《数学原理》中类型论的简化。蒯因1937年於《数理逻辑的新基础》一文中首次提及NF(此即其名稱的由來)。請注意,此条目大多是在談论NFU,這是Jensen於1969年所提出,並由Holmes於1998年闡述的一重要变体。

类型论TST[编辑]

改进版本的类型论TST的基本谓词是等於成员关系。TST有一个线性的类型层次:类型0由不加描述的个体组成。对于每个(元-)自然数n,类型n+1的对象是类型n对象的集合;类型n的集合有类型为n-1的成员。用等號连接的對象必须有相同的类型。下列两个原子公式简洁的描述了定类型规则:x^{n} = y^{n} \ x^{n} \in y^{n+1}(符号仍可改进)。

TST的公理是:

  • 外延性:带有相同成员的相同(正数)类型的集合是相等的;
  • 概括公理模式,也就是:
如果\phi(x^n)\ 公式,则集合\{x^n \mid \phi(x^n)\}^{n+1}存在。
换句话说,给定任何公式\phi(x^n) \ ,存在集合A^{n+1}\ 使得\forall x^n \exists A^{n+1} [x^n \in A^{n+1} \leftrightarrow \phi(x^n)]为真。

这个类型论比于《数学原理》首次发表的类型论簡單許多,因為它還得包括其参数不必然都有同样类型的关系类型。在1914年,諾伯特·維納展示了如何把有序对编码为集合的集合。这使得以这里描述的集合层次的方式消除了关系类型。

蒯因集合论[编辑]

公理和层化[编辑]

新基础(NF)是通过放弃TST的类型区别而获得的。NF的公理有:

  • 外延性:有相同元素的两个对象是同一个对象;
  • 概括模式:所有TST的概括实例,但去掉了类型索引(并且不用引入在变量之间新的同一性)。

通过约定,NF的概括模式使用层化公式的概念來陈述,而不直接提及类型。一个公式\phi被称为是层化的,如果存在从语法片段到自然数的一个函数f,使得对于任何\phi的原子子公式x \in yf(y) = f(x) + 1;而对于任何\phi的原子子公式x=y,有f(x) = f(y)。概括接着变成:

对于每个层化公式\phi存在\{x \mid \phi \}。甚至在层化概念内隐含的对类型的间接提及也可以消除。Hailperin在1944年证实了概括等价于它的一些推論的有限合取,所以NF可以有限的公理化而不提及类型的概念。

对于朴素集合论概括好像是不自洽的,但是在这里不是。例如,不可能的罗素类\{x \mid x \not\in x\}不是NF集合,因为 x \not\in x 不能被层化。

有序对[编辑]

关系函数在TST(以及NF和NFU)中以通常的方式定义为有序对。首先由Kuratowski在1921年提议的有序对常用的定义对于NF和相关理论有个严重缺陷:结果的有序对必定有比它的参数(它的左和右投影)的类型高2的类型。所以為了决定分层,函数有比它的的成员高3的类型。

如果能以其类型是同它的参数一样的类型的方式定义对(导致一个类型齐平有序对),则关系函数有只比它的域的成员的类型高1的类型。所以NF和相关理论通常采用蒯因有序对的集合论定义,這樣得出的是类型的类型-齐平的有序对。Holmes(1998)把有序对与它的左和右投影定為原始概念。幸运的是,無論有序对是通过定义或通过假定(就是作為原始概念)而类型齐平,通常是不重要的。

类型齐平有序对的存在蕴涵了“无穷公理”,而NFU +“无穷公理”解释了NFU +“存在着类型齐平的有序对”(它们不是同样的理论,但是区别无关紧要)。反过来,NFU +“无穷公理”+“选择公理”证明了类型齐平有序对的存在。

有用的大集合的可容纳性[编辑]

NF(以及NFU +“无穷公理”+“选择公理”,下面描述并已知是相容的)允许构造两种集合,它們都是ZFC和它的真扩展所不允许的,因为“太大”的緣故(某些集合论在真类的名义下接受这些实体):

NF(U)如何避免集合论悖论[编辑]

NF清除了三个周知的集合论悖论。NFU這個{相对}相容的理论也避免了这些悖论,增强了我们對這些理論的信心。

罗素悖论x \not\in x不是层化公式,所以不會通過概括的任何推論得出\{x \mid x \not\in x\}的存在性。蒯因构造NF的时候大概最关注于这个悖论。

关于最大基数康托尔悖论利用了康托尔定理全集的应用。康托尔定理声称(假定ZFC)任何集合的A \ 幂集P(A) \ 大于A \ (没有从P(A) \ A \ 单射函数)。但如果V \ 是全集的话,当然有从P(V) \ V \ 单射。為了解决这个问题,我们需要注意到|A| < |P(A)| \ 在类型论中没有意义:P(A) \ 的类型比A \ 的类型高1。正确的有类型版本(它是在类型论中的定理,成立的原因就像康托尔定理ZF中成立那樣)是|P_1(A)| < |P(A)| \ ,这里的P_1(A) \ A \ 的單元素子集的集合。在这个定理中,使我们感兴趣的特殊实例是|P_1(V)| < |P(V)| \ :單元素集合们少于集合们(因此一个元素的集合们少于全体对象,如果我们在NFU中的话)。从全集到这些單元素集合明显的双射x \mapsto \{x\} \ 不是一个集合;它不是集合是因为它的定义是非层化的。注意在所有已知的NFU的模型中|P_1(V)| < |P(V)| << |V| \ 都成立;“选择公理”允许我们不只证明有基本元素,而且在|P(V)| \ |V| \ 之间有很多基数。

我们现在引入某些有用的概念。若集合A \ 满足|A| = |P_1(A)| \ ,就被称为康托尔式的:康托尔式集合满足通常形式的康托尔定理。集合A \ 满足进一步条件(x \mapsto \{x\})\lceil A \ ,即单元素集合映射在A上的限制,则不只是康托尔式的而且是强康托尔式的。

下面是关于最大序数布拉利-福尔蒂悖论。我们定义(跟从朴素集合论)序数是良序排序相似性下的等价类。在序数上有一个明显的自然的良序排序;因为它是良序排序所以它属于一个序数\Omega \ 。(通过超限归纳法)可直接证明在小于一个给定序数\alpha \ 的序数们上的自然次序的序类型\alpha \ 自身。但是这意味着\Omega \ 是小于\Omega  \ 的序数们的序类型,因此它严格小于所有序数的序类型 -- 但是通过定义,后者是\Omega \ 自身!

在NF(U)中对这个悖论的解决开始于观察到在小于\alpha \ 的序数们上的自然次序的序类型的类型比\alpha \ 的类型高。因此类型齐平有序对的类型比它的参数的类型高1,而常规的Kuratowski有序对高3。对于任何序类型\alpha \ ,我们可以定义比\alpha \ 的类型高1的序类型:如果W \in \alpha \ ,则T(\alpha) \ 是次序W^{\iota} = \{(\{x\},\{y\}) \mid xWy\}的序类型。T运算的烦琐只是外观上的;可以轻易的证明T是在序数们上的严格的单调(序保持)运算。

我们可以用层化的方式重申关于序类型的引理:在小于\alpha \ 的序数们上的自然次序的序类型是T^2(\alpha) \ T^4(\alpha) \ ,依赖于使用哪个有序对定义(我们在下文中假定类型齐平有序对)。从此我们可演绎出在小于\Omega  \ 的序数们上的序类型是T^2(\Omega) \ ,从它我们演绎出T^2(\Omega)<\Omega \ 。因此T运算不是个函数;我们不能有从序数到序数的严格单调集合映射,它向下映射一个序数!因为T是单调的,我们有\Omega > T^2(\Omega) > T^4(\Omega)\ldots,在序数们中的“递减序列”不能是集合。

某些人已经断言这个结果证实了没有NF(U)的模型是“标准”的,因此在任何NFU的模型中序数们外在的不是不是良序的。我们不接受这种立场,而我们注意到还有一个NFU的定理,任何NFU的集合模型都有非良序的“序数”;NFU不结论出全集V是NFU的模型,尽管V是集合,因为成员关系不是集合关系。

关于数学在NFU中的进一步开发,和与在ZFC中相同的开发的比较,请参见数学的集合论实现en:Implementation of mathematics in set theory)。

蒯因在1940年第一版的《数理逻辑》的集合论中,结合了von Neumann-Bernays-Gödel集合论真类于NF,并为真类包括了一个无限制概括的公理模式。在1942年,J. Barkley Rosser证明了蒯因的集合论遭受Burali-Forti悖论。在1950年,Hao Wang展示了如何修正蒯因的公理来避免这个问题,蒯因在1951年第二和最终版本的《数理逻辑》中包括了结果的公理化。

参见[编辑]

引用[编辑]

  • Holmes, Randall, 1998. Elementary Set Theory with a Universal Set. Academia-Bruylant. The publisher has graciously consented to permit diffusion of this introduction to NFU via the web. Copyright is reserved.
  • Jensen, R. B., 1969, "On the Consistency of a Slight(?) Modification of Quine's NF," Synthese 19: 250-63. With discussion by Quine.
  • Quine, W. V., 1980, "New Foundations for Mathematical Logic" in From a Logical Point of View, 2nd ed., revised. Harvard Univ. Press: 80-101. The definitive version of where it all began, namely Quine's 1937 paper in the American Mathematical Monthly.

外部链接[编辑]