策梅洛-弗兰克尔集合论（Zermelo-Fraenkel Set Theory），含选择公理时常简写为 ZFC，是在数学基础中最常用形式的公理化集合论。不含选择公理的则简写为ZF。

集合论（Zer策梅洛-弗兰克尔melo-Fraenkel Set Theory），含选择公理时常简写为 ZFC，是在数学基础中最常用形式的公理化集合论。不含选择公理的则简写为ZF。

ZFC 构成自一个单一的基本本体论概念集合，和一个单一的本体论假定，就是在论域中所有的个体(就是所有数学对象)都是集合。有一个单一的基本二元关系集合成员关系；集合 a是集合 b的成员写为 ab(通常读做 "a 是 b 的元素")。ZFC 是一阶理论；所以 ZFC 包括后台逻辑是一阶逻辑的公理。这些公理支配了集合的行为和交互。ZFC 是标准形式的公理化集合论。使用 ZFC 的大量的正在进行中的普通数学推导请参见 Metamath在线计划。

在 1908 年，恩斯特·策梅洛提议了第一个公理化集合论，策梅洛集合论。这个公理化理论不允许构造序数；而多数“普通数学”不使用序数就被不能被开发，序数在多数集合论研究中是根本工具。此外，Zermelo 的一个公理涉及“明确性”性质的概念，它的操作性意义是有歧义的。在 1922 年，Abraham Fraenkel和 Thoralf Skolem独立的提议了定义“明确性”性质为可以在一阶逻辑中公式化的任何性质。从他们的工作促成了替代公理。Zermelo 集合论接受替代公理和正规公理产生了被称呼为 ZF的这个集合论。

向 ZF 增加选择公理产生了 ZFC。在数学成果要求选择公理的时候，有时明显的这么声明。这么单提出 AC 的原因是 AC 天生的是非构造性的；它确立一个集合(选择集合)的存在，而不规定如何构造这个集合。所以使用 AC 证明的结果涉及尽管可以证明其存在(如果你不忠于构造主义本体论的话)，但可能永远都不能构造出来的集合。

ZFC 有无穷多个公理，因为替代公理实际上是公理模式。已知 ZFC 和 ZF 集合论二者都不能用有限数目个公理来公式化；这最先由 Richard Montague证实。在另一方面，冯诺伊曼-博内斯-哥德尔集合论（Von Neumann–Bernays–Gödel, NBG）可以有限的公理化。NBG 的本体论同集合一样包括类；类是有成员但不是其他类的成员的实体。NBG 和 ZFC 是等价的集合论，在关于集合(就是说不以任何方式提及类)的任何定理在一个理论中可以证明就可以在另一个理论中证明的意义上。

依据哥德尔第二不完备定理，ZFC 的相容性不能在 ZFC 自身之内证明。ZFC 的广延等同于普通数学，所以 ZFC 的相容性不能在普通数学中证明。ZFC 的相容性可从弱不可及基数的存在而得出，它是其存在不能在 ZFC 中证明的某种东西。但是几乎没有人怀疑 ZFC 有什么未被发觉的矛盾；如果 ZFC 是不自洽的，早就该被发掘出来。这是确定无疑的: ZFC 免除了朴素集合论的三大悖论，罗素悖论、布拉利-福尔蒂悖论和康托尔悖论。

文献中讨论过的 ZFC 的缺陷包括:

它比几乎所有普通数学所要求的程度还要强(Saunders MacLane和 Solomon Feferman这么认为)； 相对于其他集合论的公理化，ZFC 相对要弱。例如，它不允许全集(如新基础)或类(如 NBG)的存在； Saunders MacLane(范畴论的缔造者之一)和其他人争论说任何公理化集合论对于实际上的数学工作方式而言都是不正当的。依据他的观点，数学不是关于抽象对象的搜集和它们的性质的学科，而是关于结构和结构保持的映射的学科。