Can you summarize the following document?
        
  假定 "P" 是一個雙變數謂詞,對於任何集合 "x" 有一個唯一的集合 "y" 使 "P"("x","y") 成立。接著我們可以形成一個單變數的泛函謂詞 "F",使得 "F"("x") = "y" 當且僅當 "P"("x","y")。  替代公理聲稱,給定一個集合 "A",我們可以找到一個集合 "B",它的成員完全是 "F" 在 "A" 的成員上的值。注意對於每個這樣的謂詞 "P" 都有一個相對應的公理;所以,這是一個公理模式。  在 Zermelo-Fraenkel 公理的形式語言中,這個公理模式讀做: 換句話說,  如果允許在公理模式中使用匯出的泛函謂詞,則這個公理模式可以寫為: 對於每個匯出的單變數的泛函謂詞 "F"; 換句話說:  通過外延公理可知這個集合 "B" 是唯一的。我們稱這個集合 "B" 為 "A" 在 "F" 下的像,並指示它為 "F"("A") 或(使用集合建構式符號形式){"F"("x"):"x"∈"A"}。  有時引用這個公理不帶唯一性要求: 就是說,謂詞 "P" 不被限制為泛函的:要應用它於一個集合 "A",只需存在至少一個元素 "y" 對應於 "A" 的每個元素 "x" 就可以了;"y" 對每個 "x" 是唯一的不是必需的。在這種情況下,被斷言存在的像集合 "B" 將為 "A" 的每個 "x" 包含至少一個這樣的 "y",不保證只包含唯一的一個。  有時陳述這個公理不對謂詞加任何限制: 就是說,根本不要求 "P" 把集合 "A" 的一個元素對映到任何物件。但是如果對於 "A" 的一個元素 "x" 有至少一個 "y" 對應於它,則像集合 "B" 將包含至少一個這樣的 "y"。  這個不對謂詞作限制的公理,也叫做有界公理或蒐集公理,看似比原先的替代公理更強,但是這兩個版本都可以從替代公理推匯出來。另一方面,任何泛函謂詞都是謂詞,所以有界公理也蘊涵替代公理,因此兩個公理是等價的(在給定了其他 Zermelo-Fraenkel 公理的情況下)。

  序數 ω·2 = ω + ω(使用馮·諾伊曼的現代定義)是第一個不使用替代公理就不能構造的序數。無窮公理斷言無限序列 ω = {0, 1,2...} 的存在,也只斷言了這個序列。我們希望定義 ω·2 為序列 {ω, ω + 1, ω + 2...},但是一般的序數的類不一定是集合(例如,所有序數的類不是集合)。替代公理允許你把在 ω 中每個有限數 "n" 替代為對應的 ω + "n",並保證替代所得的類是集合。注意你可以輕易地構造序同構於 ω·2 的良序集合而不需用到替代公理:取 ω 的兩個復件的不交併,然後設第二個復件大於第一個便可。但這樣所得的集合並不是一個序數,因為它在屬於關係下不是一個全序。  顯然,若要確保可以指派一個序數給任意的良序集合,也要用到替代公理。類似的,若要確保可以指派一個基數給任意集合(馮·諾伊曼基數指派),我們也需要替代公理,以及選擇公理。  所有的可數的極限序數的構造也要求替代公理,就像 ω·2 的構造那樣。較大的序數則不那麼直接地依賴於替代公理。例如 ω 是第一個不可數序數,可以構造如下:由全體可數良序組成的集合,會是 ℘(N×N) 的一個子集,這點通過分離公理和冪集公理可知(在 "A" 上的關係是 "A"×"A" 的一個子集,因此是冪集 ℘("A"×"A") 的一個元素。關係的集合因此是 ℘("A"×"A") 的子集)。把每個良序集合替代為它的序數。這是可數序數 ω 的集合,它自身可以被證明是不可數的。這個構造使用了替代公理兩次;第一次確保對每個良序集合的一個序數指派,第二次把良序集合替代為其對應的序數。這是 Hartogs 數的結果的特殊情況,而一般情況可以類似的證明。  不帶替代公理的選擇公理(ZC 集合論)不足以強到證明 博雷爾集是確定公理的;為此你需要替代公理。

  多數可以應用替代公理的應用實際上不需要它。例如,假設 "f" 是從集合 "S" 到集合 "T" 的函式。接著我們可以構造一個泛函謂詞 "F" 使得在 "x" 是 "S" 的成員的時候有 "F"("x") = "f"("x"),在其他時候隨意設 "F"("x") 為某個物件(這裡的指派方式不要緊)。然後,給定 "S" 的一個子集 "A",應用替代公理模式於 "F",構造子集 "A" 在函式 "f" 下的像 "f"("A") 為 formula_5(或表示為 "<nowiki>F</nowiki>"("A"))。但是這裡實際上不需要替代公理,因為 "f"("A") 是 "T" 的子集,所以我們可以使用分類公理模式來構造這個像為集合 formula_6。一般的說,當 "F" 在 "A" 的成員上的值都屬於某個預先構造的集合 "T" 時,使用分類公理就足夠了;只在不能獲得這樣的 "T" 的時候,才需要替代公理,比如定義在真類的子集上的運算。  按某些哲學家的說法,在上述例子中最好應用分類公理於集合 "T",因為分類公理在邏輯上弱於替代公理。實際上,在普通數學中不需要替代公理,只是需要它作為特定公理化集合論的特徵。例如,你需要替代公理來從 ω·2 向上構造馮·諾伊曼序數,而馮·諾伊曼序數對特定集合論的結果是必需的。在良序集合的理論就足夠應用的情況下,你不需要用替代公理構造這些序數。對於某些鑽研數學基礎的數學家,特別是那些專注於型別論而非集合論的人,他們或認為這個公理在各種意義上都是不需要的,因此在其工作中不包括這個公理(以及其相對應的型別論版本)。通常在基於 拓撲斯 理論建造的基礎理論上,都難以表達出替代公理,所以一般不包括它。然而,替代公理的爭論不在於有人認為它的推論必然是假的(如選擇公理的爭論);只是有部分人認為它是沒有必要的。  替代公理模式不是 恩斯特·策梅洛 在 1908年所公理化的集合論(Z)的一部分;它由 亞伯拉罕·弗蘭克爾 在 1922 年引入,從而得到了現代的 Zermelo-Fraenkel 集合論 (ZF)。陶拉爾夫·斯科倫 在同一年晚些時候獨立的發現了這個公理,實際上我們今天使用的公理列表是Skolem的最終版本 -- 通常不提及他的貢獻是因為每個單獨的公理都是 Zermelo 或 Fraenkel 早先發現的。從證明論的觀點看,增加替代公理形成了很大的差異;把這個公理模式加進Zermelo 公理使系統在邏輯上更強,允許你證明更多的陳述。特別是,在ZF 中你可以通過構造馮·諾伊曼全集 V 為模型,證明 Z 的相容性。(當然,哥德爾第二不完備定理表明這兩個理論都不能證明自身的相容性,如果它自身是相容的。)
在公理化集合論和使用它的邏輯、數學和電腦科學分支中,替代公理模式是 Zermelo-Fraenkel 集合論的一個公理模式,它本質上斷言一個集合在一個對映(泛函謂詞)下的像也是一個集合。它對於構造特定的大集合是必需的。