查看“外延公理”的源代码

在[[公理化集合论]]与使用它的[[逻辑]]、[[数学]]和[[计算机科学]]分支中，'''[[外延性]]公理'''或'''[[外延]]公理'''是 [[Zermelo-Fraenkel 集合论]]的[[公理]]之一。

==形式陈述==
在 Zermelo-Fraenkel 公理的[[形式语言]]中，它读做:

:<math>\forall A, \forall B: A=B \iff (\forall x: x \in A \iff x \in B)</math>

换句话说:
:[[全称量化|给定任何]][[集合]]<math>A</math>和任何集合<math>B</math>，<math>A</math>[[等于]]''<math>B</math>''，[[当且仅当]]给定任何集合<math>x</math>，<math>x</math>是<math>A</math>的一个成员当且仅当<math>x</math>是''<math>B</math>''的一个成员。

（这里的<math>x</math>是集合不是本质性的，但在'''ZF'''中所有东西都是集合。参见下面的带有基本元素的集合论章节）。

==解释==
要理解这个公理，注意上述符号陈述中圆括号内的子句简单的声称了 ''A'' 和 ''B'' 有完全相同的成员。所以，这个公理实际上说的是两个集合相等，当且仅当它们有完全相同的成员。它的本质是:
:集合唯一的由它的成员来决定。

外延性公理可以同 <math>\exist A, \forall x: x \in A \iff P(x)</math> 形式的[[分类公理#无限制概括|概括]]陈述一起使用，这里的<math>P</math>是不提及<math>A</math>或<math>x</math>的任何一元[[谓词]]，来定义一个唯一集合<math>A</math>，它的成员完全是满足谓词<math>P</math>的集合。我们可以接着为<math>A</math>介入新的符号；普通数学中的[[定义]]最终以这种方式工作的，当它们的陈述简化到纯集合论术语的时候。

外延性公理一般被认为是无可争议的，它或它的等价命題出现在所有[[可替代的集合論]]的公理化中。但是对于某些使用需要修改。

== 在没有等号的谓词逻辑中 ==

上面给出的公理假定等号是[[谓词逻辑]]的基本符号。某些公理化集合论的做法是不做这个假定：有的不把上述陈述作为公理，而是作为对等号的定义。那么，就必須連同来自谓词逻辑中有關等式的公理，作為关于这个被定义的符号的公理。多数等式的公理仍能从这个定义得出；余下的一个是
:<math>\forall A,\forall B: (\forall x : x\in A\iff x\in B)\Rightarrow(\forall C : A\in C\iff B\in C)</math>
而這就成为了所謂的外延性公理。

== 在有基本元素的集合论中 ==

[[基本元素]]是自身不是集合的一个集合的一个元素。在 Zermelo-Fraenkel 公理中没有基本元素，但在某些可替代的集合論的公理化中會有它们。基本元素可以被当作不同于集合的[[逻辑类型]]；在这种情况下，如果<math>A</math>是基本元素，则<math>x \in A</math>没有意义，所以外延性公理只适用于集合。

作为选择之一，在无类型逻辑中我们可以要求<math>x \in A</math>在<math>A</math>是基本元素的时候为假。在这种情况下，平常的外延性公理将蕴涵所有基本元素等于[[空集]]。为了避免这样，我们可以修改外延性公理为只适用于非空集合，并把它读为:
:<math>\forall A, \forall B, \exist x: x \in A \implies (A = B \iff (\forall y: y \in A \iff y \in B)). </math>
就是说:
:给定任何集合<math>A</math>和任何集合''<math>B</math>''，如果<math>A</math>是非空集合(就是说存在着<math>A</math>的一个成员<math>x</math>)，那么<math>A</math>和''<math>B</math>''是相等的，当且仅当它们有完全相同的成员。

另一个选择，在无类型逻辑中可定义<math>A</math>在<math>A</math>是基本元素的时候自身是<math>A</math>的唯一的元素。尽管这个方式可以胜任保存外延性公理，但基础公理反而需要调整。

== 引用 ==
*Paul Halmos, ''Naive set theory''. Princeton, NJ: D. Van Nostrand Company, 1960. Reprinted by Springer-Verlag, New York, 1974. ISBN 0-387-90092-6 (Springer-Verlag edition).
*Jech, Thomas, 2003. ''Set Theory: The Third Millennium Edition, Revised and Expanded''.  Springer.  ISBN 3-540-44085-2.
*Kunen, Kenneth, 1980. ''Set Theory: An Introduction to Independence Proofs''. Elsevier.  ISBN 0-444-86839-9.

[[Category:集合论公理]]
[[Category:罗素公理体系|W]]
[[Category:类的理论|W]]
{{集合论}}