Talk:Axiom of Pairing from Powers and Replacement

I don't want to refactor to include another proof, but Power Set of Empty Set and Power Set of Singleton can show that $\{ \O , \{ \O \} \}$ is a set much more quickly. --TheoLaLeo (talk) 08:28, 24 November 2021 (UTC)

Yes, this is true, but the object of this page is to demonstrate that the Axiom of Pairing can be directly derived from those specific first principles "Axiom of Powers" and "Axiom of Replacement", thereby showing that technically the Axiom of Pairing is redundant. This is a point which is frequently mentioned on analyses of ZF(C) but rarely demonstrated directly.

While we could just replace the entire page by invocations of those results, a) it obscures the details of this important result, and b) extra care is needed to ensure that the specific proofs of these results are based firmly on ZF(C) and not naive set theory -- and in the case of Power Set of Singleton I am not sure that we have such a result. And how sure are we (without checking carefully) that Power Set of Singleton does not itself depend upon the Axiom of Pairing itself? Such is the danger of circularity that it is better to work through the entire proof explicitly, using only results that are definitely demonstrated to depend only upon those axioms mentioned.

Whether this proof is successful at achieving that end may be up for analysis. --prime mover (talk) 09:02, 24 November 2021 (UTC)