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 Goedel'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 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