Talk:Axiom schema of replacement

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 that we should clutter the text with a formal definition, since mappings are central to formal logic in general, which is theoretically a prerequisite for this article. OTOH, an intuitive description could be appropriate, especially since people will probably come to this article without a background in formal logic. What I think is the main problem is that the article Mapping, which people would naturally turn to for further explanation, doesn't have a formal definition, nor much discussion of the concept in formal logic. So I've rewritten Mapping; what do you think of the situation now?

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.

I agree; this is why I used "F'(A)", not "F(A)". (Another notation that I've seen is "F[A]".) Or did I forget the prime somewhere?

AxelBoldt 00:42 Jan 6, 2003 (UTC)

-- Toby 03:34 Jan 8, 2003 (UTC)

Oh, I didn't see the prime, but it's there, sorry. I would prefer F[A], but I guess in this article we don't need any notation for this concept. AxelBoldt 00:42 Jan 6, 2003 (UTC)

I like the brackets better than the prime too; the problem is that I'm not sure if I didn't make it up myself ^_^. -- Toby 18:57 Jan 9, 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.

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, then that's fine too.

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.

That depends. One purpose of axiomatic systems is to prove theorems about them: Gœdel's theorems, relative consistency results, and so on. Another purpose is to provide foundations for mathematics in practice. Both of these are necessary, and indeed interrelate. (Mathematical practice would change a great deal if its foundations were known to be complete or inconsistent -- or less dramatically, if the contiuum hypothesis were known to be provable or unprovable from ZFC.) But these two purposes often lead to different ideas about how formal systems should work. Your last setence above is an example: If you want to prove theorems about a set of axioms, then you need to list them all up front; whereas if you want to formalise the practice of proving theorems using a set of axioms, then you don't want to insist on listing them all first, since that is not in fact always done in the practice in question.

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.

Our article does do that, but I guess that this isn't clear. (It must not be clear, since you don't see it! ^_^) I'm going to try to write some clarification. (You get the same recursively enumerable list as Stanford, of course -- I'm only trying to be more general than Stanford, not completely different.)

Maybe we should get rid of the term "mapping" here altogether, since it has too many meanings.

This is a separate issue; we must use some term. (Ironically, the history of Set theory suggests that you introduced it ^_^ -- but I realise that this isn't trustworthy.) I kind of like having something other than "function symbol", just as we can say "predicate" instead of "relation symbol", but I'm not wedded to it.

A couple more links that follow the Stanford approach:

• Podnieks' also includes those pesky z's.
• University of Queensland is very clean.

Like the Stanford link, the Queensland link also proves a theorem to define a function symbol that it later uses in an axiom: the empty set used in the axiom of infinity. Podnieks' site does infinity in a different way, but ironically, it explains how such proofs-before-axioms can be systematically removed -- necessary for the recursive enumeration that you want. (The explanation is given in commentary after the axiom of empty set -- which is a theorem for Podnieks -- and used in commmentary after the axiom of infinity. But it's not in complete generality.) So I'm not in as bad company as you might think! ^_^

AxelBoldt 00:36 Jan 10, 2003 (UTC)

I have some more comments to make here, but I think that they should go on Mapping (or whatever we choose to call it), since they're very general facts that an encyclopædia covering formal logic should have. But I haven't had any breakfast today, and checking my email as I am now is taking too long. So I'll start editing Mapping (and this article) in about an hour. See you then! -- Toby 21:54 Jan 11, 2003 (UTC)

I was pretty tardy on this; my schedule was thrown off when Wikipedia went down for a bit, and now I'm having trouble getting access to the Net. Hopefully I'll be better at that now! -- Toby 03:34 Jan 27, 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

Yes, you're right -- how many axioms we get will depend on how you formalise predicate logic. I just made many changes to the article, one of which addresses this technical inaccuracy. The point of the statement in the article, of course, is that it is a schema, and that's true regardless. -- Toby 03:34 Jan 27, 2003 (UTC)

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?

When I say that I'm being "more general", I don't mean that I (necessarily) get more axioms; I mean that I get a set of axioms in more different kinds of interpretations of predicate logic as a formal system. If I choose the same formalisation of prediacte logic as Stanford, then I get the same axioms. Now, I didn't explain very well how we know which axioms we get in that case; I've added stuff to Functional predicate (née Mapping) and this article to address that. Following the procedure on Functional predicate to the axiom schema, you can see for yourself that Stanford's axiom schema (or a schema of logically equivalent statements) is the result.

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.

Yes, you certainly can change the system depending on your purpose, as long as you have some metalogical theorems telling you that the systems are equivalent. Similarly, you can choose Roman numerals or Arabic numerals depending on your purpose, since there is an arithmetical theorem telling you that they are equivalent. (See hints of this theorem below.)

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.

Stanford is allowed to do this because they choose to formalise predicate logic in such a way that there are no (fundamental) function symbols. That's their choice, but we shouldn't push that on our readers. However, I think that it could have been more clear in the article how the idea of a "mapping" should be interpreted in the situation where one makes the same choices as Stanford. I hope that my additions to this article and to Functional predicate have helped with this. (As for the name, I decided that "mapping" was just far too general for anything, so I made Mapping a disambiguation page.)

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, this is essentially why "my sense" (by which I assume you mean what I introduced above with "if I say that") is equivalent to Stanford's sense. That is, they prove the equivalent theorems. Thus, if you use "my sense" to formalise mathematical practice or design an automated proof checker and then use Stanford's sense to apply Gödel's incompleteness theorems, you're OK -- the two senses are equivalent.

In fact, I do like "my sense" much better than Stanford's/Gödel's/yours, so I'll remove the scare quotes; it is my sense. But I'm not trying to write the article in my sense; I don't want an article appropriate for CS-oriented logicians but inappropriate for traditional logicians any more than the other way around. The important thing is that a statement P about an alleged "functional predicate" F is, in certain contexts, simply an abbreviation for a statement P' about a relational (ordinary) predicate F' -- derived according to the algorithm now on Functional predicate. So I don't think that the article was deficient as I originally wrote it WRT referring to a "mapping" and not to a predicate in two variables subject to a certain condition -- since the latter is exactly what it was referring to under certain conventions of abbreviation. Nevertheless, the original article was certainly deficient WRT not explaining this situation very well (or at all, really)! I think that it's better now.

As for the sources on the WWW:

• If we start with http://plato.stanford.edu/entries/set-theory/ZF.html;
• Then Podnieks' does things in the same style but states slightly different axioms in achieving it (→ vs ↔);
• And University of Queensland has the same logical content as Podnieks' but refers to the formalisation in a different way (without the z);
• And Paul Taylor writes almost the way that I originally had it, even with "one axiom for each functional relation" and everything.

None of these would agree entirely with how the article is now written, but the article is still consistent with them all. -- Toby 03:34 Jan 27, 2003 (UTC)

On second look, the Taylor link appears to be incomplete; I can quote from a print copy if anybody's concerned! -- Toby 03:45 Jan 27, 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.

Any of those meanings may be intended, depending on exactly how you formalise the language that you write ZFC in.

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?

Yes, I've seen it done formally in books on logic, and informally, mathematicians use function symbols for basic ZFC concepts all the time (although whether or not they are fundamental is impossible to decide in an informal context). Even one of the links that you provided used a function symbol, the constant (nullary function) symbol ∅, although it was derived (as a consequence of a theorem following from the axiom of empty set). Other function symbols that might be taken as fundamental are:

• braces and commas (for the axiom of pairing);
• ∪ (for the axiom of union); and
• set builder notation (for the axiom schema of separation).

In general, every time you have an axiom stating the existence of an object with a certain property, you could just as easily introduce a fundamental function symbol and let the axiom state that it has that property (assuming that one can prove that the object with that property is unique, which one can in all of these situations thanks to the axiom of extension). Introducing such symbols more closely mimics actual mathematical practice, where such symbols are indeed used; on the other hand, they complicate the language, making it harder to prove metamathematical theorems. Which you choose to do will depend on your purpose; you can rely on general theorems of logic to ensure that it doesn't matter (that is, the metamathematical theorems that you proved for the simple language with few symbols will apply to the larger language that more closely mimics mathematical practice). As for intended interpretation, the examples that I mentioned are intended to mean:

• the empty set, for ∅;
• the set whose members are some given objects, for braces and commas;
• the union of the members of a given set, for ∪;
• the set of members of a given set satisfying a certain property, for set builder notation.

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).

That's certainly not a requirement of all axiomatisations; that's a requirement of recursively enumerable axiomatisations. Of course, such axiomatisations are important, since major theorems like Gödel's apply to them. If you wish to say that the axiom of replacement applies to functional symbols defined after proving a uniqueness theorem, then you may. You can recursively enumerate all uniqueness proofs, but this is still problematic for some purposes, since there is no algorithm for deciding whether a given proposition is an axiom. To fix this, you can algorithmically rephrase the axiom schema in terms of relational predicates (as done on Functional predicate) and then insist on using only the fundamental predicates (relational or functional, if you make any functional predicates fundamental). A theorem of logic states that either set of axioms proves the same theorems, so do whatever best suits the purposes at hand. (There's also no reason not to allow the axiom schema of replacement when proving the uniqueness theorem; the theorem of logic may still be proved by induction on the length of the uniqueness proof.) ZFC has nothing to do as such with how you choose to formalise the language of your proving system; it has to do with what can be proved by that system and the intended interpretation of those theorems as statements about sets.

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.

Of the above references, Taylor is CS-oriented. I don't believe that there are fundamentally different ways of formalizing ZFC either. There are certainly different ways of formalizing the language of predicate logic in which ZFC is written, but even these differences don't seem very fundamental to me. They all have equivalent proving power and each can be interpreted in the others (else we wouldn't be talking about the same ZFC). Even the "traditional way" has never been traditional in some mathematical traditions; it's traditional among logicians, who want to keep the language simple so that they can prove metamathematical theorems about it easily. But such theorems have little to do with the ordinary mathematics that can be built upon ZFC as a foundation. OTC, it's the CS people, trying to design automated proof-checkers that can actually be used by working mathematicians, that use the more involved language because it more closely corresponds with mathematical practice. In any case, since the differences are not fundamental and have little to do with the nature of this particular axiom, I think that a discussion of these issues is out of place here. It would be great for another article -- although I don't really consider myself qualified to write such an article. (I'm comfortable using different formalisations of the language of predicate logic and translating between them, but I understand the differences between them only at a practical level. For example, I don't really know when it's necessary to be able to algorithmically decide whether or not a propoisition is an axiom and when it's sufficient to be able to recursively enumerate the axioms.) As for the "other complaints on this page", there is only one post by somebody other than ourselves, that of Matthew Woodcraft. While his post did address the difference between the functional formulation and the relational formulation, ultimately, it was a response to an actual error in the article that I did fix.

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)

That's how I found Taylor's book! But I will obviate the need to go the library again, because despite everything that I just wrote, you have convinced me that the article needs to be changed much along the lines that you want. What convinced me is a matter that I haven't addressed yet today: the issue of clarity. Apparently, the article is not clear to you, who actually know more about the issues involved than should be expected of the intended audience of this article. Therefore, there is a problem. Furthermore, in reviewing our past correspondence, I see a claim that phrasing the axiom in this way is "more general" than phrasing it your way, and that's just not so. Just as the functional language can be reinterpreted in the relational language, so the relational language can be reinterpreted in the functional language. Indeed, how else would anyone know how to write it in the functional language, given that Frankel originally wrote it in the relational language? (which he may not have, it might be interesting to look his original work up). While I do believe that the functional language gets better at the heart of the meaning of the axiom, that insight can always be described further down in the article. This is enough to convice me to change it. And I have a new reason of my own; I want to add to the article, contrasting the axiom schema of replacement with the axiom schema of collection, and this is more clear in the relational language. So, I will rewrite it now. -- Toby 07:12 May 1, 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

Axiom of boundedness?

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.:

$(\forall X,\exists \,Y:P(X,Y))\rightarrow \forall A,\exists B,\forall C:C\in B\iff \exists D:D\in A\land P(D,C)$

which can't be right. I think we want something like

$(\forall X,\exists \,Y:P(X,Y))\rightarrow \forall A,\exists B,\forall C:C\in A\rightarrow \exists D:D\in B\land P(C,D)$

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 F[X], 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)

Got it. x is actually the element, and f(x) maps to the class { y | P(x,y) }, collapsed to minimum rank. Errr, this leaves out the bit which says that we can collapse a class to a set like this, the article on rank doesn't help, and the intuition for "collapse" is much weaker than the intuition for "replacement" in the first place! -Dan 16:32, 1 May 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)

Function

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