分离公理模式
集合论的ZF公理系统中的公理模式
分离公理模式,属于集合论的ZF公理系统中的公理模式。
定义
分离公理模式是集合论的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)应用替换公理模式,即得所求的集合。所求集合为空集时,这个集合的存在性需要空集定理保证。综上,由替换公理模式和空集公理可以证明分离公理模式。
注意上面的证明最后一句话中使用了排中律,保证非空集合必有元素。在直觉主义的逻辑中,排中律并不成立,所以分离公理模式是必要的。
参考资料
最新修订时间:2024-05-21 11:46
目录
概述
定义
证明
参考资料