分离公理模式是策梅洛-弗兰克尔集合论（ZF系统）的核心公理之一，用于从已知集合中构造满足特定性质的子集。该公理通过限制集合构造方式，直接排除了罗素悖论的产生，奠定了公理化集合论的基础。作为ZF系统的第二条公理，它与外延公理、配对公理等共同构建集合论的形式化框架。其数学表达要求对于任意集合X和逻辑谓词P(z)，存在由X中满足P(z)的元素组成的集合Y。

分离公理模式在形式化语言中可以表述为：对任意集合X和定义在X元素上的逻辑谓词P(z)，存在集合Y={z∈X | P(z)}。该表述包含两个核心限制：

这与朴素集合论。

1901年罗素悖论引发第三次数学危机后，策梅洛于1908年提出首个公理化集合论系统，其中第二条公理即为分离公理模式。弗兰克尔在1922年改进该系统时保留了该公理的核心思想，最终形成现代ZF公理系统。

在策梅洛的原始构想中，该公理被描述为'通过限定公理元素对应的性质同时为真来定义集合'，其对话式解释强调'只有当性质在某个已有集合的元素范围全体适用时，才能进行集合构造'。

标准的ZF系统将该公理模式形式化为：∀X∃Y∀z(z∈Y ↔ (z∈X ∧ φ(z)))其中φ(z)是包含自由变量z的一阶逻辑公式，且Y不在φ中出现。

1963年柯恩通过力迫法证明分离公理模式独立于ZF系统的其他公理，这一成果：为集合论模型研究提供了新工具

该公理模式的确立使得：