替換公理模式

替換公理模式是集合論的ZF公理系統中的一個公理模式。 替換公理模式的表述是：“對任意集合x和任意對x的元素有定義的邏輯公式F(z)，存在集合y，使w∈y若且唯若存在z∈x而且F(z)=w”。 替換公理模式的套用之一是用來構造序數ω·2。

替換公理模式是集合論的ZF公理系統中的一個公理模式。替換公理模式有時被其形式上更弱，在其他公理（包括分離公理模式）下等價的收集公理模式替代。替換公理模式的表述是：“對任意集合x和任意對x的元素有定義的邏輯公式F(z)，存在集合y，使w∈y若且唯若存在z∈x而且F(z)=w”。收集公理模式的表述是：“對任意集合x和定義在x和所有集合的類上的二元關係A(z,w)，如果對任何z∈x都存在w使A(z,w)為真，那么存在集合y，使得當存在z∈x，就存在w∈y，使A(z,w)為真”。
替換公理模式的套用之一是用來構造序數ω·2。從空集開始，不斷套用並集公理和無序對公理（用來構造{x}）可以證明所有自然數的存在，通過無窮公理和分離公理模式可以證明ω的存在，繼續取後繼可以證明ω+i（i∈N）的存在，但是因為不用替換公理模式無法證明這些序數組成一個集合，所以無法證明ω·2的存在。利用替換公理模式可以將N替換為{x|x=ω+i，i∈N}，與N取並集即可。同理，證明每個良序集都有對應的序數也要用到替換公理模式。