分离公理模式

分离公理模式是集合论的ZF公理系统中的一个公理模式，但由于可以由替换公理模式和空集公理（注意后者是单独一条公理，在公理系统中优于一个公理模式）证明，目前有时已经不将之作为公理看待。它的表述为：“对任意集合x和任意对x的元素有定义的逻辑谓词P(z)，存在集合y，使z∈y当且仅当z∈x而且P(z)为真”。

由分离公理模式可以简单地由任何集合的存在性证明空集公理，只要使P(z)为矛盾式。无限公理保证了一个集合的存在性，所以在有分离公理模式的ZF公理系统中，空集公理是多余的。[1]

由替换公理模式可以“几乎”证明分离公理模式，即证明当所求的集合中存在元素时，分离公理模式成立。由前提不妨设存在这样的元素是w，则令f(z)=z当P(z)为真，f(z)=w当P(z)为假。对x和f(z)应用替换公理模式，即得所求的集合。所求集合为空集时，这个集合的存在性需要空集定理保证。综上，由替换公理模式和空集公理可以证明分离公理模式。

注意上面的证明最后一句话中使用了排中律，保证非空集合必有元素。在直觉主义的逻辑中，排中律并不成立，所以分离公理模式是必要的。[2]