配對公理

在公理化集合論和使用它的邏輯、數學和計算機科學分支中，配對公理是 Zermelo-Fraenkel 集合論的公理之一。

在 Zermelo-Frankel 公理的形式語言中，這個公理讀做：

${\displaystyle \forall x,\forall y,\exists A,\forall z:z\in A\iff (z=x\lor z=y)}$

換句話說：

給定任何集合 x 和任何集合 y，有著一個集合 A 使得，給定任何集合 z，z 是 A 的成員，若且唯若 z 等於 x 或者 z 等於 y。

這個公理實際說的是，給定兩個集合 x 和 y，我們可以找到一個集合 A ，它的成員就是 x 和 y。我們可以使用外延公理證明這個集合 A 是唯一的。我們可以叫這個集合 A 為 x 和 y 的對，並把A指示為 {x,y}。所以這個公理的本質是：

任何兩個集合都有一個對。

{x,x} 簡寫為 {x}，叫做包含 x 的單元素集合。注意單元素集合是對的特殊情況。

配對公理還允許定義有序對。對於任何集合 ${\displaystyle a}$ 和 ${\displaystyle b}$，有序對的定義如下：

${\displaystyle (a,b)=\{\{a\},\{a,b\}\}.\,}$

注意這個定義滿足條件

${\displaystyle (a,b)=(c,d)\iff a=c\land b=d.}$

有序的n-元組可以遞歸的定義如下：

${\displaystyle (a_{1},\ldots ,a_{n})=((a_{1},\ldots ,a_{n-1}),a_{n}).}$

配對公理一般被認為是無可爭議的，它或它的等價命題出現在任何可替代的集合論的公理化中。不過在 Zermelo-Fraenkel 集合論的標準陳述裡，配對公理可以從冪集公理和替代公理模式中得出，所以它有時被省略。

與空集公理一起，配對公理可以一般化為如下模式：

${\displaystyle \forall x_{1},\ldots ,\forall x_{n},\exists A,\forall y:y\in A\iff (y=x_{1}\lor \cdots \lor y=x_{n})}$

就是說：

給定任何有限數目的集合 x₁ ,..., x_n，有一個集合 A，它的成員就是 x₁ ,..., x_n。同樣地，通過外延公理可知這個集合 A 是唯一的，其指示為{x₁,...,x_n}。

當然，我們不能嚴格地指出何謂有限數目的一些集合，除非早就給定了一個有限集合，而上述的x₁ ,..., x_n都屬於這個集合。所以，這不是一個單一的陳述而是一個模式（英語：Logical form），對每個自然數 n 有一個單獨的陳述。

• 情況 n = 1 是帶有 x = x₁ 而 y = x₁ 的配對公理。
• 情況 n = 2 是帶有 x = x₁ 而 y = x₂ 的配對公理。
• 情況 n > 2 可以透過多次使用配對公理和併集公理來證明。

例如，要證明情況 n = 3，使用配對公理三次，來生成對 {x₁,x₂}，單元素集合 {x₃}，接著的對 {{x₁,x₂},{x₃}}。併集公理接著生成想要的結果 {x₁,x₂,x₃}。我們可以擴展這個模式以包括 n=0，如果我們把這個情況詮釋為空集公理的話。

所以，它可以作為公理模式來替代空集公理和配對公理。但是人們通常單獨使用空集公理和配對公理，並把它作為一個定理模式來證明。注意接受這個模式為公理模式不會替代併集公理，在其他情況下仍需要併集公理。

另一個公理在給定空集公理時可以蘊涵配對公理：

${\displaystyle \forall x,\forall y,\exists A,\forall z(z\in A\iff (z\in x\lor z=y))}$

作代入（英語：Substitution (logic)）： x={}，y=a，我們得到 A 為 {a}。接著再作代入：x={a}，y=b，我們得到 A 為 {a,b}。透過這種方式可以構造任意有限集合。而且這個公理可以用來生成所有繼承有限集合，而不需使用併集公理。

• Paul Halmos, Naive set theory. Princeton, NJ: D. Van Nostrand Company, 1960. Reprinted by Springer-Verlag, New York, 1974. ISBN 0-387-90092-6 (Springer-Verlag edition).
• Jech, Thomas, 2003. Set Theory: The Third Millennium Edition, Revised and Expanded. Springer. ISBN 3-540-44085-2.
• Kunen, Kenneth, 1980. Set Theory: An Introduction to Independence Proofs. Elsevier. ISBN 0-444-86839-9.