分离公理模式是集合论的ZF公理系统中的一个公理模式,但由于可以由
替换公理模式和
空集公理(注意后者是单独一条公理,在公理系统中优于一个公理模式)证明,有时已经不将之作为公理看待。它的表述为:“对任意
集合x和任意对x的元素有定义的逻辑
谓词P(z),存在集合y,使z∈y当且仅当z∈x而且P(z)为真”。
由分离公理模式可以简单地由任何集合的存在性证明空集公理,只要使P(z)为
矛盾式。无限公理保证了一个集合的存在性,所以在有分离公理模式的
ZF公理系统中,空集公理是多余的。
由替换公理模式可以“几乎”证明分离公理模式,即证明当所求的集合中存在元素时,分离公理模式成立。由前提不妨设存在这样的元素是w,则令f(z)=z当P(z)为真,f(z)=w当P(z)为假。对x和f(z)应用替换公理模式,即得所求的集合。所求集合为空集时,这个集合的存在性需要空集定理保证。综上,由替换公理模式和空集公理可以证明分离公理模式。
注意上面的证明最后一句话中使用了
排中律,保证非空集合必有元素。在
直觉主义的逻辑中,排中律并不成立,所以分离公理模式是必要的。