Axiom talk:Axiom of Unions

From ProofWiki
Jump to navigation Jump to search

At the risk of interfering mid-way, I wonder why we now have two pages for Axiom of Unions, for set theory and class theory, which do in fact state exactly the same thing (if you unpack the definition of union of set of sets). Am I missing something? — Lord_Farin (talk) 06:31, 9 May 2022 (UTC)

Subtle but important difference.
Axiom:Axiom of Unions/Set Theory allows you to create a union out of a set of sets.
Axiom:Axiom of Unions/Class Theory starts from having previously defined a union of a given class. Having done that, it then declares that if the class you built the union from was a set, then the union is also a set.
--prime mover (talk) 16:00, 9 May 2022 (UTC)
Got it, makes sense. Might be worthwhile to explicate this on the page, though, to avoid future confusion. — Lord_Farin (talk) 16:06, 9 May 2022 (UTC)
Yes, I have it in mind to do that, as soon as I find a way to do it coherently and explicatabiliously. --prime mover (talk) 17:02, 9 May 2022 (UTC)

After further analysis (in other words, I found something in the book that I misunderstood and didn't follow up on first and second time round): there's a note that says: "We could replace $A_5$ (which is the Axiom:Axiom of Unions/Class Theory) by the apparently weaker statement ${A'}_5$: for any set $x$ there is a set $y$ that contains all elements of all elements of $x$ (which is Axiom:Axiom of Unions/Set Theory)." So the formulations (at least in the context of class theory) are equivalent anyway.

Exercise $5.1$ of this chapter is the proof of the above: "Why is Note $1$ true?" (which I had originally mistakenly thought applied to Note $1$ in Section $3$, which is uniqueness of the empty class), and it remains for me (or someone) to prove this.

Be that as it may, it is still appropriate to keep these formulations separate, because the only the first one can be applied in the context of pure set theory, while both can be applied in class theory. Because S&F keep them separate, and I suspect other treatments may also use Formulation 2, it's still probably worth keeping this structure so as to provide an appropriate context for a student who has perhaps only come across the one. --prime mover (talk) 19:38, 9 May 2022 (UTC)

... Right, I've made an attempt at this: Axiom:Axiom of Unions/Set Theoretical and Class Theoretical. It occurs to me that I am going to have to invent something more generic, as the same argument is going to be needed in a number of different contexts. I can see Axiom:Axiom of Powers looming out of the mist. --prime mover (talk) 20:33, 9 May 2022 (UTC)
Beautiful, nice job! — Lord_Farin (talk) 05:27, 10 May 2022 (UTC)