Talk:Zermelo–Fraenkel set theory

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 as a matter of course. 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)

After looking at the rest of this talk page (I had previously skimmed it for references to the Axiom of Union specifically) I see that the same basic issue once existed with the Axiom of Power set. The treatment of that axiom in the current article seems much clearer to me, and I think the same approach would work well here. Since no one has disputed that version in the past few years, and the situation is basically identical (i.e. the formal statement from the source only asserts the existence of a superset of the more natural set, which can then be constructed by separation) I now feel confident enough to make the edit myself.207.165.235.61 (talk) 19:51, 21 July 2016 (UTC)

At some point, User:CBM had checked that the axioms were identical to the published source. I don't know whether that's really necessary, but it does short-circuit a lot of arguments. Different formulations, though equivalent when taken all together, sometimes give you surprises when you start removing or weakening axioms, so there is some advantage to having a source that we can cite for the exact set of axioms. --Trovatore (talk) 20:11, 21 July 2016 (UTC)

That makes sense. I left the formal statement as is and just mentioned that while $A$ needn't be $\cup {\mathcal {F}}$, the existence of $\cup {\mathcal {F}}$ follows from separation. My wording could conceivably be better, if you want to have a look, but I think it clarifies things without giving up either the source formulation or the more natural notion that $\cup {\mathcal {F}}$ exists.207.165.235.61 (talk) 20:36, 21 July 2016 (UTC)

I just had to change the formulation of the Uni on Axiom to be identital to the one in the main article, [[1]]. The reason is that during a lecture to my students, I used the previous formula, and easily found that it implies the existence of a universal set. — Preceding unsigned comment added by Vlad Patryshev (talk • contribs) 17:51, 18 November 2017 (UTC)

In *this* article, we use the exact axioms from Kunen's textbook, so that we have a matching set. Perhaps you could explain how the axiom from Kunen's book implies the existence of a universal set? The axiom that you replaced it with implies Kunen's axiom in any case... — Carl (CBM · talk) 18:08, 18 November 2017 (UTC)

Ok, thank you. I guess I was wrong; this formula, although not exactly original, is equivalent to the original, with the separation axiom. Sorry. Vlad Patryshev (talk) 23:45, 18 November 2017 (UTC)

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)

Please use upper-case for sets and lower for elements

For human-readers is better to see sets with upper-case labels, when possible. Example:

• $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]$     is ugly
• $\forall X\forall Y[\forall z(z\in X\Leftrightarrow z\in Y)\Rightarrow X=Y]$     is better

The intention in an encyclopedic article is also to be didactic. Krauss (talk)

In ZFC, elements of sets are also sets, so x, y, and z are all sets. In any case, we take the axioms directly from Kunen's book for consistency, so if everything is lowercase there it will also be lowercase here. Have you checked what case Kunen uses? — Carl (CBM · talk) 10:39, 14 November 2017 (UTC)

The convention is to use upperclass letters for second-order variables. — Charles Stewart (talk) 11:26, 14 November 2017 (UTC)

Kunen's axioms

Right now, we use the axioms from Kunen (1980), with only a few typographical changes (e.g. we don't have bounded quantifiers, and we sometimes rename variables). I have just double checked this against the source. I wanted to explain the reasoning behind using the axioms from a single text in this article. There are several reasons:

1. For verifiability: if we simply allow editors to write axioms from memory, the resulting list becomes unverifiable.
2. For correctness. There are many variations of individual axioms that are harmless when the full set of axioms is taken into account, but which make a difference when only some of the other axioms are taken into account. By using a single set of axioms from one source, we ensure that there are no subtle issues with the way the particular axioms have been stated.
3. Reducing arguments. There are many ways to formulate the individual axioms, some of which are obviously correct and some of which are not. Rather than wasting time discussing/arguing these things, we can use a single set of axioms which we know to be correct, so that we can focus editor time on other things.

There is no particular reason that Kunen's book was chosen, apart from its role as a standard text and reference for set theory. Some other well respected text could also be used; the key point is that all the axioms come from the same place. — Carl (CBM · talk) 18:24, 18 November 2017 (UTC)

Neither cognitive nor didactic

The article is a complete mess. In order to understand the introductory section of the article a reader must understand many notions internally linked. When reader learns all about Russel paradox, axiom of choice, ..., metamathematics, consistency she might want to rewrite whole article, maybe this way:

• change the article title to Axiomatic set theory
• start with Language of Set Theory (LST) definition (basic symbols, list of variables, atomic formula, formula, standard abbreviations)
• list of axioms (extensionability, empty set, pairing, union, separation scheme, replacement scheme, power set, infinity, foundation, axiom of choice)
  • proofs in principle, proofs in practice
  • interpretations
  • new sets from old
• classes, class terms, and recursions
• etc, etc

So, each new section shall be described and based on the previous ones.

History of the theory shall be contained in footnotes or branched to a new article(s)--ASKechris (talk) 15:13, 8 January 2018 (UTC)

One thing more: no need for references from XX century, except maybe for historical reasons.--ASKechris (talk) 15:16, 8 January 2018 (UTC)

A separate article on axiomatic set theory, something along those lines, sounds very reasonable. Then it would not be so tightly tied to the "ZFC" concept. One challenge is always with finding a way to write reasonably within the framework of Wikipedia's verifiability and "original research" policies - even uncontroversial things such as the way I would imaging writing "proofs in principle vs. proofs in practice" might be claimed to be "original research". At the moment axiomatic set theory points to a section of set theory. — Carl (CBM · talk) 17:50, 8 January 2018 (UTC)

Agreed to all your points. As to the framework of Wikipedia, the most reasonable rule of that framework is WP:IGNORE--ASKechris (talk) 23:35, 8 January 2018 (UTC)

The set theory article is already linked in the first sentence of this article and provides the general background you want. JRSpriggs (talk) 05:45, 9 January 2018 (UTC)

I'm not looking for any background. What I've wanted to see is given above, prefixed with *.--BTZorbas (talk) 18:05, 13 January 2018 (UTC)

Wikipedia is a reference work, not a textbook. The article is not a course in mathematical logic. So no, we don't want to start from the ground up. We want to talk about the subject matter of the article, which is ZF(C) specifically, not formal first-order theories in general.

So things like discussions of "proofs in general" and "proofs in practice", or what an atomic formula is, belong in other articles, which are linked to from this one.

That said, the organization of this article could stand to be tightened. The lead is too long and suffers from lack of a coherent narrative flow, and the article as a whole kind of has the same issue. At a quick glance, it just seems to be a lot of stuff jammed together, without an overarching structure that the reader can easily grasp.

That's an easy problem to diagnose but a hard one to solve. I don't have any clear plan to offer. But I don't think your outline is going to be the way to go. --Trovatore (talk) 05:14, 14 January 2018 (UTC)

I do not understand meaning of "a reference work". Wikipedia is rejected as a reference (work) by academia. (Some survey shows that 72% of colleges and universities rejected Wikipedia as a reference.) My only concern is the article reader: who is (s)he? If we assume (s)he is an average educated person which math education is at a secondary school level, then this article hardly could attract attention of such reader. The introductory is completely useless. In the article there exists an implicitly defined LST which is cumbersome and outdated. My proposal of the LST excludes mentioning the first order logic. I do not think that this article shall have links to separate article for each of the axioms for these axioms shall not be separated that way. Von Neumann shall not be mentioned before "new sets from old", etc., etc. At the end, why to use almost 40 year old references here for the core of this theory description?--BTZorbas (talk) 17:40, 24 January 2018 (UTC)

What "reference work" means is, it's a place you go to look things up, not a text that attempts to teach you the material. That's what encyclopedias are. At the university level, you should not be citing encyclopedias (whether Wikipedia or print encyclopedias) — you should look up the sources the encyclopedias cite, read those, and cite them instead.

There is no reason to avoid 40-year-old sources; while a great deal of work has been done in set theory in that time, the stuff at the level of this article has essentially not changed at all.

This article is about a rather specific topic, a specific formal theory. It is not about set theory in general. It is not about formal theories in general. Your "average educated person" would have better luck starting with more general articles. --Trovatore (talk) 03:28, 25 January 2018 (UTC)

Unspecifik Link 2014 Reference

The reference in section virtual classes, Formalism and Beyond: On the Nature of Mathematical Discourse (Logos) Digital original Edition by Godehard Link (Editor), is extemly broad. Since it is a collection of essays: "The essays collected in this volume focus on the role of formalist aspects in mathematical theorizing and practice, examining issues such as infinity, finiteness, and proof procedures, as well as central historical figures in the field, including Frege, Russell, Hilbert and Wittgenstein. Using modern logico-philosophical tools and systematic conceptual and logical analyses, the volume provides a thorough, up-to-date account of the subject." Maybe the reference could say which essay? Jan Burse (talk) 02:41, 3 March 2019 (UTC)

Sets don't seem to exist

Did this specific axiomatization come from somewhere in particular? Because, as far as I can tell, it doesn't prove that there exist any sets at all. Every axiom assumes at least one set. Luke Maurer (talk) 02:15, 10 March 2019 (UTC)

(If the Axiom of Infinity is supposed to be what bootstraps everything, then (a) the prose should be written so that it doesn't seem to presume that a set w exists and (b) the formal notation shouldn't presume that the empty set already exists.) Luke Maurer (talk) 02:19, 10 March 2019 (UTC)

@Luke Maurer: The axioms listed in this article are taken from Kunen's "Set Theory: An Introduction to Independence Proofs", see Zermelo–Fraenkel set theory#Axioms. The second paragraph of that section talks about the existence of at least one set.

IMHO, the usage of Kunen's axioms (especially when this is combined with the omission of the axiom of empty set) is somewhat idiosyncratic. However, see Talk:Zermelo–Fraenkel set theory/Archive 1#Why no mention of the axiom of the empty set? from 2007 and Talk:Zermelo–Fraenkel set theory/Archive 1#Rephrasing "The Axioms" intro, and Axiom of Infinity from 2008. – Tea2min (talk) 07:17, 10 March 2019 (UTC)

This all seems worth spelling out, or at least nodding to, in the text about the axiom. I see there was a proposal to add some nice explanatory text about how $\varnothing \in X$ can be seen as shorthand:

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "http://localhost:6011/en.wikipedia.org/v1/":): {\displaystyle \forall y (\forall u (u \notin y) \Rightarrow y \in X) \,} .

I don't see any objection to it in the thread; is there a problem? (Speaking for myself, it's still unsatisfying because it really says “if there's an empty set, it's in $X$,” when what we want is “there's an empty set and it's in $X$.”) — Preceding unsigned comment added by Luke Maurer (talk • contribs) 02:55, 1 April 2019 (UTC)

If X is the set whose existence is guaranteed by the axiom of infinity, then we can apply the axiom of separation to X to get the existence of the empty set. Then one can infer that X does contain that empty set. So you get what you wanted indirectly. JRSpriggs (talk) 03:08, 1 April 2019 (UTC)

You have to remember that first-order logic guarantees that something exists. That together with separation is enough to guarantee the existence of the empty set. --Trovatore (talk) 03:36, 1 April 2019 (UTC)

History section contradicts other pages

The articles for Dimitry Mirimanoff, the axiom of regularity, and John Von Neumann all assert that Von Neumann proposed the axiom of regularity not Mirimanoff, but the history section of this page says Mirimanoff proposed the axiom of regularity. Furthermore, Zermelo set theory includes the axiom of choice, so adding replacement and regularity should yield ZFC not ZF.

WingsOfEpsilon (talk) 17:14, 8 May 2019 (UTC)

Please feel free to change the History section, if you have references to reliable sources to back you up. Notice that Wikipedia is not a reliable source. JRSpriggs (talk) 02:35, 9 May 2019 (UTC)

Wrong reference?

"the cumulative hierarchy of sets introduced by John von Neumann.[8]" But [8] refers to Shoenfield's text. Should it not refer to a paper of von Neumann? (Unfortunately I am unable to say which paper.) 31.49.9.229 (talk) 00:27, 30 December 2019 (UTC)

This is just speculation, but if John Von Neumann's paper is not a suitable reference for some reason (in German rather than English, expression is too archaic to be understandable to most modern students, out of print, makes no claim of originality for John, is an unpublished letter or lecture, or whatever), then a suitable reference by Shoenfield attributing the idea to John would be preferable. JRSpriggs (talk) 08:42, 30 December 2019 (UTC)

Provable that V satisfies the axiom of choice?

I edited Zermelo–Fraenkel set theory#Motivation via the cumulative hierarchy to change "It is provable that a set is in V if and only if the set is pure and well-founded; and provable that V satisfies all the axioms of ZFC, if the class of ordinals has appropriate reflection properties." to say "... provable that V satisfies all the axioms of ZF, ..." with the edit summary "V might not satisfy AxCh; so ZF rather than ZFC.". @Trovatore: reverted me with the edit summary "hmm? Choice is a standard assumption".

Sure, choice is a standard assumption, but is it provable that V must satisfy it? Provable from what assumptions? Presumably we are not just assuming ZFC itself, since that would beg the question. Presumably we should use some weaker theory and the definition of V. Otherwise, there is no point to having this sentence at all. And no point to saying "... if the class of ordinals has appropriate reflection properties." which is intended to justify Fraenkel's addition of the Replacement schema. Many people work within theories which do not satisfy choice and I doubt that they would say that the well founded pure sets (i.e. V) in their models must always satisfy the axiom of choice. JRSpriggs (talk) 21:02, 22 September 2022 (UTC)

The context is the von Neumann hierarchy as a motivation for Zermelo–Fraenkel set theory (which is ambiguous as to whether it means ZF or ZFC). But in the context of it as an intuitive motivation, it's as strong a motivation for choice as it is for any of the other axioms. If you take the full powerset at every stage, of course you include the choice sets. --Trovatore (talk) 22:12, 22 September 2022 (UTC)

"... of course you include the choice sets." This begs the question because you are assuming that the full powerset has choice sets in it.

See Axiom of choice#Stronger forms of the negation of AC. If there are models for any of the following, then their V contains sets whose powersets lack choice functions:

• every set of reals has the Baire property
• the axiom of determinacy
• the existence of an amorphous set [amorphous sets may require urelements, therefor not in V]
• the continuum is a countable union of countable sets
• all limit ordinals have cofinality ω

OK? JRSpriggs (talk) 08:13, 23 September 2022 (UTC)

Yes, but their V is not the real V, and while those models are genuine models, they satisfy statements that are not true.

Remember, this is a motivation, not a proof. If you accept the motivation, intuitively, you cannot reject choice. --Trovatore (talk) 15:41, 23 September 2022 (UTC)

But if I accepted your position that we should ignore the word "provable" and just base this on our intuition about V, then I would change it the other direction from "ZFC" to "ZFC+V=L". On what ground would you reject the axiom of constructibility? JRSpriggs (talk) 19:50, 24 September 2022 (UTC)

Unlike AC, there's no good intuitive reason in the first place to think V=L should be true. It's almost the opposite concept (in spite of the fact that V=L actually implies AC over ZF). The point is that you take the full powerset at every stage, all the possible ways of including some objects and omitting others, completely arbitrarily and not requiring any rule whatsoever for which you include and which you omit. So just look at the first place where it makes a difference, the powerset of the natural numbers. If V=L, then every set of naturals has a very canonical place in a completely well-specified hierarchy. Why in the world should that be true, for completely arbitrary sets of naturals?

Of course, that argument doesn't actually say why V shouldn't equal L, but only casts doubt on why it should. To see why V shouldn't equal L, you need to go to large cardinals. This now becomes a Popperian/Lacatosian argument rather than a self-evidence argument (the argument for AC is one of self-evidence). Large cardinals are falsifiable, and not falsified, and have explanatory power. They fit together coherently. This provides a strong reason to accept them, and therefore necessarily reject V=L. --Trovatore (talk) 05:53, 25 September 2022 (UTC)

But the largest of the large cardinals, Reinhardt cardinals and Berkeley cardinals, are incompatible with the axiom of choice. JRSpriggs (talk) 18:55, 26 September 2022 (UTC)

I think the general expectation is that Reinhardt cardinals are inconsistent even over ZF; the proof just hasn't been found yet. --Trovatore (talk) 20:39, 26 September 2022 (UTC)

Axiom system more attuned to the cumulative hierarchy V

In line with the program of reverse mathematics, I want to derive ZF from a weaker set theory together with a definition of V. I thought of using Kripke–Platek set theory, but even that may have too much. Henri Poincaré criticized the axiom of union as being impredicative. And the axiom of collection (replacement) maybe too strong. Anyway, here is my current thinking:

• Axiom of extensionality: Two sets are the same if and only if they have the same elements.
• Axiom of empty set: There exists a set with no members, called the empty set and denoted {}.
• Axiom of adjunction: Given a set and an element, there is a set whose elements are the elements of the given set together with the given element.
• Axiom of Δ₀-separation: Given any set and any Δ₀ formula φ(x), there is a subset of the original set containing precisely those elements x for which φ(x) holds. (This is an axiom schema.)
• Axiom of infinity
• Axiom of Hartogs number: For every set there is an ordinal which cannot be mapped injectively into it.
• V:
  • For every ordinal α, there is a unique set V_α such that $\forall x(x\in V_{\alpha }\leftrightarrow \exists \beta <\alpha (x\subseteq V_{\beta }))$.
  • For every set s, there is an ordinal α such that s is an element of V_α.

OK? JRSpriggs (talk) 23:16, 5 October 2022 (UTC)

Not the place to discuss it, but what you seem to be asking for is basically impossible. Reasoning about the cumulative hierarchy in a formal theory will never give you more consistency strength than the theory you start with. The cumulative hierarchy as a motivation is a different matter; that's done by informal argument, not in a formal theory. --Trovatore (talk) 00:30, 6 October 2022 (UTC)

This is not as strong as ZF (let alone ZFC), but it is stronger than it would be if one left out the definition of V part. That part allows one to prove the axioms of union, regularity, and powerset. Pairing follows from empty set and adjunction, of course. JRSpriggs (talk) 14:48, 6 October 2022 (UTC)

Add an axiom saying that Ord is Mahlo — for every closed unbounded class of ordinals C (definable by a formula with parameters), there is a regular ordinal in C. JRSpriggs (talk) 21:57, 8 October 2022 (UTC)

Beginning with any ordinal α form a sequence as follows: take V_α, take the Hartogs number of that set, take the next regular ordinal after that, then repeat. The limits of this sequence will be a closed unbounded class of ordinals, so there will be a regular ordinal Κ among them (perhaps we could call this a semi-strong inaccessible cardinal). Then using Δ₀-separation we can prove that the axioms of separation and replacement hold in V_Κ as well as the other axioms mentioned above (except Mahlo). The only difficulty is showing that the image set provided by the axiom of replacement is bounded in V_Κ. If it were unbounded, then by the regularity of Κ the ranks of its elements would have to form a set with order type Κ. This could then be mapped injectively backwards through the function to subsets of the domain of the function which lie in V_α+1 and that contradicts the fact that Κ is larger than the Hartogs number of that set by the construction of Κ. So we have a model of ZF without choice. JRSpriggs (talk) 13:57, 9 October 2022 (UTC)

AC formulation

In this diff, Caleb Stanford replaced the longstanding version of AC ("every set can be wellordered") with a version that I agree sounds more like what you'd call the "axiom of choice". I'm going to presume Caleb did this correctly, though I haven't checked.

The background here is that the axioms as presented are taken from Kunen's book. It's a bit idiosyncratic to use "every set can be wellordered" as a ZFC axiom, and probably even more idiosyncratic to call this statement (as Kunen in fact does) the "axiom of choice".

But at some point CBM went through and carefully checked character-by-character that Kunen's axioms had been faithfully transcribed. The idea is that all the axioms should come from a single source. Different but intuitively equivalent formulations of axioms can cease being equivalent when other axioms are dropped or changed, so it's worth being a bit careful with this.

Kunen's formulation strikes me as a good one to use, with the sole slightly sour note being this idiosyncrasy about AC. If we're troubled enough by it, we could switch to Jech's, but someone should go through and make sure it's done right, for all the axioms rather than just one. (I think maybe Jech uses Collection instead of Replacement? I don't like that and don't think it's very standard, so it's not a clear win in any case.) --Trovatore (talk) 17:49, 4 September 2023 (UTC)

Hi Trovatore, thank you for the context on the page history! It makes sense to use well-ordering as in Kunen's book, but in this case, the introduction needs some work to be consistent with the article -- and we also need explain somewhere to beginners that ZFC = ZF + C can refer equivalently to the well-ordering theorem. Potential downsides are that it's a bit nonstandard, and makes it harder to find the section which discusses Choice.

The other thing I'd like to point out is that the form of the axiom -- which uses the shorthand "R well-orders X" is not consistent with the rest of the article. That should also be addressed, I haven't referenced Kunen's book to compare. But I am surprised that there's not a formal statement in Kunen's book.

Thanks, Caleb Stanford (talk) 20:55, 4 September 2023 (UTC)

Hmm, I hadn't really noticed this before. The axioms are all collected together in §7 of the introduction, and I don't think he's defined at that point what it means for a relation to well-order a set. He drills down into individual axioms in Chapter I, with Choice being treated in Chapt. I §6, with "R well-orders X" being defined on p. 14 (this is the 1980 edition; don't know if there's a later one). I'm not sure what you mean by "not consistent with the rest of the article" — it surely doesn't contradict the rest of the article, or if it does the rest of the article should be changed, as this is completely standard usage. --Trovatore (talk) 22:39, 4 September 2023 (UTC)

I meant that "9. Well-ordering axiom" is the first occurence in the article of "well-ordering", whereas the article refers to "Choice" several times earlier in the article. C.f. introduction:

Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded."

For a reader not familiar with set theory, reading this sentence, it would be impossible to locate in the list of axioms which one corresponds to C.

Note that Kunen -- unlike the article -- still refers to the well-ordering theorem as Choice, which matches better with the ZF/ZFC distinction for an introductory text. Caleb Stanford (talk) 22:57, 4 September 2023 (UTC)

Oh, got it. That's actually a really good point. Right, if we're following Kunen, we should call this Choice. Some editors (understandably) find this jarring — if it's too painful to call it Choice, we should probably switch to a different source. --Trovatore (talk) 18:04, 5 September 2023 (UTC)

For a specific non-empty set X, if there is a choice function for the (powerset of X)\{ {} }, then there is a well ordering R of X. And vice-versa. So it is not such a far stretch to call this the axiom of choice. JRSpriggs (talk) 00:07, 6 September 2023 (UTC)

Since there seems to be a rough consensus, I've taken an additional cut to lightly edit based on this discussion. Feel free to edit further. Best, Caleb Stanford (talk) 03:04, 6 September 2023 (UTC)

To use an example from reverse mathematics, the Bolzano-Weierstrass theorem is equivalent to the axiom of arithmetical comprehension over RCA₀, but articles containing definitions of ACA₀ do not define ACA₀ as RCA₀ plus the Bolzano-Weierstrass theorem. C7XWiki (talk) 03:43, 10 February 2024 (UTC)

Add parentheses in ¬A=B for clarity?

In the "formal language" section, in the first table, ¬A=B is used on rows 1 and 4. That's how "=" is used in https://forallx.openlogicproject.org/html/ (page 231, chapter 26 "Identity") and row one basically defines "A≠A" as ¬A=B so it's clear enough I suppose. But I'd say typically you see negation "taking precedence over" relation symbols and so ¬A=B would not be equivalent to ¬(A=B). I think ¬(A=B) is more readable but there's technically nothing wrong with how it is now. I propose changing the aforementioned table like so:

Set-builder statement	Formal language
$A\neq B$	$\lnot \ ($A $=$ B$)$
$A\notin B$	$\lnot \$A $\in$ B
$A\subseteq B$	$\langle x\rangle (x\in$ A $\Rightarrow x\in$ B$)$
$A\subset B$	$\langle x\rangle (x\in$ A $\Rightarrow x\in$ B$)\land \lnot \ ($A $=$ B$)$
$\forall x\in A,\ x\in B$	$\langle x\rangle (x\in$ A $\Rightarrow x\in$ B$)$
$\exists x\in A,\ x\in B$	$\langle \exists x\rangle (x\in$ A $\land \ x\in$ B$)$

Does anyone else agree with this or am I tripping? 88.193.176.69 (talk) 12:56, 14 August 2024 (UTC)

Since ¬ is applied to formulas whereas relation symbols (or =, which in many formulations is not technically a relation symbol but rather part of the logic) apply to terms, there is ordinarily no confusion. If you had a unary ¬ that was also a function symbol, admittedly that would be a problem and you'd need to disambiguate.

Other notes:

• Using the bare variable instead of the ∀ is rare these days. I think maybe Russell and Whitehead used that? In general their notation did not catch on.
• Out of curiosity, why didn't you also suggest parentheses in the formula $\lnot A\in B$?

--Trovatore (talk) 16:47, 15 August 2024 (UTC)

Looking more closely, the entire "Formal language" section is uncited, though some of it is probably sourceable to the general refs. But at least the last third of it is problematic.

• The notation is idiosyncratic (angle brackets around quantifiers; the missing ∀; use of commas after quantifiers).
• The use of the term "set-builder notation" for a just slightly higher level on top of the bare formal language seems to come out of nowhere. That isn't what "set-builder notation" means at all, at least not standardly.
• The second table identifies terms in the language of set theory (incorrectly called "set builder notation") with existential assertions, which is just wrong
• The abbreviation "wff" is also idiosyncratic. Some people do use it, but not usually in a very formal context.

I'm tempted to just remove the whole section, or at least the bit starting from where it starts talking about "set-builder notation". It's true that something ought to be said about the formal language. But this is not that something. --Trovatore (talk) 22:40, 15 August 2024 (UTC)

I agree that the bare-variable representation of the ∀ quantifier is rare these days and except for special situations is probably best avoided in these pages. Interestingly, I was just reviewing Robert Rogers' (1971) Mathematical Logic and Formalized Theories and realizing that he adopts a form of this notation throughout his text, using a parenthetical (x) to indicate ∀x. I hadn't seen that before. Craftwd (talk) 19:10, 10 December 2024 (UTC)

Garbled phrasing in section on axiom schema of specification?

In the Axioms section, under the sub-section for Axiom Schema of Specification, there seems to be some garbled phrasing in the paragraph beginning "This restriction is necessary to avoid Russell's paradox ...." The garbled portion appears in the very long parenthetical in that paragraph:

"... we need to previously restrict the sets y will regard within a set z that leaves y outside so y can't refer to itself ..."

I think the basic idea is that the elements of the to-be constructed set y must come from some already-defined set z, right? Somewhere along the line the phrasing seems to have gotten garbled, but perhaps I'm missing something or mis-reading here. Craftwd (talk) 18:26, 10 December 2024 (UTC)