Talk:Zermelo–Fraenkel set theory

Archives:

• Talk:Zermelo–Fraenkel set theory/Archive 1

Why no mention of the axiom of the empty set?

nt —Preceding unsigned comment added by 86.146.254.177 (talk) 07:10, 16 December 2007 (UTC)

Presumably Kunen chose to omit it because it can be deduced from the other axioms. From the axiom of infinity we get the existence of a set. From the axiom schema of specification we can reduce that set to the empty set. It is unique by the axiom of extensionality. JRSpriggs (talk) 08:08, 16 December 2007 (UTC)

The current article is incorrect in its treatment of the empty set. In the preamble to the axiom of infinity, The current article asserts the existence of the null set is derived from extensionality, regularity, specification, pairing, union, and replacement. This is false, because each of those axioms are (vacuously) true if no set exists. Hurkyl (talk) 09:19, 1 February 2008 (UTC)

I tried to fix this problem. How do you like the new version? Notice that the axiom of infinity itself supplies the existence of a set which is needed to show that the empty set exists. JRSpriggs (talk) 06:47, 3 February 2008 (UTC)

I don't see anything false, so I'm mostly content. However, I notice another problem. The presentation invokes the axiom of infinity in order to prove the existence of the empty set -- and yet the statement of the axiom of infinity presupposes that the empty set exists! I think it's not possible to simultaneously: write a correct article, keep Kunen's axioms in the form he wrote them, and to omit the axiom of the null set (or whatever equivalent Kunen used). Hurkyl (talk) 03:32, 5 February 2008 (UTC)

First-order logic, with no axioms at all, proves that something exists--if you want to allow the opposite possibility you have to go out of your way to do it. Then by applying separation, you get that the empty set exists. You don't need the axiom of infinity for this. --Trovatore (talk) 03:37, 5 February 2008 (UTC)

That depends on your choice of logical axioms, or semantically speaking, on what you define to be a model. While customary axioms prove $\forall x\varphi \to \exists x\varphi$ or $\exists x(x=x)$, and customary model theory does not consider the empty set as a model, it may be convenient to also consider empty models (e.g, in algebra, when you would like to have a theorem "the intersection of two subsemigroups is a subsemigroup), and hence to use a system of logical axioms in which "there exists something" is not derivable.

In set theory we are of course not interested in empty models; all the more reason to explicitly postulate the empty set, just to make this point clear.

Since the ZFC axioms are anyway not independent of each other, I think that the derivability of the empty set axiom is not a good reason to exclude it. (The fact that Kunen excludes it, on the other hand, is a good reason. Just not a very good one.)

A reason to include it is the role that it plays in the relationship between replacement and separation. Replacement in its strict form (namely, that the class of function values is a set, not only contained in a set), implies separation in the case that the set $\{x\in z:\varphi (x)\}$ is nonempty, but you need the empty set axiom to get the full separation axiom from replacement. (Of course all this is not relevant when we use the ZFC axioms, but it might be worth a remark when we discuss them.)

Aleph4 (talk) 12:13, 5 February 2008 (UTC)

See also Talk:Axiom of empty set#Does logic imply the existence of the empty set?. JRSpriggs (talk) 09:24, 6 February 2008 (UTC)

Of course, I should have checked there... Aleph4 (talk) 14:00, 6 February 2008 (UTC)

Trovatore is right in that I didn't consider shunting the postulate that something exists off to the logical axioms -- but as Aleph4 points out, that postulate only exists in certain formulations of first-order logic. If the intent is for the article to rely on this postulate, then I assert that it needs to be explicitly stated someplace.

The problem, as I see it, is that the choices made in the article has many drawbacks. The restriction to a certain kind of logic is unnecessary, it complicates the exposition, and it diverges from traditional presentations of ZFC. The benefits are... fewer axioms?

The previous discussion sounds like Kunen's list of axioms actually did include an axiom asserting the existence of a set. Am I reading that correctly? Hurkyl (talk) 02:51, 14 February 2008 (UTC)

Well, what is standardly called "first-order logic" does imply that something exists. Modifications of FOL that avoid that implication are called free logic. --Trovatore (talk) 03:10, 14 February 2008 (UTC)

Really, the problem is with how the axiom of infinity is presented here, with the condition $\varnothing \in X$. But we can rewrite it without referring to the empty set, namely by stating instead that there exists some element of X of which nothing is an element, i.e. $\exists x[x\in X\land \forall y(y\notin x)]$. I'll see what I can do.... -- Smjg (talk) 11:43, 9 August 2010 (UTC)

(←) We should not rewrite the axiom. The axioms are taken directly from a source for verifiability. Of course we could come up with dozens of equivalent axiom systems, but then they are not the systems that we can actually verify by looking at a source. I have, in the past, checked the axioms symbol by symbol against the source.

Apart from that, on a technical level, your change wouldn't address any issues with the existence of the empty set. The symbol $\emptyset$ is just an abbreviation, it is not actually in the language of ZFC. The formula you changed to is just an unwrapping of the abbreviation. It doesn't actually change the formal axiom, and so it cannot address any perceived problems. In other words, Kunen's axiom is an abbreviation for the axiom you changed to.

More generally, I don't see what issue you are concerned about with the empty set. The issue of "at least one set exists" is covered in detail in the second paragraph of that section. — Carl (CBM · talk) 12:15, 9 August 2010 (UTC)

Perhaps a better way of translating $\varnothing \in X\,$ into the language of set theory is $\forall x(\forall y(y\notin x)\rightarrow x\in X)\,.$ Then if the empty set exists, the axiom says that X is a superset of the natural numbers; and if the empty set does not exist, the axiom says that it does exist, to wit $\varnothing =X\,$ in that case. JRSpriggs (talk) 06:50, 10 August 2010 (UTC)

That's pretty. But either translation gives that the axiom of infinity stated here implies that the empty set exists. The article points our that (since the axiom starts with an existential quantifier) the axiom implies some set exists regardless of what the matrix says, and we can use comprehension to make the empty set out of that. Then, empty set in hand, we can go back to the axiom of infinity to get an infinite set, at which point it doesn't matter too much how we translate "$\emptyset \in X$". — Carl (CBM · talk) 11:04, 10 August 2010 (UTC)

The second paragraph states that the axiom of infinity is how we find that any set exists in the first place. As has been said, all other axioms are vacuously true in a system where no sets exist at all.

The beginning of that section states "The following particular axiom set is from Kunen (1980)." It later states that Kunen included the axiom of the empty set, but goes on not to list it. As such, the axiom of infinity as written uses ∅ before we have any concept of what it means. If we're going to discard something from the source, we can't just blindly leave the rest of the source intact without regard for whether it still makes sense.

The point is that the way it is written at the moment is circular logic: existence of ∅ → axiom of infinity → existence of a set → existence of ∅. The formulation I gave doesn't rely on the preconceived notion of the empty set - it merely postulates that X has some member having no members. Therefore, it avoids the circularity. -- Smjg (talk) 13:01, 10 August 2010 (UTC)

Kunen does not include any axiom of the empty set – you must not have actually looked at the reference. He simply assumes at least one set exists, along with the axioms here. Usually, the assumption that at least one object exists is considered part of the background logic. Kunen explicitly says on p. 10:

"Under most developments of formal logic, this is derivable from the logical axioms and thus redundant to state here, but we do so for emphasis."

Now, the axiom of infinity stated here already implies "at least one set exists", so anything that can be proven from the axioms here + "at least one set exists" can also be proven from just the axioms listed here. But really you don't need any non-logical axiom to assert that at least one set exists, it's just part of first-order logic.

In any case, simply changing the matrix of the axiom of infinity cannot make any difference. The key point, from the point of view of "at least one set exists" is that the outermost quantifier is existential. There is no circularity because the axiom of infinity is assumed, not proved. — Carl (CBM · talk) 13:48, 10 August 2010 (UTC)

Sorry, I misread the beginning of paragraph 2. So Kunen implicitly assumed at least one set exists, and then derived the existence of the empty set from this and the axiom of specification. But assuming a non-empty domain of discourse is by no means universal. Then it states that the axiom of infinity is how we know that any set exists (and can therefore derive the existence of the empty set), and this is the only way in the absence of it being assumed that we know any set exists. As such, it's anomalous that we have the axiom of infinity written in a way that assumes we already know ∅ exists.

The axiom of infinity being assumed makes no difference. It can't rely on the existence of something that isn't known to exist yet. Maybe I should've been more specific: existence of ∅ → that the axiom of infinity makes sense → axiom of infinity → existence of a set → existence of ∅.

Or are you taking the view that the definition of ∅ is really embedded in the axiom, like this?

$\exists X\left[\{x\in X|x\neq x\}\in X\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

-- Smjg (talk) 15:09, 10 August 2010 (UTC)

(1) Yes, the definition of $\emptyset$ is already embedded in the axiom, because the symbol $\emptyset$ itself is not actually part of the language. Similarly, the language of ZFC does not contain set-builder notation. The only non-logical symbol in the language of ZFC is the ∈ symbol. There are no constant symbols in the language and no term-forming operations.

(2) The second paragraph does not say quite what you are describing. It says that at least one set exists by background assumptions, and also the axiom of infinity asserts that a set exists. The word "also" is key: these are separate reasons that it isn't necessary to add another axiom asserting that at least one set exists.

The assumption that at least one object exists is nearly universal in first-order logic, to the point that systems that do not have this property have a special name, free logic. Kunen himself says "most developments", rather than "some developments". Also, note my comment below about Jech's book. — Carl (CBM · talk) 16:22, 10 August 2010 (UTC)

I've just reworded the phrase about the axiom for the existence of a set, because I found it unclear (I also reworded the part about the axiom of choice because it was even more unclear, and could easily be repaired, but that is a separate matter). I did this in complete ignorance of this discussion, so maybe I've unknowingly stepped on some sensitive toes; please don't take offence but just correct. Just as a matter of personal opinion: I think it is a serious problem that the axiom of infinity should contain a symbol for the empty set, which is not part of the language, because the whole point of giving formal expressions is to remove any doubt about formalization. The question remains (given that set builder notation cannot be used) is the infinity axiom can be written properly in formal notation. Could one just replace $\varnothing \in X$ by $\exists Y\left[Y\in X\land \forall Z(Z\in Y\Rightarrow \lnot Z=Z)\right].$? But I guess this is similar to something already said above, Marc van Leeuwen (talk) 10:45, 27 April 2011 (UTC)

It's worth noting that the other natural candidate for an axiom system to use here, Jech's Set Theory, does not include either the axiom of the empty set or the axiom "at least one set exists" but Jech does point out that the latter is a consequence of the axiom of infinity. — Carl (CBM · talk) 13:52, 10 August 2010 (UTC)

I agree that as it currently stands (2 Jan 2012) the axioms are erroneous because they rely on the axiom of infinity to guarantee the existence of at least one set, but that axiom itself relies on the existence of the empty set. One way to fix that is to include an axiom that asserts the existence of the empty set, as Wolfram does and Stanford (http://plato.stanford.edu/entries/set-theory/ZF.html). The current version is neither fish nor fowl, as it appears to wish to stick as closely as possible to Kunen's version, yet it concedes that Kunen does include an axiom of the empty set. In any case, there's no point in simply importing definitions wholesale from a text without a critical overlay because every text contains some errors (the writers of such texts all being human like us).

A concise solution to the circularity would be to include the assertion of the existence of at least one set in the axiom of infinity, as follows:

$\exists X\left[\exists z(z\in X)\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

This can be readily shown to be equivalent to the existing version together with an axiom asserting the existence of the empty set.

But regardless of what solution is adopted, it cannot be left as it is, as the current presentation of the axiom of infinity uses the empty set symbol without definition, so the axiom is a malformed formula. Andrewjameskirk (talk) 20:26, 1 January 2013 (UTC)

The existence of at least one object (therefore at least one set, in this case, because all objects of discourse are sets) is a logical validity in first-order logic (though not in free logic) and follows from no axioms at all. --Trovatore (talk) 20:30, 1 January 2013 (UTC)

To Andrewjameskirk: As explained above, the subformula using the empty set symbol can be regarded as a shorthand for a more correct formula. As such it is more readable than the more formal expression.

Please show how you would derive the usual form of the axiom of infinity from your variation of it! JRSpriggs (talk) 08:28, 2 January 2013 (UTC)

To JRSpriggs: That would be fine if the shorthand is explained. At present it is not explained, which makes the formula, as presented, incorrect, because the symbol $\varnothing$ is undefined. I propose the following simple amendment that allows retention of the shorthand but explains it, in order to make it unimpeachably correct:

[add the following words after the formula]

This axiom appears to presuppose the existence of the empty set $\varnothing$, but it need not do so. In a formulation that does not include an assertion of the existence of the empty set (or of any set other than the infinite set), the subformula $\varnothing \in X$ can instead be considered as a shorthand for the more precise subformula $\forall y(\forall u(u\notin y)\Rightarrow y\in X)\,.$.

Just to see what it would look like, I'll put here what the axiom would look like with the substitution in it, fully expanded.

$\exists X\left[\forall y(\forall u(u\notin y)\Rightarrow y\in X)\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

I agree it's a bit long. So the best solution seems to be to keep the abbreviated formula and explain the shorthand, per my proposal here.

Although a slightly more concise version is available by prenexing the $\forall y$ to get:

$\exists X\forall y\left[(\forall u(u\notin y)\Rightarrow y\in X)\land (y\in X\Rightarrow S(y)\in X)\right]$ Andrewjameskirk (talk) 00:05, 22 August 2014 (UTC)

To Trovatore: Some but not all presentations of FOP logic include an assertion of a non-empty domain of discourse. It is unnecessarily restrictive to assert in the article that it is always the case in first-order logic that the domain is non-empty. A harmonious and inclusive way to deal with this would be to state at the top that the axioms are presented under the assumption that the underlying logic has a non-empty domain, and that where that is not assumed, adding an empty set axiom (as per SEP or Ito) can achieve the same result. Regardless of what approach is taken there though, the passage commencing "Second, however, even if ZFC is formulated in so-called free logic, in which it is not a theorem that something exists, the axiom of infinity (below) asserts that an infinite set exists" is circular, as it justifies the existence of the empty set via the Infinity Axiom, which itself relies on the existence of the Empty Set.Andrewjameskirk (talk) 02:43, 8 January 2013 (UTC)

If the empty set is a model, then your logic is not what is standardly called first-order logic. First-order logic has no empty models. Free logic is a different thing; it is not first-order logic as the term is standardly understood. --Trovatore (talk) 02:52, 8 January 2013 (UTC)

The axiom of infinity is not circular; the symbol $\emptyset$ is not actually in the language of ZFC, and so the axiom of infinity does not literally use this symbol. The expression we write down is simply an abbreviation for the actual axiom, which says something like

$(\exists x)[(\exists y)[y\in x\land (\forall z)[z\not \in y]]\land (\forall w)[w\in x\to (\exists v)[v\in x\land v=w\cup \{w\}]]$.

Even that last formula is still an abbreviation; the full axiom would spell out "$v=w\cup \{w\}$" in the language of ZFC. The key point, though, is that the axiom starts with an existential quantifier, so regardless of its internals it implies that at least one set exists. — Carl (CBM · talk) 12:44, 8 January 2013 (UTC)

Zermelo-Fraenkel-Skolem set theory

To my knowledge, the more inclusive name has it's third contributor - Skolem - included. The article should be changed accordingly, in my view. See: [1]. --151.202.103.127 (talk) 21:20, 12 January 2008 (UTC)

See WP:COMMONNAMES. --Trovatore (talk) 21:21, 12 January 2008 (UTC)

Equality without equality

The defining properties of equality are reflexivity (x=x) and the substitution property. The substitution property says that if x=y, then any predicate containing x implies the result of replacing some (or all) of the occurrences of x in the predicate by y. From these one can also show that equality is symmetric and transitive.

If the logic being used does not provide equality, then it can be defined as a macro (abbreviation) for the substitution property. In the case where there is only the one binary relation, ∈, this becomes ∀z[z∈x↔z∈y] ∧ ∀z[x∈z↔y∈z] . This definition works regardless of the axioms used.

However, Palnot has been putting in ∀z[z∈x↔z∈y] which is not the full definition. True, it is equivalent in the presence of the axiom of extensionality (when suitably formulated). But we should not make a definition dependent on an axiom being present. JRSpriggs (talk) 11:35, 15 April 2008 (UTC)

Rephrasing "The Axioms" intro, and Axiom of Infinity

I think it's again worth bringing up the article's inconsistent handling of the empty set and infinity. I cite three specific problems:

• The article claims to present Kunen's axioms, but to the best of my knowledge, Kunen does include an axiom 0 asserting the existence of a set. Previous revisions of the page stated that that axiom was omitted, but that seems to have been removed.

• The statement of the axiom of infinity assume makes use of the empty set symbol, which has not been previously defined.

• The discussion following infinity asserts that infinity (together with other axioms) imply the empty set, making the presentation circular. Also, given the current convention that 'first-order logic' implies the existence of an object (which is Kunen's omitted axiom), infinity is not needed to prove the existence of the empty set. (which is the original reason why the axiom was stricken from the Wikipedia article)

I think the best solution would be to actually include Kunen's axiom 0, and follow it with comments that the axiom is redundant given Wikipedia's conventions, and define the empty set there. But due to the fierce resistance against it seen in the past, I offer the following compromise:

Use this as the introductory paragraph: (addition in bold)

There are many equivalent formulations of the ZFC axioms; for a rich but somewhat dated discussion of this fact, see Fraenkel et al. (1973). The following particular axiom set is from Kunen (1980). Kunen's axiom 0 asserting the existence of a set is implied by Wikipedia's conventions regarding first order logic, and omitted from the list below. The axioms per se are expressed in the symbolism of first order logic. The associated English prose is only intended to aid the intuition.

and use this as the discussion following infinity (after mentioning omega)

... $\varnothing$ is defined to be the unique set satisfying $\forall x:x\notin \varnothing$. It's existence is assumed by this statement of infinity, and can be proven from the axiom of specification and Wikipedia's convention that first-order logic asserts a set exists. Its uniqueness follows from the axiom of extensionality.

--Hurkyl (talk) 02:17, 29 April 2008 (UTC)

This is partly an argument over what First-order logic is, and partly an argument over how to present the axiom of infinity clearly to the reader.

I disagree with having an existential assumption built into first order logic. Thus I believe that some axiom must explicitly affirm the existence of a set (in order for this to be the ZFC we know and love, which does have sets). The axiom of infinity does assert the existence of a set (intended to be an infinite set) — a set which contains any empty set which might exist and any successor of any set which might be a member of this infinite set.

The article states the axiom as:

$\exists X\left[\varnothing \in X\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

Many people would be able to (sort of) understand this version of the axiom who would be unable to understand a more correct version such as:

$\exists x\left[\forall e(\forall k\lnot (k\in e)\Rightarrow e\in x)\land \forall y\forall z([y\in x\land \forall w(w\in z\iff (w\in y\lor w=y))]\Rightarrow z\in x)\right].$

This more correct version does not assume the existence of the empty set nor of the successor of a set, but once one has it one can prove that they do exist. JRSpriggs (talk) 14:20, 29 April 2008 (UTC)

There's the third option,

$\exists x\left[\exists e(\forall k\lnot (k\in e)\land e\in x)\land \forall y\forall z([y\in x\land \forall w(w\in z\iff (w\in y\lor w=y))]\Rightarrow z\in x)\right].$

I think we can finesse the issue of free first order logic by again pointing out that Kunen (and ZFC, really) assumes that there is at least one set, and that in some formalizations this is built into the semantics of FOL.

Really, I am not fond of emphasizing the analysis of which axioms imply which other axioms. While this is of technical interest, it's only a minor point in the study of ZFC as an axiomatic framework for set theory, because ZFC does include all the axioms, regardless whether they are independent or not. So I favor solutions that don't make the reader dwell on independence too long. — Carl (CBM · talk) 15:22, 29 April 2008 (UTC)

I tend to agree with both of you. In my humble opinion, the absolute most important things are correctness and reader friendliness; my intent was a compromise with what I perceived as a resistance against reintroducing redundancy in hopes of getting an improvement accepted by the community. But if I'm just imagining things, I'd be happy to draft up a bolder suggestion. --Hurkyl (talk) 03:21, 1 May 2008 (UTC)

I added a paragraph to discuss the existence of at least one set - I am relatively satisfied by that. I also moved and lengthened the discussion of the existence of the empty set. I am less happy with that, I hope others can improve it. — Carl (CBM · talk) 12:14, 1 May 2008 (UTC)

Actually, you can prove it from Infinity and Separation without resorting to assumptions based on your interpretation of FOL (this is occasionally useful if we want to base a view of set theory on intuitionistic logic rather than bootstrapping it off of something that already uses an implicit definition of sets). Infinity is the only axiom that begins with an existential, so it cannot be satisfied in an empty universe of discourse. This means at least one set exists. Apply a contradictory formula to Separation, and voila: the empty set exists. TricksterWolf (talk) 07:49, 26 November 2011 (UTC)

Meta theory

The meta theory of anything seem to require us to have a preconception of natural numbers, set union, and subset, and also proof by induction and some other stuff. Also we are allowed to quantify over formulas. So it seems to me that the meta theory of any logic is actually the natural language version (when we read the symbols out loud) of ZF.

That's more or less right. Metatheory is standardly done in ZF (or some sub- or super-theory thereof), although usually in a rather informal style, as you note. You can, in particular, do the metatheory of ZF in ZF (or perhaps a stronger theory like ZF + "There is an inaccessible cardinal" if you want to be able to construct a model of ZF). When this is done carefully and in great formal detail, formulas, and sets thereof, are coded as sets and such metatheoretic relations as satisfaction are then defined as relations on these sets. See, for example, the text _Set Theory: An Introduction to Large Cardinals_ by Frank Drake. TXLogic

From the few things I do understand it is no way as powerful as ZF, e.g. we don't use the AC in any meta theorems, but it does seem a bit circular as ZF is supposed to make rigorous the conceptions above. I don't think it's possible to overcome this circularity without taking things like union and induction, especially natural numbers, to be true primitive knowledge like food and water. Is this how mathematicians think? Money is tight (talk) 15:44, 14 January 2010 (UTC)

There is no circularity. When formulas are coded as sets, formal systems and their models are just complex set theoretic objects. TXLogic

What use is this article?

I've never seen an article on Wikipedia that was so useless in explaining the idea to the layman is simple language. If teh editors of this article are as clever as they would wish to be seen they could have made this MUCH clearer. —Preceding unsigned comment added by 217.206.81.100 (talk) 13:39, 5 March 2010 (UTC)

Concrete suggestions are very welcome. — Carl (CBM · talk) 13:46, 5 March 2010 (UTC)

Perhaps that for which he is asking is an explanation for each axiom of why it is needed to do the usual things that mathematicians do. For example:

• Extentionality defines what a set is, the simplest structure which can be used to categorize things.
• Foundation ensures that a set is what it is intended to be by making sure that its transitive closure can only be implemented in one way.
• Empty set gives us something with which to start to build the Von Neumann universe. So that we have something rather than nothing.
• Pairing allows us to to make ordered pairs and then define functions as sets. It also allows sets to be combined before taking unions.
• Union allows sets which have been put together with pairing or replacement to be unified so that all the elements can be accessed together.
• Separation allows us to pick out the elements in which we are interested and make them a distinct set so they can be further manipulated.
• Power set allows us to combine all the subsets made with separation (or otherwise) into one object, which we could not otherwise do. It gives us access to higher cardinalities which we could not otherwise reach.
• Replacement allows classes of the same cardinality as an existing set to be made a set. It gives us the range of a function which might not otherwise be possible. It establishes the existence of larger ordinals than could otherwise be obtained. It enables definitions by transfinite recursion.
• Infinity gets us out of V_ω and into the interesting stuff.
• Choice assures us that the universe of sets has a relatively predictable structure consistent with some of our intuitions derived from finite sets.

How is that? Is that what you want? JRSpriggs (talk) 03:40, 6 March 2010 (UTC)

Well-ordering Theorem vs. Axiom of Choice

The Wellordering Theorem (WO) and AC are of course equivalent in ZFC. But I think that AC should be in the drivers seat (i.e. in the "List of Axioms" instead of WO). I have no profound reasons for this, but nonetheless, here they are:

1.) The name "The Axiom of Choice" fits better together with the other Axioms. (Important? No, but it is potentially confusing for the beginner to use WO.)

2.) Arguably, AC is much more "intuitively true" than WO - at least in my mind.

3.) The first part of the article speaks about AC and not WO.

An argument for WO instead of AC is that the reference to Kunen's book (he uses WO I suppose) needs modification.

An other argument (for or against) would be historical precedence.

YohanN7 (talk) 09:00, 8 July 2010 (UTC)

I agree — Kunen's choice is a bit idiosyncratic, I think. It does have some practical advantages in that it's often easier to check directly whether a given model satisfies WO, and a historical argument could be made on the grounds that Cantor proposed as a "law of thought" (he didn't call it an axiom) that every set can be wellordered. But then Cantor was not directly responsible for ZF.

Maybe we could take Jech as the source for the axioms instead. --Trovatore (talk) 09:11, 8 July 2010 (UTC)

B t w, a technicality: Shouldn't minimal be least in the definition of a wellorder?

Clearly, if Cantor proposed WO, that is a heavyweight argument for WO. The practical advantages of WO that you mention, on the other hand, are surely known by those actually working with that kind of problems?

Do you agree that AC is easier stated than WO?

I don't suggest a complete rewrite (contentwise) of the subsection in question, merely to swap "drivers". YohanN7 (talk) 09:44, 8 July 2010 (UTC)

On the history of things: Here is a quote from Axiom of choice: "In fact, Zermelo initially introduced the axiom of choice in order to formalize his proof of the well-ordering principle.". YohanN7 (talk) 10:20, 8 July 2010 (UTC)

The list of axioms here is taken from Kunen's book. There are benefits to taking all the axioms from one text, one of which is verifiability of the formal axioms. We could certainly switch wholesale to the axioms by Jech or some other set theory text. But we would want to go through and change all the axioms to fit that book, not just change one of them. However, Kunen's book is the standard textbook in set theory these days, so it's not an unreasonable choice. It just seems like a matter of taste which form of the axiom of choice it taken as an "axiom". — Carl (CBM · talk) 10:57, 8 July 2010 (UTC)

I'm quite happy as things are in the article for the present (was never really unhappy about it). Trovatore and Carl have good arguments (I do not have a copy of Jech's book I should say (Jech's axioms <==> Kunen's axioms)). A change might perhaps (or not) improve the article but the effort might not be worth it.

[That technical detail by the way, I still want "least element", not only "minimal";)]

It is, as Carl says, probably a matter of taste whether one prefers WO over AO. Still, this page is high priority isn't it? It should be since ZFC is pretty much math as it is taught. It should be as good and easy as possible. My personal biased opinion is that AC is a clearer statement for people having little background in math. I think that the statement of AC (biased or not) is clearer to the newcomer than WO that requires relations, linear orders on top of that, etc. /Best Regards YohanN7 (talk) 12:50, 8 July 2010 (UTC)

I just want to second the argument about naming. Having a theorem among a list of axioms is in complete contradiction with what one is doing. At first reading I was actually convinced that the list had ended, and that the section about WO was discussing the status of this theorem relative to the axioms, and it required going back and re-reading a lot of context to get me convinced that the Well-ordering theorem was actually part of the lists of axioms. (Another point that put me off is that the formal expression for the Well-ordering theorem has a rather different appearance from the others, and is, um... informal.) Couldn't it just be called "Axiom of well-ordering" without committing an infraction against Kunen? Marc van Leeuwen (talk) 11:52, 27 April 2011 (UTC)

To Marc van Leeuwen: Axioms are theorems; and it is often a matter of taste which theorems are chosen to be axioms. JRSpriggs (talk) 12:47, 27 April 2011 (UTC)

Axioms are theorems only in the strict sense of the theorem/non-theorem distinction in formal logic. But certainly this is not the reason that the well-ordering theorem is called a theorem. And looking at the theorem article, a theorem is something that requires a proof, and even if one cares to restate an axiom as a theorem with a trivial proof quoting the axiom (don't know what that is good for, but certainly possible), that does not wipe out the distinction. I agree that in an axiomatic approach one can exchange certain axioms for other ones, which implies changing axiom/theorem labels, and this is what goes on here. If one chooses to make well-ordering an axiom, then one should call it that. Marc van Leeuwen (talk) 10:00, 4 May 2011 (UTC)

The word "theorem" is part of the name of the well-ordering theorem. If we talked about the "well-ordering axiom", no one would know what we were talking about (or they would confuse it with the well-ordering principle which is different as it applies only to subsets of the natural numbers). JRSpriggs (talk) 14:31, 4 May 2011 (UTC)

Well, Kunen calls it the axiom of choice, not the wellordering theorem. If we're really following Kunen, we should call it the axiom of choice, even if we give the statement of the wellordering theorem. I agree with Marc that it's confusing to list axioms and call one of them a theorem. (It would be nice to call it something like wellordering axiom but we're not allowed to make up names.) --Trovatore (talk) 17:48, 4 May 2011 (UTC)

I do not think that we should follow Kunen (or any other author) so slavishly that we use the wrong name for a proposition. JRSpriggs (talk) 18:25, 4 May 2011 (UTC)

Well, nevertheless it is confusing to have theorem in the name. Honestly I do kind of think this is an argument for going with Jech's enumeration instead; as I said I think Kunen's is a bit idiosyncratic. There are decent pedagogical reasons for Kunen's choice (it's an easier proposition to check in the context of a given model, and the equivalence can be proved in the exercises) but in an encyclopedia article I kind of think we should use the form more usually thought of as one of the axioms. --Trovatore (talk) 20:24, 4 May 2011 (UTC)

I don't oppose switching to Jech's list of axioms. I do feel there is a benefit to having exactly the list of axioms from some reference, rather than our own list. Unfortunately, there's no "canonical" list of axioms; different authors pick different specific axioms, and even the names of the axioms are changed from one author to another (e.g. separation v. comprehension, replacement v. collection). So the best we can do is pick some author and use that list. — Carl (CBM · talk) 12:19, 6 May 2011 (UTC)

Kunen calls it "Axiom 9. Choice." The statement here is just like the one from Kunen, including the words "well orders" in the formula. The axiom was retitled from "axiom of choice" to "well ordering theorem" in our article in this edit.

In YohanN7's comment, he or she mentions "math as it is taught". That was the reason we took the axioms from Kunen's book in the first place, because it seems to be the standard textbook in set theory these days. — Carl (CBM · talk) 12:49, 27 April 2011 (UTC)

It looks messy the way it is, talking about Axiom of Choice and then... where is the Axiom of Choice? I'd suggest at least something like "9. Well-ordering theorem (equivalent to Axiom of Choice)". --Hugo Spinelli (talk) 21:00, 3 May 2011 (UTC)

For what it's worth my two pence is that I think it should be switched to the Axiom of Choice. Most introductory texts I've seen refer to the Axion of Choice. On this note, it seems peverse that the article is titled Zermelo-Franklen Set Theory then refers throughout to ZFC (the C standing for choice!), perhaps Zermelo-Franklen Set Theory (with Choice) or something. In terms of the earlier reference to keeping it all in reference to one text, I would suggest that we do so but switch to a text that uses Choice not WO, and might suggest Goldrei, "Classic set theory : a guided independent study". Whilst this change would appear to be a big undertaking all it would mean is changing WO to axiom of choice and adding the empty set axiom and keeping the other 8 the same, so it would also solve the discussion higher up this page about excluding the empty set axiom. — Preceding unsigned comment added by 129.67.169.195 (talk) 20:37, 2 June 2012 (UTC)

The problem is, we want to have a sourceable collection of axioms. Right now, the article uses the ones from Kunen. I have in the past looked commented favorably on the possibility of changing to the ones from Jech, but we can't really just go in and substitute ones that we can see personally are equivalent in context. --Trovatore (talk) 21:42, 2 June 2012 (UTC)

TXlogic here: I myself think the case for changing axiom 9 to an explicit statement of Choice is rather overwhelming. Kunen's text is excellent but his decision to axiomatize ZFC with the W.O. Theorem (and, moreover, to call it "Choice") is out of the ordinary, to say the least — of the dozen+ set theory texts I own, Kunen's is the only one that doesn't adopt a standard formulation of Choice. As for the importance of verifiability, Jech's text is certainly every bit as authoritative as Kunen's and, with the exception of Choice, his statement of the axioms is basically identical to Kunen's. I volunteer to make the change; I just don't want to go to the trouble only to have it reverted, so I'm checking here first. Jech uses essentially the formulation "Every set of nonempty sets has a choice function", which is probably the easiest version to state, so I would set the axiom up by defining the notion of a function (and hence that of an ordered pair). On a related note, I would also suggest changing all of the ugly gifs generated by the use of the math tags with proper HTML symbols. I also volunteer to do this. (TXlogic · talk) —Preceding undated comment added 20:09, 25 November 2012 (UTC)

As long as all the axioms are changed to the ones from Jech I definitely won't revert it. My concern is just that we should have a verifiable set of axioms from one text rather than cobbling them together from different places. I don't really think the case is very overwhelming, though, which I why I never made the change myself. — Carl (CBM · talk) 20:17, 25 November 2012 (UTC)

With some minor reservations I support this change. My view is that, while Kunen's choice to make the wellordering theorem an axiom and call it Choice is defensible for his own book, it is not very standard. My reservations would have to do with some other details that I don't quite remember (for example, does Jech talk about the axiom of collection rather than the axiom of replacement? That's not very standard either.) --Trovatore (talk) 22:05, 25 November 2012 (UTC)

Jech uses the term "Replacement". "Collection" (usually) signifies any of several similar but different axioms. For example, the version in KPU does not require a functional mapping on a given set A, but rather only a total mapping φ(x,y), in the sense that, for every element a ∈ A, there has to be at least one object b such that φ(a,b). Collection then says that there is a set B containing at least one such object b for every a ∈ A. Note that B could contain all sorts of other stuff as well, another big difference with Replacement. This version of Collection obviously implies Replacement. (KPU also requires that φ be ∆₀, but that's neither here nor there.) (TXlogic · talk)

a few rough spots

1) The axiom schema of collection appears exactly once in the text, when it is defined. The axiom schema of replacement is discussed extensively, but not listed as an axiom. The relation between the two is not specified within the text of the article; you have to click "axiom of replacement" (or construct a proof) in order to get the story.

2) The axiom of pairing, as listed in the article, does not state that there is a set which contains *exactly* two elements, contrary to the text. The version of the axiom of pairing which is linked to, however, does.

3) (edit: Removed as it was an error on my part)

4) In general, I believe that axioms which are redundant in ZF but not in Z belong in their own labelled section. Since most such axioms are consequences of the axiom schema of replacement, which is perhaps the most unintuitive of the ZF axioms, a few short but explicit derivations would IMO improve the article for set theory outsiders. I think it would be acceptable to alter the numbering of Kunen's axioms as this does not significantly impair verifiability.

5) There should be an explanation of the use of "a set that contains" rather than "a set that is equal to". Presumably this distinction is important when the axiom schema of specification is not assumed, but then we're not in ZF, and as it stands I think it just adds confusion for many readers.

I'm happy to try my hand at contributing, but given that the text and links seem to be at odds with the (contentious but supported, according to the talk page) axioms as written, and the fact that I am a set theory outsider, it seems best to solicit guidance first.

99.37.200.117 (talk) 03:24, 23 August 2010 (UTC)

The collection/relacement thing is mildly irritating - Kunen calls it the "replacement scheme", but some people are overly picky about "replacement" versus "collection". I edited the text there to keep the word "collection" but also include the word "replacement". I don't think it's really helpful to focus on which axioms are redundant to which others, even to the extent that we currently do. — Carl (CBM · talk) 17:37, 29 August 2010 (UTC)

Errors, Inaccuracies, and Infelicities in this Entry

1. The article is entitled "Zermelo-Fraenkel set theory" but the entry begins by talking about ZFC. "ZF" should be introduced to indicate the axioms without Choice. "ZFC" should be introduced as ZF + Choice.

2. "ZFC has a single primitive ontological notion, that of a hereditary well-founded set." ZFC is a mathematical theory, i.e., a set of axioms in a first-order language (at least, in the article — there are of course higher-order versions as well). Its ontological commitments are the stuff of philosophy and belong in an entry on the philosophy of mathematics, not here. The entire notion of an ontological primitive is out of place. The only appropriate notion here is that of a primitive of the *language* — as in fact noted in the following paragraph. It seems to me that, at the least, the first sentence of this paragraph ought to go.

3. "Most of the ZFC axioms state the existence of particular sets." False. Only the axiom of infinity does. The rest of the axioms (with the exception of extensionality) tell you that certain sets exist GIVEN certain others.

4. "In 1908, Ernst Zermelo proposed the first axiomatic set theory, Zermelo set theory. This axiomatic theory did not allow the construction of the ordinal numbers." Completely false. In fact, Zermelo did not construct what we now think of as the ordinals, which were defined by Mirimanoff and later, and to greater effect, by von Neumann. But the ordinals are perfectly able to be defined in in Z set theory: An ordinal is a transitive set that is well-ordered by membership. What IS true is that, in Z set theory, one can't prove that there are any ordinals ≥ ω+ω. But that is another matter altogether.

5. "Many authors require a nonempty domain of discourse as part of the semantics of the first-order logic in which ZFC is formalized." Misleading at best. It is a *requirement* of the semantics of first-order logic that the domain of discourse be nonempty. Logics that allow non-empty domains are so-called FREE logics. No set theory text in existence uses anything but classical first-order logic. (Bencivenga published a paper on set theory with free logic, but it's little more than a curiosity.)

6. "Also the axiom of infinity (below) also implies that at least one set exists..." True but irrelevant to the point. That something exists (hence, in the context of ZF, that a set exists) is simply a theorem of the underlying first-order logic of ZF set theory.

7. Set abstraction {x ∈ y | ... } is introduced without explanation or any formal underpinnings in the definition of the empty set. It would not take much to clarify and justify the notation on the basis of Separation and Extensionality.

8. Upper case variables suddenly appear on the scene in the Union axiom. Granted, Kunen does this himself, but the effect is confusing to the reader.

9. As others have noted, it is just nutty to introduce an axiom called the Well-ordering THEOREM. The axioms of a first-order theory are those sentences of the language of the theory that are simply given without proof. The theorems of a theory are those statements of the theory that are provable from the axioms. Granted, every axiom is trivially provable from itself, but it is highly confusing (and, to my knowledge, completely unprecedented) to use the word "theorem" as part of the name of an axiom. It is very confusing. Kunen calls it "Choice". Why you are so dedicated to preserving every detail of Kunen's axiomatization and yet depart from him in this entirely confusing and nonstandard way is baffling. But, even more to the point...

10. As others have also noted, it is simply a really bad idea to use the well-ordering theorem as an axiom. The main reason is that it utterly destroys the self-contained character of the entry. The proper background for the making sense of the well-ordering theorem requires the entire set theoretic analysis of binary relations, including the notion of an ordered pair, which makes no appearance at all in the article. The slavish devotion to the precise details of Kunen's axiomatization basically undermines the usefulness of the article, and it could be completely avoided by using a standard version of Choice, e.g.,

 ∀x[∀y(y ∈ x → (y ≠ ∅ ∧ ∀z((z ∈ x ∧ z ≠ y) → y ∩ z = ∅))) → ∃z∀y(y ∈ x → ∃!w(w ∈ y ∧ w ∈ z))]

where ∃! is the quantifier "there is exactly one".

There is discussion of a version of Choice that says there is a choice function for every nonempty set of nonempty sets, but this has the same liabilities as using the well-ordering version of Choice, namely, that it requires the notion of a function to be defined or the presentation again fails to be self-contained.

11. "At stage 0 there are no sets yet." More accurately, stage 0 is the empty set, at least on most standard presentations of the cumulative hierarchy.

12. "It is provable that a set is in V if and only if the set is pure and well-founded." No notion of "purity" has been defined, nor is one necessary. All sets are "pure" in ZF, i.e., free of urelements in their transitive closures. More seriously, the statement in question is NOT provable, at least, not in ZF — as noted at the beginning of the article, ZF does not countenance proper classes. Of course, reference to V could be explained away as shorthand for talk of formulas, but that once again will require a lot of background that is missing from the entry (and would arguably not be appropriate in this sort of entry anyway).

13. "It is possible to change the definition of V..." But V was never defined in the first place; how is it possible to change a definition that was never given? Furthermore, it is just wrong to characterize the constructible universe as a change in the definition of V. In fact, it is critical to the axiom of constructibility that the definition is NOT changed; otherwise "V = L" would be trivial.

14. "NBG and ZFC are equivalent set theories in the sense that any theorem not mentioning classes and provable in one theory can be proved in the other." The correct way to say this is that NBG is a *conservative extension* of ZFC, not that the two theories are equivalent.

15. The point of Abian and LaMacchia's work is unclear — is its significance the fact that it demostrates the independence of certain of the axioms relative to others?

16. "Because non-well-founded set theory is a model of ZFC..." This is incoherent; well-founded set theory is a THEORY, not a MODEL. What is intended here, I think is that the *consistency* of non-well-founded set theory (relative to ZF) shows that the axiom of regularity is independent of the other ZFC axioms.

17. "If consistent, ZFC cannot prove the existence of the inaccessible cardinals that category theory requires." Inaccessible cardinals are introduced here without definition. And the allusion to category theory is completely out of place; it means nothing to the average reader. And why bring category theory into play at all, as if that were the only motivation there is for introducing inaccessibles? Inaccessibles came on the scene in the history of ZFC LONG before category theory was a gleam in MacLane's eye (and they are profoundly important in Zermelo's 1930 analysis of the cumulative hierarchy).

Finally, virtually all browsers in the world support HTML symbols. The ugly graphical formulas should be removed in favor of HTML. — Preceding unsigned comment added by TXlogic (talk • contribs) 22:19, 19 February 2012 (UTC)

To TXlogic: Most of these complaints are just nit-picking. Some are significant, but need to be dealt with individually. Notice that you are free to try to fix these problems yourself, but others may revert you or further change your work.

Sure, whatever. I'm not sure what counts as a nit and what doesn't, it's a sliding scale. I simply listed errors, inaccuracies and other problems as I found them. I will try to find the time to fix the more significant problems. (TXLogic)

More importantly, your version of the axiom of choice is mistaken. It would be satisfied by any model of ZF, just take z to be the union of x. You left out the essential feature that not more than one element is chosen from each element of x. For correct statements of the axiom of choice, see Talk:Axiom of choice/Archive 5#Unclear. JRSpriggs (talk) 05:58, 20 February 2012 (UTC)

You are of course correct — at one point there was a uniqueness quantifier ∃! there but it seems I managed to omit it in the course of editing my comments. Hm, but come to think of it, that alone wouldn't have been quite right, as you need to ensure that the members of the original set are disjoint. I've fixed the statement above accordingly; I also removed the assumption that x is nonempty, which is not necessary. But, now that I look at it, it might be better after all to use the version that asserts the existence of a choice function, which is much simpler (and, FWIW, is the version I always use, which I suppose I mention as a weak sauce excuse for borking the version I had originally written out above):

 ∀x(∀y(y ∈ x → y ≠ ∅) → ∃f(Function(f) ∧ ∀y(y ∈ x → f(y) ∈ y)))

Of course, "Function(f)" and the notation "f(y)" would have to be defined. (TXLogic)

I agree with User:TXlogic that talk about "ontological notions" is a bit misplaced. Perhaps "primitive notion" or "undefined notion"? Tkuvho (talk) 09:02, 20 February 2012 (UTC)

I think it is best to avoid the suggestion that ZFC, the mathematical theory, contains any "notions" at all; ZFC is simply a certain type of mathematical object, a formal system. Of course, you want to say something about what the intended meaning of the sentences in that system. But I think all you want to say is that the language of set theory contains a single primitive 2-place predicate designed to express the relation "is a member of". (TXLogic)

The purpose of the second paragraph is to clarify that ZFC does not deal directly with urelements nor proper classes, unlike some other set theories. At the same time, this article should ideally (if it was perfect) cover all aspects of ZFC, including philosophical ones, not only mathematical aspects. I think that someone unfamiliar with ZFC would likely find the second paragraph informative in terms of explaining the motivation behind the theory. — Carl (CBM · talk) 13:49, 20 February 2012 (UTC)

"primitive ontological notion" could be replaced by "primitive (undefined) notion" which is clearer. Talking about ontology tends to imply a commitment to "ontological reality" of set-theoretic concepts which is unnecessary and sometimes harmful. Tkuvho (talk) 13:54, 20 February 2012 (UTC)

It is true that there is only one undefined notion, that of a "set", but the paragraph is saying that that undefined notion is intended to represent, not just that the undefined notion is named "set". The intention (of those who developed ZFC) is that ZFC is supposed to capture the cumulative hierarchy of hereditary well-founded sets, when this is viewed as a pre-existing structure outside of ZFC. Kunen discusses this some on pp. 8-9. (Similarly, Euclid's axioms are intended to formalize, among other things, the pre-existing collection of lines on the Euclidean plane, although "line" is an undefined term in the theory itself.) — Carl (CBM · talk) 14:03, 20 February 2012 (UTC)

The fact that "set" is intended to "represent" is already implied by "primitive". I agree with what you wrote but "ontological" is still not as good as "undefined". Tkuvho (talk) 14:06, 20 February 2012 (UTC)

Perhaps "unanalyzed" is better than "underfined"? Tkuvho (talk) 14:07, 20 February 2012 (UTC)

I am OK with "primitive" instead of "ontological". The trouble is the the notion of set was both defined and analysed before the ZFC axioms were created, and the axioms were intended to capture this notion. So when we say "undefined" it could sound like we mean "undefined in the metatheory" when we really mean "undefined in the object theory". The same thing happens for numbers: the concept of a natural number was both defined and analyzed before the Peano axioms were created, but these axioms treat "number" as an undefined term. In modern language we don't often say "undefined term" in the latter sense, we just specify the signature of the formal language. — Carl (CBM · talk) 14:12, 20 February 2012 (UTC)

It is not true that SET is an undefined notion in ZFC (if we must talk of notions); there simply is no such notion in ZFC. The only undefined notion is MEMBERSHIP. The undefined, i.e., primitive, notions of a theory are those intuitively expressed by the primitive, non-logical vocabulary of the theory, the axioms of which are designed to capture those notions formally. SET is a primitive notion in ZFCU, i.e., ZFC with urelements, because there is actually a non-trivial predicate "SET" which is axiomatized accordingly. But there is no such predicate, and there are no such axioms, in ZFC. So, while I think it would be natural and helpful to point out that, INTUITIVELY, sets are the things taken to be in the range of the quantifiers of ZFC, I think it would be confusing to say that SET is an undefined notion of the theory and thereby disconnect the idea of the primitive NOTIONS of a theory from the primitive non-logical VOCABULARY of the theory. (TXLogic) —Preceding undated comment added 19:10, 20 February 2012 (UTC).

Eliminating the notion of "set" from this page will not improve readability. What you seem to be suggesting is that this page should focus uniquely on syntax and avoid discussion of sematics altogether. Formally speaking this may be preferable, but not practically speaking. In principle we could replace every occurrence of "set" by "widget" and speak of ZFC as the theory of widgets. Such an approach would be mathematically rigorous and untainted by ontological considerations, but would it be any more useful than defining a function as a "correspondence" rather than a "rule" in the lead of function (mathematics)? Tkuvho (talk) 08:52, 21 February 2012 (UTC)

Nortexoid's four edits on 24 October 2012

Nortexoid (talk · contribs) made four edits to this article on 24 October 2012 (UTC). I reverted them. He challenged this on my talk page. My problems with his edits are as follows:

• Generally, details which might be useful to some readers were removed in several cases.
• The axiom of infinity (perhaps in combination with the axiom of separation) does imply the existence of the empty set. Yet the statement to that effect was removed. However one expands the axiom of infinity to account for the constant symbol for the empty set (by adding "$\land \forall w(\lnot w\in \varnothing )\,$" at the end, by replacing "$\varnothing \in X\,$" with "$\exists z(\forall w(\lnot w\in z)\land z\in X)\,$", or by replacing it with "$\forall z(\forall w(\lnot w\in z)\rightarrow z\in X)\,$"), it will still imply the existence of that set.
• Stressing that the uniqueness of the emptyset means its independence of "w" may help some readers who would otherwise assume that there is merely one emptyset per "w".
• He said "... the axiom schema of separation implies the existence of at least one set from which the empty set can be 'separated'." which is false. The axiom schema of separation alone does not imply the existence of anything.
• How would one say that a set has an infinite number of members? The method used in the axiom of infinity is at least as good as any other method. So using "immediate consequence" is pointless and confusing.

JRSpriggs (talk) 07:09, 26 October 2012 (UTC)

• Not if there are urelements. The axioms then need to be relativized to sets. I see now, however, that there is some strange passage in the intro which states "The axioms of ZFC prevent its models from containing urelements" which is obviously false without any specific formulation of ZFC having yet been given. And of course there are formulations of ZFC with urelements. The statement should perhaps say instead that the formulation of ZFC given in the article does not allow for urelements.
• Not charitable, since it is was fairly clear that I meant in conjunction with the other axioms. The ellipses in the passage you quote was filled with "The axiom of the empty set is implied by the nine axioms presented here since..."
• This point is hardly important, but in any case the axiom asserts the existence of *one* particular infinite set, viz. omega. Since that set is infinite, the axiom implies the existence of *at least* one infinite set. But it does not "more colloquially" assert the existence of at least one infinite set. There are better candidates for that statement such as "there is a set X, proper subset Y of X, and one-one correspondence between X and Y".

— Preceding unsigned comment added by Nortexoid (talk • contribs) 19:31, 26 October 2012‎ (UTC)

To Nortexoid: Please do not mix your comments in with mine. It is very hard to read and confusing. I have separated them out to avoid the appearance that I have gone mad and argued with myself. JRSpriggs (talk) 04:31, 27 October 2012 (UTC)

• ZFC-with-urelements is not ZFC. It is a separate theory with different axioms. Thus the statement that ZFC forbids urelements remains true.
• No, it was not clear what you 'meant'. In any case, your statement is still wrong because it says that the axiom of separation is used twice when it is only used once.
• You have not defined infinite set, but rather Dedekind-infinite set (a simpler concept).

JRSpriggs (talk) 04:47, 27 October 2012 (UTC)

• The ZF developed in Supppes permits urelements. See esp. p. 20. To say that it is thereby not ZF is a strange remark.
• It says the axiom is used 'twice'? As a native English speaker, I don't get that reading. I sort of see what you mean, but as I said, that is simply not a charitable reading of the sentence, nor one anyone would likely hear.
• Since we are talking about ZFC, emphasis on 'C', the two are equivalent. Take a look at the article you link to which states that in the presence of choice, a set is infinite iff it is Dedekind-infinite. I should add that I said "a better candidate" in any case, so even if you didn't like Choice, it was just an example of a sentence which, for some notion of infinity, literally says there is an infinite set. The axiom of infinity still doesn't say that, I'm afraid.

Nortexoid (talk) 08:51, 27 October 2012 (UTC)

Whatever Suppes does, if a system of set theory admits urelements then it is not the theory "ZFC" described in this article - "ZFC with urelements" is a very different theory.

I looked at the diff for the four edits just now, and I do not see that it was an improvement overall to the previous text. Parts of it seemed less clear, e.g. "The existence of the empty set is unique", but most of it just seemed to be a rephrasing.

In general, apart from these edits, I don't think it's worth spending too much time on how to prove "some set exists". It is a side note only that certain axioms imply this, since the underlying logic already implies it, and because nobody studies empty models of set theory. — Carl (CBM · talk) 18:12, 27 October 2012 (UTC)

• ZFC with urelements just is not a "very different theory" since it's just ZFC with the axioms relativized to sets and, usually, and separate axiom for the empty set. Also, and as I've already stated, the article should just say that it's not interested in urelements instead of stating something false. You're right though--it's not a big deal. But still. Nortexoid (talk) 22:47, 27 October 2012 (UTC)

The second paragraph of the lede begins, "ZFC is intended to formalize a single primitive notion, that of a hereditary well-founded set, so that all entities in the universe of discourse are such sets. Thus the axioms of ZFC refer only to sets, not to urelements (elements of sets which are not themselves sets) or classes (collections of mathematical objects defined by a property shared by their members).". I can't think of a much more direct way for the article to say that. — Carl (CBM · talk) 23:25, 27 October 2012 (UTC)

That paragraph makes it sound like no formulation of ZFC could have urelements. It needs to be phrased more cautiously. Nortexoid (talk) 10:31, 28 October 2012 (UTC)

In fact, Zermelo's 1908 (very informal) axiomatization included urelements. That said, it seems to me that the article should reflect modern usage. The fact is that "ZFC" is used pretty much universally among set theorists and logicians to refer to axiomatizations that have only the membership predicate as primitive and, hence, whose quantifiers are intended to range over pure sets only. On that understanding, it is indeed the case that no formulation of ZFC could have urelements. When urelements are allowed (i) a new predicate (for either sets or urelements) is introduced, (ii) an axiom is introduced saying that only sets have members (and in some formulations, an axiom saying that urelements exist (indeed perhaps "proper class" many, as in Harvey Friedman's formulation), (iii) most of the usual axioms of ZFC are qualified so they only apply to sets, and (iv) the new theory is referred to as "ZFCU" or "ZFC with urelements". As JRSpriggs emphasizes, when you alter ZFC to accommodate urelements, you no longer have ZFC, you have a different (albeit importantly related) theory. TXLogic —Preceding undated comment added 16:50, 19 November 2012 (UTC)

Without the axiom of separation

TXlogic (talk · contribs) says that we need neither the axiom of the empty set nor the axiom schema of separation. He thinks that the axiom of infinity will give us the empty set. But that is not so clear to me. Please show how one can prove the existence of the empty set, if one:

• omits the axiom of the empty set;
• omits the axiom schema of separation; and
• uses the axiom of infinity in the form $\exists X\left[\forall z(\forall w(\lnot w\in z)\rightarrow z\in X)\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

It appears to me that to get the empty set from this version of infinity without using separation, one would need to establish the existence of a transitive set (such as the transitive closure of the infinite set X) and then apply the axiom of regularity. Can you show that without first using separation to extract the true natural numbers from X? JRSpriggs (talk) 04:57, 23 November 2012 (UTC)

My guess is they were thinking of the axiom of infinity as

$\exists X\left[\exists z(\forall w(\lnot w\in z)\land z\in X)\land \forall y(y\in X\Rightarrow S(y)\in X)\right].$

I looked for it but I don't see the claim you mention in the article. — Carl (CBM · talk) 12:38, 23 November 2012 (UTC)

TXlogic (talk · contribs) here. JRSpriggs (talk · contribs): As Carl notes, I never claimed that the existence of the empty set follows from the axiom of infinity. I only claimed that the existence of some set follows from it (trivially, in first-order logic (since it's a logical theorem) and immediately in free logic (since "a set exists" follows immediately from "an infinite set exists"). However, just to respond, of course you need the axiom schema of Separation (or Replacement) to prove that the empty set exists from the existence of an arbitrary set (infinite or not). The empty set axiom is superfluous in the context of the other axioms (as clarified in the exposition of Separation in the article); it would be redundant to add it as an axiom of ZFC because it is derivable from Separation (or, in free logic, Separation+Infinity). TXlogic

I am sorry for bothering you with my mistake. I think that I saw your sentence "Hence, there is no need for a separate axiom." (referring to the axiom of the empty set) and misread it as "... there is no need for an axiom of separation.". I was reading the diff and the variation in colors made it hard to concentrate on the content. JRSpriggs (talk) 05:57, 24 November 2012 (UTC)

Now that you mention it, that sentence could use some sharpening up. TXlogic —Preceding undated comment added 19:15, 25 November 2012 (UTC)

Power set axiom

Chetrasho (talk · contribs) inserted mistaken information on the power set axiom. When I reverted him, he reverted me, saying "Superset is an undefined term linking to subset. A power set is a SET and not a class. Also, copied corrected axiom from axiom of power set".

• However as the text before the list of axioms says "The following particular axiom set is from Kunen (1980).". So we are not free to use just any version of the power set axiom (such as the one at axiom of power set). We must use the particular version in Kunen which is as the article stated before Chetrasho's change.
• "Superset" is a well-known term for the correlative (inverse) of "subset", that is, A is a superset of B just when B is a subset of A. It is defined clearly in the article on subsets.
• To get the version of the power set axiom in the article on it, you must apply the axiom schema of separation to Kunen's version to remove any excess elements which are not subsets of the base set. Until you do that, you only know that the power "set" is a subclass of the set whose existence is guaranteed by Kunen's version of the power set axiom.

Therefore, I will revert again. JRSpriggs (talk) 02:13, 28 January 2013 (UTC)

Edits

Thanks for explaining about Kunen. Sorry for missing out on that part. I still thought the section was unclear, so I made the following edits based on your input:

• Subset is clearly defined and used throughout.

• Kunen's Axiom of Power Set is clearly stated.

• The power set is clearly defined using the axiom of power set and the axiom schema of specification.

Chetrasho (talk) 16:00, 5 February 2013 (UTC)

— Preceding unsigned comment added by Chetrasho (talk • contribs) 15:56, 5 February 2013 (UTC) 

Confusing edit by Arthur Rubin

In [2] Arthur Rubin claimed I added the text "in which you cannot prove that something exists" when in fact according to Wikiblame it was added by User:Crasshopper in this edit. Additionally he appears to have accidentally reverted CBM's edit with no explanation. (Update: he reverted the revert, looks like edit conflict - I made a minor fix to complete CBM's edit). Dcoetzee 14:49, 3 September 2013 (UTC)

My apologies. I still don't think your edits are particularly good, but I'm an expert, so I may not understand the nuances as seen by non-experts. — Arthur Rubin (talk) 15:37, 3 September 2013 (UTC)

The edits are intended to make the material more accessible for people with only a basic entry-level introduction to set theory (and who tend to be confused by first-order logic statements with many quantifiers). I invite any specific improvements or criticism you can raise. Dcoetzee 15:41, 3 September 2013 (UTC)

"It is not a theorem that X" is jargon. Crasshopper (talk) 04:04, 4 September 2013 (UTC)

Missing reference

Shoenfield (1977) is cited twice with no explanation of what it is. 86.166.163.239 (talk) 13:15, 19 May 2015 (UTC)

Presumably, that's

J. R. Shoenfield, Axioms of set theory,

in

Barwise, K. J. Editor (1977) Handbook of Mathematical Logic. xi+1165 pages ISBN 0-7204-2285-X.

But we really should ask user CBM (talk · contribs) who added the section on the cumulative hierarchy in 2009, I think (diff). – Tobias Bergemann (talk) 10:15, 28 August 2015 (UTC)

Yes, that's right. No idea where the reference might have gone, or why I wouldn't have put it in. Good spot, IP. — Carl (CBM · talk) 10:44, 28 August 2015 (UTC)

Recent changes to union axiom

User:46.109.150.165 has changed the formal statement of the union axiom from

$\forall {\mathcal {F}}\,\exists A\,\forall Y\,\forall x[(x\in Y\land Y\in {\mathcal {F}})\Rightarrow x\in A]$

to

$\forall {\mathcal {F}}\,\exists A\,\forall x\,[x\in A\iff \exists Y\,(x\in Y\land Y\in {\mathcal {F}})]$.

Now, it appears to me that the new version is the one I probably would have thought of as the axiom of union. It says $\cup {\mathcal {F}}$ exists, whereas the old version says there is a set including $\cup {\mathcal {F}}$. These are equivalent, given separation, so it doesn't make very much actual difference.

But the question is, which version is in the source we're using? I can't remember whether we're using Kunen or Jech these days. Is there someone else who's willing to sort this out, so I don't have to? --Trovatore (talk) 07:21, 23 January 2016 (UTC)

For what it's worth, the article itself claims to use the axiom set from Kunen: "There are many equivalent formulations of the ZFC axioms... The following particular axiom set is from Kunen (1980)." — Tobias Bergemann (talk) 08:31, 23 January 2016 (UTC)

Thanks, Tobias. --Trovatore (talk) 19:56, 23 January 2016 (UTC)

I am not an expert in this field, and am thus uncomfortable editing the page itself, but it does seem to me that regardless of the formulation used, the formal statement and English description should match (as much as it's possible for an informal statement to match a formal one). The entry for the Axiom of Union starts with the English sentence: "The union over the elements of a set exists.", then gives an example, and proceeds to say, "Formally, for any set of sets ${\mathcal {F}}$ there is a set $A$ containing every element that is a member of some member of ${\mathcal {F}}$". The former sentence corresponds to the formal statement with the biconditional, whereas the latter corresponds to the one with the conditional. I realize that the two statements are equivalent given the other axioms, but it seems to me that the equivalence between formal statements and informal descriptions of individual axioms should be immediate, rather than dependent on other axioms. In other words, I disagree with the claim that "it doesn't make very much actual difference". While it makes little difference with respect to mathematical validity, it has the potential to make significant difference with respect to clarity and accessibility. Even a trivial deduction like this one can be non-trivial to someone who's trying to understand a significant amount of new information, particularly one not used to making such formal inferences on a regular basis. Therefore I would suggest that whichever formal statement is used, the English statement corresponding to the other should be either removed or edited to agree with it. I don't know how important it is to stick to the formulation given by a particular mathematician, and I'll leave consideration of that question to the experts, but from my non-expert point of view, it seems preferable to go with the biconditional version (and edit the non-corresponding sentence to match it: something like "Formally, for any set of sets ${\mathcal {F}}$ there is a set $A$ containing exactly those elements that are members of some member of ${\mathcal {F}}$ ) simply because the entry is titled "The Axiom of Union", and that statement more closely captures the usual notion of set union. Also, that's the version given in the main "Axiom of Union" article. Alternatively, the title of the entry could be changed, or, at the very least, a note could be added that clarifies why the two (informal) statements are equivalent. 207.165.235.61 (talk) 18:48, 21 July 2016 (UTC)(I know I had an account at some point, but I can't find it, so I'm sorry about that)

Proper classes

There's been an unfortunate slow-motion edit war recently over this text:

Unlike von Neumann–Bernays–Gödel set theory and Morse–Kelley set theory (MK), ZFC does not admit the existence of proper classes. These ontological restrictions are required for ZFC to avoid Russell's paradox, but critics argue these restrictions make the ZFC axioms fail to capture the informal concept of set.

I doubt that any of us are in disagreement over the actual state of affairs, so the real problem is to find adequate wording. Can we agree on these points?

• ZFC considered literally, as a collection of purely syntactic strings in a formal language, does not have any symbols that correspond to proper classes. That's just a fact. If it needs a source, it won't be hard to find.
• On the other hand, there are quite standard uses of (definable, maybe with parameters) proper classes in reasoning that can be straightforwardly if perhaps tediously formalized in ZFC. Mathematicians who make use of these may still be quite happy to think of their arguments as being "ZFC-arguments", whatever that means exactly.

If we agree on those, then we should be able to come to some agreement on wording.

There's another, broader point I'd like to bring up about that section. The language in question is in a section that starts with "ZFC has been criticized both for being excessively strong and for being excessively weak", and the bit about proper classes seems to be relevant to arguing for a strengthening. But proper classes really are not much of a strengthening of ZFC. NBG is a conservative extension of ZFC, and Kelley–Morse is only very slightly stronger. The strengthenings relevant to the research of the last half-century or so are more along the lines of large-cardinal axioms (though certainly not limited to them). But large cardinals are not mentioned here at all, which I think is a fairly serious omission. --Trovatore (talk) 05:42, 28 January 2016 (UTC)