![]() | This ![]() It is of interest to the following WikiProjects: | ||||||||||
|
The term "mapping" should be defined here, since it is kind of central to the whole affair. In fact, it's not clear to me what it is.
I don't think we can define the image of A under F as F(A), since F(A) already has a meaning, F applied to the argument A, and that may very well be different from the image A under F.
AxelBoldt 00:42 Jan 6, 2003 (UTC)
I still have a problem: the logical concept you describe in mapping is what I would call a function symbol in a logical theory: something that turns into a function when interpreted in a model. But the formal language of ZF doesn't contain any function symbols (only the predicate symbols = and ∈). I thought that a mapping in the sense of the replacement axiom is a special well-formed-formula (with two free variables) in the formal language of ZF. I was just concerned about the precise meaning of the word "special" in the last sentence. This link http://plato.stanford.edu/entries/set-theory/ZF.html seems to agree, although they don't use the term "mapping" at all but put the requirement into the axiom itself. AxelBoldt 17:45 Jan 8, 2003 (UTC)
The predicates = and ∈ are the only primitive predicate symbols in ZF, but there are other derived predicate symbols; the Stanford link's version of replacement thus refers to an arbitrary predicate symbol φ. Similarly, there are derived function symbols (same thing as "mapping", a term that I used here primarily since it was already used in the text on Axiomatic set theory). As explained on Mapping, one can think of a function symbol as a certain kind of predicate symbol, subject to a certain axiom, which is what the Stanford link does explicitly; our article is more generous about how you want to think about things.
Ironically, the Stanford link does introduce a derived function symbol (a nullary one, that is a constant symbol): ∅, which is used in the axiom of infinity. As with any derived function symbol, one needs to prove (in a result) or assume (in a hypothesis) a statment about it, which is the statement about uniqueness that appears on both the Stanford page and on Mapping. The Stanford page doesn't formally prove this statement before using ∅, which should be done, but they do indicate how to prove it using the axioms of extension and null set in the text after the axiom of null set -- so that's all good. Thus in the axiom schema of replacement, one must assume this of F -- which the Stanford page does explicitly, and which we do implicitly by referencing Mapping.
I do think that Wikipedia needs more discussion about derived symbols and the many ways to think about them. I really don't know enough at this point to write that. I'm trying to be as general as possible when writing text like that appearing in this article -- thus I just say "mapping" without insisting that this term be interpreted in any particular way, while explaining as much as I can about possible interpretations on Mapping -- but I'll probably be imperfect, at least until I read more logic literature. The only thing that I'm sure of is that most logic literature (including presentations of ZFC), whatever its point of view, will insist on that POV being followed without exception -- which is reasonable in a document that's intended to be both formally rigorous and self contained. But that insistence is just what I'd like to avoid on Wikipedia. If you say that a mapping is just a predicate written in longhand in terms of = and ∈ that satisfies a certain uniqueness postulate, then that's fine; if I say that it's a new symbol that should be explicitly introduced subsequent to proving a certain uniqueness theorem (possibly in a box), then that's fine too. The possibilities should be explained on Mapping -- and I agree that the discussion there is so far incomplete -- but Wikipedia shouldn't insist on any of them.
-- Toby 18:57 Jan 9, 2003 (UTC)
I'm cool with derived symbols and even derived function symbols.
Yes. But I have a problem with using the latter notion of mapping in the context of the replacement axiom schema. I'm concerned that, while in the middle of specifying an infinite list of axioms, we refer to "proving a certain uniqueness theorem" (using those very axioms? or which axioms?) Typically, the proving starts only after you have clarified what your axioms are.
I think (hope) we agree that every axiom can be written as a string in the language of ZF, and this language does not contain symbols such as ∅ or ∉ or ∃!; these derived symbols are just abbreviations that can always be parsed away mechanically. Essentially then, when writing down an axiom schema, we need to specify unambiguously which strings in the language of ZF qualify as axioms. This needs to be done "mechanically", i.e. it should be possible to write a program which lists the axioms one by one (it's a general requirement that axiom sets are recursively enumerable -- otherwise Gödel's incompleteness theorems don't even apply). Right now, our article does not appear to do that, but the Stanford version does.
Maybe we should get rid of the term "mapping" here altogether, since it has too many meanings.
A couple more links that follow the Stanford approach:
AxelBoldt 00:36 Jan 10, 2003 (UTC)
I don't think this line:
Note that there is one axiom for every such mapping F
is correct. The way I've always seen it is to have one instance of the axiom for each proposition-in-two-variables, and extend each instance to include the requirement that its proposition is a mapping.
After all, whether a given proposition-in-two-variables is a mapping or not depends on the theory we're describing, so we can't really assume we know the answer when defining the axioms. Matthew Woodcraft
That is exactly the point I'm trying to make. Toby, you say that you get precisely the same recursively enumerable set of axioms as Stanford, but at the same time that you are trying to be more general. I don't understand that at all. The same set of strings is the same set of strings. And I don't understand how your mechanical procedure which lists all axioms would work. Like Matthew says above: how would the procedure know what the mappings are that it can use?
I agree with your statement that axiom systems are used both to prove statements from them and also statements about them, but that doesn't mean that you can change the axiom system depending on what purpose you currently have in mind. You have to have one clean recursively enumerable set of axioms, and with that you can the play the two quite different games.
When I suggested to drop "mapping" altogether, you say we must use some term. In fact we don't. Stanford's axiom schema implicitely defines mappings; we don't need a word for them. We only need to be able to refer to formulas with two free variables.
One other point: if we use the Stanford version of the axiom schema, and then you start proving theorems in your set theory and one day you manage to prove that a certain formula F is indeed a mapping, then you are allowed to use the replacement schema in your sense with this very F; that's what Stanford's axiom scheme (with modus ponens) allows you to do. AxelBoldt 05:46 Jan 24, 2003 (UTC)
Yes, I am still concerned that we give a very unorthodox and close to unintelligible form of the axiom here. The functional predicate article gives various meanings for the term; it's not good style to link to that article and let the reader guess which meaning is intended. After reading through that article, the only clear sense that I can assign to the axiom schema is the one given in the last line of that article, the one I have campaigned for all along.
Have you seen a single ZFC formalization with fundamental function symbols? I don't think these exist, and I'm not trying to push anything on the reader. Why would you use fundamental function symbols in your language; why make it more complicated than necessary? What would be the intended interpretation of these symbols?
The orthodox ZFC formalizations I know are first order theories with one or two fundamental predicates (∈ and =) and without fundamental function symbols. As in any first order theory, functional symbols may be introduced as mere abbreviations after having proved a uniqueness theorem. The reader may come away with the impression that that's the notion of "functional predicate" we are referring to in the replacement axiom schema; we are not. The reason: we haven't cleanly specified what "proving a uniqueness theorem" means. What axioms can be used in the proof? Are you allowed to use the axiom schema of replacement, or is that not yet in place? We simply haven't specified the axiom schema in an explicit enough fashion (meaning in a fashion that would allow me to write a program which lists all members of the schema one-by-one -- a requirement of all axiomatizations).
Why do you think this could be an issue of "CS-oriented logicians" versus "traditional logicians"? Which of the above cited sources do you consider "CS-oriented"? If you really think there are fundamentally different ways of formalizing ZFC (which I don't), then NPOV requires that you make this distinction explicit, clearly explain the "traditional way" and who uses it, and the "CS way" and who uses it. Right now, you somehow try to gloss over the difference by trying to craft one version of the axiom schema that could please both (but doesn't -- see the other complaints on this page) and then pointing to the functional predicate article which allows many interpretations. I think we should strive for a higher standard of clarity, especially when dealing with an axiom system on which all of mathematics is built.
Toby, I would really like you to go to the set theory shelf of the library, take a random sample of three books on ZFC, and look at the replacement axiom schema. AxelBoldt 17:14 Apr 26, 2003 (UTC)
I think this page is unreadable. Surely if the A of R is an axiom or schema, it can be put more simply. It isn't accessible at all. No offence, but it reads like it was written by a group who know it so well that they can't even see the fog that washes the page.
Centroyd
Occasionally the axiom is quoted without the uniqueness requirement. In other words, allowing any predicate, instead of only functional predicates.
To me this means just take the statement at the top of the page and drop the exclamation mark, i.e.:
which can't be right. I think we want something like
right? Also:
Given a predicate P, define a functional predicate F by F(x) = { y is of rank α | P(x,y)}. Using replacement, one defines FX], the union of which satisfies the requirements of boundedness.
Can't there be two elements in x with the same rank? How would F be functional then? -Dan 21:40, 30 April 2006 (UTC)
Also also:
and thus the two axioms are equivalent (In Z)
The article on Z excludes foundation. Can this equivalence be proven without it?
Anyway, I've fixed up the statement section a bit. I dropped the proof out. -Dan 15:48, 1 May 2006 (UTC)
How can the axiom of boundedness be equivalent to the axiom of replacement? Take the relation x R y to mean 0=0 (ie always true), then the mapping under R of {x} is U, the universal class, certainly not a set. —Preceding unsigned comment added by 81.210.250.222 ( talk) 08:11, 30 March 2008 (UTC)
A function is a relation. A relation is a subset of cartesian product. A cartesian product is a set of ordered pairs. An ordered pair is a set. But a set is something that satisfies axioms that is defined by a function. lol, wat are u talking about? A is a B , B is a A.
The axiom schema of replacement and the axiom of empty set are equivalent to the axiom schema of collection and the axiom schema of separation. This is not yet fully explained in the article. JRSpriggs ( talk) 04:36, 4 April 2008 (UTC)
From Alan U. Kennington (
talk). 2009-3-21:
It is not at all clear to me how to prove that the axiom of collection follows from the axiom of replacement without using the axiom of choice. Can someone definitely confirm that this implication follows without the axiom of choice? To use the axiom of replacement, you need a function. It is not clear how to construct such a function from a general relation without the axiom of choice. I have consulted books by Shoenfield and Mendelson to try to answer this, and Google too. No luck yet. —Preceding
undated comment added 13:42, 20 March 2009 (UTC).
Carl, many thanks indeed for that. But as far as I can see, you have provided an outline of the proof that the axiom of replacement implies the axiom of specification, not the axiom of collection. I wanted to prove the axiom which states that if R is a predicate of two variables and X is a set, then . Or in low-level logic notation, . Yes, I understand that we are not talking about functions in the sense of a set of ordered pairs here. Functions here are simply predicates with two variables which have a unique second argument for any given first argument. -- Alan U. Kennington ( talk) 04:11, 21 March 2009 (UTC)
Here is how I see the problem of proving the axiom of collection using the axiom of replacement. Let Zx denote the class of z which satisfy R(x,z). This may not be a set. So we can't use the axiom of unions to just take the union of Zx over all x in X. (This would be the range of R.) In the worst case, the classes Zx would be disjoint. So now to get the "cardinality" of the range of R down to the same as that of X, we need to choose a single z in each class Zx and take the union of those to form a set Y which has the same "cardinality" as X so that the axiom of replacement can be applied. I.e. we really need a one-to-one association between X and its images under the relation R in order to apply the axiom of replacement. However, if you do have a general means of choosing a single element out of each of an arbitrary collection of collections, what you have there is the axiom of choice. In other words, it seems to me that the axiom of collection implies the axiom of choice, almost. It's not quite that at this stage of my outline of a proof because the axiom of collection only reduces each of the classes R({x}) to a set, not necessarily to a singleton. But it is clearly a choice-like assertion. It is stating that out of any set of classes, you can choose a set from each of the classes. I just don't see how to get this from the ZF axioms. -- Alan U. Kennington ( talk) 05:56, 21 March 2009 (UTC)
Carl, thanks once again for this. The question is so fundamental, I'm sure someone has either proved the necessity or the non-necessity of AC for proving collection from replacement. My original source for this issue was the Japanese Mathematical Society Encyclopedic Dictionary of Mathematics, second edition, section 33.B, which states that the axiom of collection is actually part of ZF. If this is so, then there is more than one version of ZF out there, assuming that the axiom of collection requires AC. Unfortunately, very many texts bundle AC together with ZF to make ZFC anyway, on the assumption that almost all mathematicians are happy with AC. I personally am crusading against the axiom of choice, in my own small way. So I really need to know if the axiom of collection version of ZF is "tainted" by AC. Since ZF is the basis of most mathematics, it's really important to know if there are two non-equivalent versions of ZF out there! -- Alan U. Kennington ( talk) 14:57, 21 March 2009 (UTC)
Many thanks for that outline of a proof. However, I'm having difficulties accepting it. To take an extreme example, suppose φ is true for all values of its arguments. Let n equal zero for simplicity. I assume you're taking the infimum over all y which satisfy φ(x,y) for fixed x. So now rank(y) is the smallest ordinal number which is greater than the rank of any member of y. In a book by Shoenfield, this transfinite induction is performed within ZFC. In a book my Mendelson, the induction is performed in the chapter on the axiom of choice. So this makes me a little suspicious. But these rank values are clearly unbounded since y ranges over all sets. So now we come to the definition of the infimum. I thought that the infimum of the class of ordinals was undefined, since an infimum must be a member of the set (or class) within which one calculates the infimum. So it seems that the infimum is undefined for all x in X. My hunch is that you may have assumed that for any fixed x the class of y for which φ(x,y) is true is not a proper class. If that is so, then the most difficult obstacle is already overcome. Also, I'm not sure what Vr is defined to be. -- Alan U. Kennington ( talk) 02:31, 22 March 2009 (UTC)
I guess the most important step in that proof is the assertion that the cumulative hierarchy is the same as the class of all sets in ZF. But is that assuming the axiom of collection? If it is only assuming the axiom of replacement, the issue seems to be settled. But if the version of ZF which is used to show that the sets Vα exhaust all sets includes the axiom of collection, the proof would seem to be circular! -- Alan U. Kennington ( talk) 18:58, 23 March 2009 (UTC)
Okay, in that case it seems to me that some of these ideas should appear in the articles on the subject. In the section: Relation to the axiom schema of specification, it would be good to have some statements about what the situation is relative to ZF, in addition to the ZFC discussion. In fact, I think the entire page should reference ZF rather than ZFC. The vast majority of material on that page requires only ZF. A false impression might be gained from the constant reference to ZFC that AC is required for all or most of the assertions on that page.
Specifically in the "Relation to the axiom schema of specification" section, or perhaps even better in the "Axiom schema of collection" section, I think there should be an outline of the proof that the collection axiom follows from the replacement axiom over the other ZF axioms, with links to the pages on Von Neumann universe and Cumulative hierarchy, and possibly also Regularity and cumulative hierarchy and Transfinite recursion. Apart from the Example applications section, I don't see anything that requires AC on that page.
On the subject of proving that every set has a rank, and that the von Neumann tranfinite induction using power sets covers all ZF sets, yes it is true that this is in many standard texts. The problem is only tracing back through all of the supporting theory to ensure that AC and the collection of axiom have not crept in there somehow.
I think that this terminates any doubt (if you think that computers can do math):
Theorem cp: collection principle. Also on the metamath proof explorer site is
the Boundedness Axiom, which bears an uncanny resemblance to the collection axiom!
--
Alan U. Kennington (
talk)
14:43, 24 March 2009 (UTC)
The section Axiom schema of replacement#History and philosophy seems to imply that Zermelo set theory is adequate to prove the existence of each set in Vω·2 (provided that it is a definable subclass of Vω·2). However, I do not see how one could prove that Vω is a set without using replacement. So this section may be misleading in that respect. JRSpriggs ( talk) 05:42, 25 February 2010 (UTC)
"defining formulas" may identify surjective functions that are not bijections. Example: Union is definable and there exists only one for each set. The image of the set including only the empty set and the set that includes only the empty set under the definable union function is the set including only the empty set. Note: This comment may be deleted when the issue is deemed resolved by an expert in the theory of sets. — Preceding unsigned comment added by 85.97.49.95 ( talk) 23:29, 26 October 2012 (UTC)
I hesitate to write more here about that, but Zermelo's notion of definiteness should be covered somewhere in Wikipedia. It was a vague notion and it was the main dispute between him, Skolem and Fraenkel, who ultimately sided with Skolem; that was a leading cause of the breakdown in the good personal/work relationship Fraenkel had with Zermelo. There are dozens of pages about this definiteness issue/dispute in Ebbinghaus' book. Is there a page on Wikipedia where the topic is even mentioned? Skolem simply identified definiteness with first-order definiability, a view that Zermelo never accepted. 86.127.138.67 ( talk) 19:53, 13 April 2015 (UTC)
I think there is an error in the statement of this scheme as presented here; since clearly the symbol B needs to be forbidden from occurring free in phi. Otherwise we'd arrive at the following inconsistency:
Let phi be the formula "x=x ^ not y in B". From axiom of pairing we do have non empty sets. Take any non empty set A, now we have Exist y (x=x ^ not y in B) for some x in A, since we don't have a set of all sets; accordingly we must have the following:
Exist y in B (x=x ^ not y in B) for some x in A, a contradiction!.
Therefore the symbol "B" must be restricted from occurring free in phi.
Notation: "^" refers to 'conjunction'.
Zuhair — Preceding unsigned comment added by 62.201.200.11 ( talk) 13:35, 19 September 2015 (UTC)
To JRSpriggs: Actually I do know what you meant, but that is not enough, the wording must be corrected, because as it stays the statement is abhorrently FALSE. I think you need to add (a part from B not occurring free in φ) after the word "restrictions" and the word "any" to be deleted.
Zuhair — Preceding unsigned comment added by 62.201.200.11 ( talk) 07:42, 21 September 2015 (UTC)
I think the axiom schema of collection, which is often more suited to constructive settings and other settings (see e.g. https://arxiv.org/abs/1110.2430, constructive set theory, and strong collection) should receive its own article. It seems to have quite different properties from replacement when other axioms are changed. Would anyone be interested in helping create and write such an article? To start, I would move the current content under the "Collection" section to such an article, and link to it from this article instead. In general, I think it's best that conceptually distinct axiom schemas receive their own articles (see e.g. axiom of empty set, axiom of adjunction, axiom of regularity vs. epsilon-induction, etc.), since it helps keep things organized and mitigates duplication in other articles (which can just directly link to the article in question instead). 2601:547:501:8F90:B99F:CF8E:E353:38A5 ( talk) 06:03, 9 September 2022 (UTC)
![]() | This ![]() It is of interest to the following WikiProjects: | ||||||||||
|
The term "mapping" should be defined here, since it is kind of central to the whole affair. In fact, it's not clear to me what it is.
I don't think we can define the image of A under F as F(A), since F(A) already has a meaning, F applied to the argument A, and that may very well be different from the image A under F.
AxelBoldt 00:42 Jan 6, 2003 (UTC)
I still have a problem: the logical concept you describe in mapping is what I would call a function symbol in a logical theory: something that turns into a function when interpreted in a model. But the formal language of ZF doesn't contain any function symbols (only the predicate symbols = and ∈). I thought that a mapping in the sense of the replacement axiom is a special well-formed-formula (with two free variables) in the formal language of ZF. I was just concerned about the precise meaning of the word "special" in the last sentence. This link http://plato.stanford.edu/entries/set-theory/ZF.html seems to agree, although they don't use the term "mapping" at all but put the requirement into the axiom itself. AxelBoldt 17:45 Jan 8, 2003 (UTC)
The predicates = and ∈ are the only primitive predicate symbols in ZF, but there are other derived predicate symbols; the Stanford link's version of replacement thus refers to an arbitrary predicate symbol φ. Similarly, there are derived function symbols (same thing as "mapping", a term that I used here primarily since it was already used in the text on Axiomatic set theory). As explained on Mapping, one can think of a function symbol as a certain kind of predicate symbol, subject to a certain axiom, which is what the Stanford link does explicitly; our article is more generous about how you want to think about things.
Ironically, the Stanford link does introduce a derived function symbol (a nullary one, that is a constant symbol): ∅, which is used in the axiom of infinity. As with any derived function symbol, one needs to prove (in a result) or assume (in a hypothesis) a statment about it, which is the statement about uniqueness that appears on both the Stanford page and on Mapping. The Stanford page doesn't formally prove this statement before using ∅, which should be done, but they do indicate how to prove it using the axioms of extension and null set in the text after the axiom of null set -- so that's all good. Thus in the axiom schema of replacement, one must assume this of F -- which the Stanford page does explicitly, and which we do implicitly by referencing Mapping.
I do think that Wikipedia needs more discussion about derived symbols and the many ways to think about them. I really don't know enough at this point to write that. I'm trying to be as general as possible when writing text like that appearing in this article -- thus I just say "mapping" without insisting that this term be interpreted in any particular way, while explaining as much as I can about possible interpretations on Mapping -- but I'll probably be imperfect, at least until I read more logic literature. The only thing that I'm sure of is that most logic literature (including presentations of ZFC), whatever its point of view, will insist on that POV being followed without exception -- which is reasonable in a document that's intended to be both formally rigorous and self contained. But that insistence is just what I'd like to avoid on Wikipedia. If you say that a mapping is just a predicate written in longhand in terms of = and ∈ that satisfies a certain uniqueness postulate, then that's fine; if I say that it's a new symbol that should be explicitly introduced subsequent to proving a certain uniqueness theorem (possibly in a box), then that's fine too. The possibilities should be explained on Mapping -- and I agree that the discussion there is so far incomplete -- but Wikipedia shouldn't insist on any of them.
-- Toby 18:57 Jan 9, 2003 (UTC)
I'm cool with derived symbols and even derived function symbols.
Yes. But I have a problem with using the latter notion of mapping in the context of the replacement axiom schema. I'm concerned that, while in the middle of specifying an infinite list of axioms, we refer to "proving a certain uniqueness theorem" (using those very axioms? or which axioms?) Typically, the proving starts only after you have clarified what your axioms are.
I think (hope) we agree that every axiom can be written as a string in the language of ZF, and this language does not contain symbols such as ∅ or ∉ or ∃!; these derived symbols are just abbreviations that can always be parsed away mechanically. Essentially then, when writing down an axiom schema, we need to specify unambiguously which strings in the language of ZF qualify as axioms. This needs to be done "mechanically", i.e. it should be possible to write a program which lists the axioms one by one (it's a general requirement that axiom sets are recursively enumerable -- otherwise Gödel's incompleteness theorems don't even apply). Right now, our article does not appear to do that, but the Stanford version does.
Maybe we should get rid of the term "mapping" here altogether, since it has too many meanings.
A couple more links that follow the Stanford approach:
AxelBoldt 00:36 Jan 10, 2003 (UTC)
I don't think this line:
Note that there is one axiom for every such mapping F
is correct. The way I've always seen it is to have one instance of the axiom for each proposition-in-two-variables, and extend each instance to include the requirement that its proposition is a mapping.
After all, whether a given proposition-in-two-variables is a mapping or not depends on the theory we're describing, so we can't really assume we know the answer when defining the axioms. Matthew Woodcraft
That is exactly the point I'm trying to make. Toby, you say that you get precisely the same recursively enumerable set of axioms as Stanford, but at the same time that you are trying to be more general. I don't understand that at all. The same set of strings is the same set of strings. And I don't understand how your mechanical procedure which lists all axioms would work. Like Matthew says above: how would the procedure know what the mappings are that it can use?
I agree with your statement that axiom systems are used both to prove statements from them and also statements about them, but that doesn't mean that you can change the axiom system depending on what purpose you currently have in mind. You have to have one clean recursively enumerable set of axioms, and with that you can the play the two quite different games.
When I suggested to drop "mapping" altogether, you say we must use some term. In fact we don't. Stanford's axiom schema implicitely defines mappings; we don't need a word for them. We only need to be able to refer to formulas with two free variables.
One other point: if we use the Stanford version of the axiom schema, and then you start proving theorems in your set theory and one day you manage to prove that a certain formula F is indeed a mapping, then you are allowed to use the replacement schema in your sense with this very F; that's what Stanford's axiom scheme (with modus ponens) allows you to do. AxelBoldt 05:46 Jan 24, 2003 (UTC)
Yes, I am still concerned that we give a very unorthodox and close to unintelligible form of the axiom here. The functional predicate article gives various meanings for the term; it's not good style to link to that article and let the reader guess which meaning is intended. After reading through that article, the only clear sense that I can assign to the axiom schema is the one given in the last line of that article, the one I have campaigned for all along.
Have you seen a single ZFC formalization with fundamental function symbols? I don't think these exist, and I'm not trying to push anything on the reader. Why would you use fundamental function symbols in your language; why make it more complicated than necessary? What would be the intended interpretation of these symbols?
The orthodox ZFC formalizations I know are first order theories with one or two fundamental predicates (∈ and =) and without fundamental function symbols. As in any first order theory, functional symbols may be introduced as mere abbreviations after having proved a uniqueness theorem. The reader may come away with the impression that that's the notion of "functional predicate" we are referring to in the replacement axiom schema; we are not. The reason: we haven't cleanly specified what "proving a uniqueness theorem" means. What axioms can be used in the proof? Are you allowed to use the axiom schema of replacement, or is that not yet in place? We simply haven't specified the axiom schema in an explicit enough fashion (meaning in a fashion that would allow me to write a program which lists all members of the schema one-by-one -- a requirement of all axiomatizations).
Why do you think this could be an issue of "CS-oriented logicians" versus "traditional logicians"? Which of the above cited sources do you consider "CS-oriented"? If you really think there are fundamentally different ways of formalizing ZFC (which I don't), then NPOV requires that you make this distinction explicit, clearly explain the "traditional way" and who uses it, and the "CS way" and who uses it. Right now, you somehow try to gloss over the difference by trying to craft one version of the axiom schema that could please both (but doesn't -- see the other complaints on this page) and then pointing to the functional predicate article which allows many interpretations. I think we should strive for a higher standard of clarity, especially when dealing with an axiom system on which all of mathematics is built.
Toby, I would really like you to go to the set theory shelf of the library, take a random sample of three books on ZFC, and look at the replacement axiom schema. AxelBoldt 17:14 Apr 26, 2003 (UTC)
I think this page is unreadable. Surely if the A of R is an axiom or schema, it can be put more simply. It isn't accessible at all. No offence, but it reads like it was written by a group who know it so well that they can't even see the fog that washes the page.
Centroyd
Occasionally the axiom is quoted without the uniqueness requirement. In other words, allowing any predicate, instead of only functional predicates.
To me this means just take the statement at the top of the page and drop the exclamation mark, i.e.:
which can't be right. I think we want something like
right? Also:
Given a predicate P, define a functional predicate F by F(x) = { y is of rank α | P(x,y)}. Using replacement, one defines FX], the union of which satisfies the requirements of boundedness.
Can't there be two elements in x with the same rank? How would F be functional then? -Dan 21:40, 30 April 2006 (UTC)
Also also:
and thus the two axioms are equivalent (In Z)
The article on Z excludes foundation. Can this equivalence be proven without it?
Anyway, I've fixed up the statement section a bit. I dropped the proof out. -Dan 15:48, 1 May 2006 (UTC)
How can the axiom of boundedness be equivalent to the axiom of replacement? Take the relation x R y to mean 0=0 (ie always true), then the mapping under R of {x} is U, the universal class, certainly not a set. —Preceding unsigned comment added by 81.210.250.222 ( talk) 08:11, 30 March 2008 (UTC)
A function is a relation. A relation is a subset of cartesian product. A cartesian product is a set of ordered pairs. An ordered pair is a set. But a set is something that satisfies axioms that is defined by a function. lol, wat are u talking about? A is a B , B is a A.
The axiom schema of replacement and the axiom of empty set are equivalent to the axiom schema of collection and the axiom schema of separation. This is not yet fully explained in the article. JRSpriggs ( talk) 04:36, 4 April 2008 (UTC)
From Alan U. Kennington (
talk). 2009-3-21:
It is not at all clear to me how to prove that the axiom of collection follows from the axiom of replacement without using the axiom of choice. Can someone definitely confirm that this implication follows without the axiom of choice? To use the axiom of replacement, you need a function. It is not clear how to construct such a function from a general relation without the axiom of choice. I have consulted books by Shoenfield and Mendelson to try to answer this, and Google too. No luck yet. —Preceding
undated comment added 13:42, 20 March 2009 (UTC).
Carl, many thanks indeed for that. But as far as I can see, you have provided an outline of the proof that the axiom of replacement implies the axiom of specification, not the axiom of collection. I wanted to prove the axiom which states that if R is a predicate of two variables and X is a set, then . Or in low-level logic notation, . Yes, I understand that we are not talking about functions in the sense of a set of ordered pairs here. Functions here are simply predicates with two variables which have a unique second argument for any given first argument. -- Alan U. Kennington ( talk) 04:11, 21 March 2009 (UTC)
Here is how I see the problem of proving the axiom of collection using the axiom of replacement. Let Zx denote the class of z which satisfy R(x,z). This may not be a set. So we can't use the axiom of unions to just take the union of Zx over all x in X. (This would be the range of R.) In the worst case, the classes Zx would be disjoint. So now to get the "cardinality" of the range of R down to the same as that of X, we need to choose a single z in each class Zx and take the union of those to form a set Y which has the same "cardinality" as X so that the axiom of replacement can be applied. I.e. we really need a one-to-one association between X and its images under the relation R in order to apply the axiom of replacement. However, if you do have a general means of choosing a single element out of each of an arbitrary collection of collections, what you have there is the axiom of choice. In other words, it seems to me that the axiom of collection implies the axiom of choice, almost. It's not quite that at this stage of my outline of a proof because the axiom of collection only reduces each of the classes R({x}) to a set, not necessarily to a singleton. But it is clearly a choice-like assertion. It is stating that out of any set of classes, you can choose a set from each of the classes. I just don't see how to get this from the ZF axioms. -- Alan U. Kennington ( talk) 05:56, 21 March 2009 (UTC)
Carl, thanks once again for this. The question is so fundamental, I'm sure someone has either proved the necessity or the non-necessity of AC for proving collection from replacement. My original source for this issue was the Japanese Mathematical Society Encyclopedic Dictionary of Mathematics, second edition, section 33.B, which states that the axiom of collection is actually part of ZF. If this is so, then there is more than one version of ZF out there, assuming that the axiom of collection requires AC. Unfortunately, very many texts bundle AC together with ZF to make ZFC anyway, on the assumption that almost all mathematicians are happy with AC. I personally am crusading against the axiom of choice, in my own small way. So I really need to know if the axiom of collection version of ZF is "tainted" by AC. Since ZF is the basis of most mathematics, it's really important to know if there are two non-equivalent versions of ZF out there! -- Alan U. Kennington ( talk) 14:57, 21 March 2009 (UTC)
Many thanks for that outline of a proof. However, I'm having difficulties accepting it. To take an extreme example, suppose φ is true for all values of its arguments. Let n equal zero for simplicity. I assume you're taking the infimum over all y which satisfy φ(x,y) for fixed x. So now rank(y) is the smallest ordinal number which is greater than the rank of any member of y. In a book by Shoenfield, this transfinite induction is performed within ZFC. In a book my Mendelson, the induction is performed in the chapter on the axiom of choice. So this makes me a little suspicious. But these rank values are clearly unbounded since y ranges over all sets. So now we come to the definition of the infimum. I thought that the infimum of the class of ordinals was undefined, since an infimum must be a member of the set (or class) within which one calculates the infimum. So it seems that the infimum is undefined for all x in X. My hunch is that you may have assumed that for any fixed x the class of y for which φ(x,y) is true is not a proper class. If that is so, then the most difficult obstacle is already overcome. Also, I'm not sure what Vr is defined to be. -- Alan U. Kennington ( talk) 02:31, 22 March 2009 (UTC)
I guess the most important step in that proof is the assertion that the cumulative hierarchy is the same as the class of all sets in ZF. But is that assuming the axiom of collection? If it is only assuming the axiom of replacement, the issue seems to be settled. But if the version of ZF which is used to show that the sets Vα exhaust all sets includes the axiom of collection, the proof would seem to be circular! -- Alan U. Kennington ( talk) 18:58, 23 March 2009 (UTC)
Okay, in that case it seems to me that some of these ideas should appear in the articles on the subject. In the section: Relation to the axiom schema of specification, it would be good to have some statements about what the situation is relative to ZF, in addition to the ZFC discussion. In fact, I think the entire page should reference ZF rather than ZFC. The vast majority of material on that page requires only ZF. A false impression might be gained from the constant reference to ZFC that AC is required for all or most of the assertions on that page.
Specifically in the "Relation to the axiom schema of specification" section, or perhaps even better in the "Axiom schema of collection" section, I think there should be an outline of the proof that the collection axiom follows from the replacement axiom over the other ZF axioms, with links to the pages on Von Neumann universe and Cumulative hierarchy, and possibly also Regularity and cumulative hierarchy and Transfinite recursion. Apart from the Example applications section, I don't see anything that requires AC on that page.
On the subject of proving that every set has a rank, and that the von Neumann tranfinite induction using power sets covers all ZF sets, yes it is true that this is in many standard texts. The problem is only tracing back through all of the supporting theory to ensure that AC and the collection of axiom have not crept in there somehow.
I think that this terminates any doubt (if you think that computers can do math):
Theorem cp: collection principle. Also on the metamath proof explorer site is
the Boundedness Axiom, which bears an uncanny resemblance to the collection axiom!
--
Alan U. Kennington (
talk)
14:43, 24 March 2009 (UTC)
The section Axiom schema of replacement#History and philosophy seems to imply that Zermelo set theory is adequate to prove the existence of each set in Vω·2 (provided that it is a definable subclass of Vω·2). However, I do not see how one could prove that Vω is a set without using replacement. So this section may be misleading in that respect. JRSpriggs ( talk) 05:42, 25 February 2010 (UTC)
"defining formulas" may identify surjective functions that are not bijections. Example: Union is definable and there exists only one for each set. The image of the set including only the empty set and the set that includes only the empty set under the definable union function is the set including only the empty set. Note: This comment may be deleted when the issue is deemed resolved by an expert in the theory of sets. — Preceding unsigned comment added by 85.97.49.95 ( talk) 23:29, 26 October 2012 (UTC)
I hesitate to write more here about that, but Zermelo's notion of definiteness should be covered somewhere in Wikipedia. It was a vague notion and it was the main dispute between him, Skolem and Fraenkel, who ultimately sided with Skolem; that was a leading cause of the breakdown in the good personal/work relationship Fraenkel had with Zermelo. There are dozens of pages about this definiteness issue/dispute in Ebbinghaus' book. Is there a page on Wikipedia where the topic is even mentioned? Skolem simply identified definiteness with first-order definiability, a view that Zermelo never accepted. 86.127.138.67 ( talk) 19:53, 13 April 2015 (UTC)
I think there is an error in the statement of this scheme as presented here; since clearly the symbol B needs to be forbidden from occurring free in phi. Otherwise we'd arrive at the following inconsistency:
Let phi be the formula "x=x ^ not y in B". From axiom of pairing we do have non empty sets. Take any non empty set A, now we have Exist y (x=x ^ not y in B) for some x in A, since we don't have a set of all sets; accordingly we must have the following:
Exist y in B (x=x ^ not y in B) for some x in A, a contradiction!.
Therefore the symbol "B" must be restricted from occurring free in phi.
Notation: "^" refers to 'conjunction'.
Zuhair — Preceding unsigned comment added by 62.201.200.11 ( talk) 13:35, 19 September 2015 (UTC)
To JRSpriggs: Actually I do know what you meant, but that is not enough, the wording must be corrected, because as it stays the statement is abhorrently FALSE. I think you need to add (a part from B not occurring free in φ) after the word "restrictions" and the word "any" to be deleted.
Zuhair — Preceding unsigned comment added by 62.201.200.11 ( talk) 07:42, 21 September 2015 (UTC)
I think the axiom schema of collection, which is often more suited to constructive settings and other settings (see e.g. https://arxiv.org/abs/1110.2430, constructive set theory, and strong collection) should receive its own article. It seems to have quite different properties from replacement when other axioms are changed. Would anyone be interested in helping create and write such an article? To start, I would move the current content under the "Collection" section to such an article, and link to it from this article instead. In general, I think it's best that conceptually distinct axiom schemas receive their own articles (see e.g. axiom of empty set, axiom of adjunction, axiom of regularity vs. epsilon-induction, etc.), since it helps keep things organized and mitigates duplication in other articles (which can just directly link to the article in question instead). 2601:547:501:8F90:B99F:CF8E:E353:38A5 ( talk) 06:03, 9 September 2022 (UTC)