text:
Talk:Axiom schema of replacement

What is a mapping?
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)

 * Brackets are the only notation I've seen anywhere else. I just changed it. I ought to log in one of these days, but here's a date stamp 85.50.128.216 (talk) 07:32, 15 November 2012 (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, \exist\, Y: P(X, Y)) \rightarrow \forall A, \exist B, \forall C: C \in B \iff \exist D: D \in A \land P(D, C)$$

which can't be right. I think we want something like
 * $$(\forall X, \exist\, Y: P(X, Y)) \rightarrow \forall A, \exist B, \forall C: C \in A \rightarrow \exist 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)

Axiom of Boundedness (part 2)
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)
 * All boundedness/collection guarantees is that there exists a B which contains an R-image of x for every x in A. It doesn't give us a set containing all the R-images. Thus in this case all it says is that there is a set which has an element. Algebraist 21:16, 30 March 2008 (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, wat are u talking about? A is a B, B is a A.

 * The issue here is that the "function" being described in the axiom of replacement is not actually a set function; it's really just a formula φ(x,y) that happens associate a single y with each x. — Carl (CBM · talk) 21:24, 30 March 2008 (UTC)

Replacement plus Nullset equals Collection plus Separation
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)

 * They are both mentioned, at least. I copyedited the proof that replacement and empty set imply separation a few days ago. The article currently just says that ZC proves that replacement and collection are equivalent, but doesn't go into detail.
 * As long as we're making a todo list: the first displayed formula now has the parameters w visible, but the other two don't. The role of the parameters isn't mentioned. — Carl (CBM · talk) 12:46, 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).

 * Suppose R is a non-vacuous property of sets, and let x be some particular set with property R. Define a function F such that F(y) = y if y has property R and F(y) = x otherwise. Then the range of F is exactly the collection of sets with property R. Whether this argument can be formalized in a particular set theory depends on exactly how the axiom of replacement is stated as an axiom and exactly which other axioms are included. — Carl (CBM · talk) 14:06, 20 March 2009 (UTC)

 * Also, you do not literally need a function for the axiom of replacement - that's why it's an axiom scheme. You just need a formula of two variables that defines a function. There is no need for the function defined to exist as a set (the whole point of the axiom of replacement is to show that any initial segment of a definable class function does actually exist as a set). — Carl (CBM · talk) 15:56, 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 $$\exists Y,\forall x,(x\in X\cap\hbox{Domain}(R)\Rightarrow R(\{x\})\cap Y\neq\emptyset)$$. Or in low-level logic notation, $$\exists Y,\forall x,((x\in X\land\exists a,R(x,a))\Rightarrow\exists b,(b\in Y\land R(x,b)))$$. 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)

 * I apologize; I misread your original query. I also don't see why replacement and collection would be equivalent without the axiom of choice. For a quick check, I looked at the SEP article here and they explicitly say that the two are equivalent over the other axioms of ZFC.   If the form of collection stated in this article is equivalent to replacement over the rest of ZF that would be remarkable.  For now, I have rephrased the article to be more clear about the equivalence that I know holds. JRSpriggs may be able to explain a better proof of the equivalence.

 * One perpetual source of confusion is that there are lots of different things that are called that axiom of replacement and the axiom of collection, and it might be that if these are chosen very carefully then AC is not required to prove the equivalence. For example, if in the axiom of collection required that for each x there was a unique y, without assuming there are no other elements in the set being constructed, this would probably be equivalent to replacement without the axiom of choice. — Carl (CBM ·&nbsp talk) 13:52, 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)

 * To show that Replacement implies Collection:
 * Suppose that we have φ such that $$\forall x\, \exist\, y \phi(x, y, w_1, \ldots, w_n)\,.$$ Let ψ be defined by $$\psi(x, p, w_1, \ldots, w_n, A) \equiv p = inf \{ rank (y) + 1 | (y = \{\} \land x \notin A) \lor (\phi(x, y, w_1, \ldots, w_n) \land x \in A) \} \,.$$ Applying replacement to ψ we get P, the set of such p for x in A. Let $$r = \cup P \,.$$ Let $$B = V_{r} \,.$$ Then $$\forall x \in A\, \exist y \in B\, \phi(x, y, w_1, \ldots, w_n) \,.$$
 * In addition to Replacement, this proof probably requires: null-set, pairing, union, powerset, extensionality, and regularity. I do not believe that it needs choice or separation (since that follows from replacement). JRSpriggs (talk) 15:18, 21 March 2009 (UTC)

 * Thanks; the direction that I didn't see immediately was that Collection implies Replacement, because I was overlooking something obvious. By the way, this discussion reminded me that we also didn't have an article on Scott's trick. — Carl (CBM · talk) 15:53, 21 March 2009 (UTC)

 * Re Alan: there are subtly different version of ZF around, in the sense that different authors use different axioms. However, I have never seen an example where there are two theories ZF(1) and ZF(2) defined by different authors, where either ZF(1) doesn't prove ZF(2), or vice versa. That would be an interesting example if it exists. — Carl (CBM · talk) 15:53, 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)

 * Vr is a set from the cumulative hierarchy. Here is a prose exposition of the proof that may be more clear. We know that for all x in A there is at least one y with φ(x,y). Thus for each x there is some minimal rank σx of a witness y. Define a function F from A to the ordinals that maps x to this minimal rank σx. Then, by replacement, the range of F is a set O of ordinals. Any set of ordinals has an upper bound; take σ to be an upper bound of O. Then every x in A has a corresponding y of rank no more than σ, so the set Vσ contains at least one y for each x in A, as desired. The key point here is that it is possible to prove that every set has a rank in ZF without the use of AC, and also possible to define each of the sets Vα. — Carl (CBM · talk) 02:54, 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)

 * This comes down to proving that every set has a rank, which is done in many set theory texts. It does not require anything outside of ordinary ZF to do this. — Carl (CBM · talk) 01:54, 24 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)

 * I think your suggestions for improving the article are sound. By the way, Kunen explicitly states (theorem 4.1) that, relative to ZF without the axiom of foundation, the axiom of foundation is equivalent to the proposition that every set has a rank (which, in his notation, is the statement V = WF). — Carl (CBM · talk) 15:40, 24 March 2009 (UTC)

Models of Zermelo's set theory
The section Axiom schema of replacement 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)

 * It may depend on exactly how the axiom of infinity is stated, but the axiom of infinity will usually give you Vω and so it's Vω + ω that's problematical. If it doesn't, I would take that as a sign that the axiom of infinity wasn't stated correctly for use in Z set theory. — Carl (CBM · talk) 12:24, 25 February 2010 (UTC)

 * Yes. If, instead of the usual axiom of infinity aimed at producing ω, you said that there is a set which contains the empty set and is either closed under power set and separation or closed under pairing and union, then you could establish the existence of Vω. But I have not seen that version. JRSpriggs (talk) 01:50, 27 February 2010 (UTC)

 * Better, use $$\exists I \, ( \{\} \in I \land \forall x \in I \, \forall y \in I \, ( x \cup \{ y \} \in I ) ) \,.$$ The only difference between this and the usual axiom of infinity is that x and y may be distinct here and are forced to be the same there. JRSpriggs (talk) 18:32, 28 February 2010 (UTC)

Bijection or Surjection
"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)

 * Well caught. Everyone else had overlooked this egregious error until you fixed it. Thank you. JRSpriggs (talk) 05:07, 27 October 2012 (UTC)

definiteness
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 am not aware of any place it is mentioned in Wikipedia.
 * Is Zermelo's idea more restricted than first order definability (say Σ0 as in Kripke–Platek set theory) or more general as in second order logic? JRSpriggs (talk) 10:27, 14 April 2015 (UTC)

 * Dear IP 86.127.138.67, Ebbinghaus has at least 13 books. Which one are you referring to? Tkuvho (talk) 12:03, 14 April 2015 (UTC)
 * His biography of Zermelo. After a bit of reflection, the obvious place to detail Zermelo's notion of definiteness would be Zermelo set theory, which would also save that page from being a mere reduct of the article on ZFC. 86.127.138.67 (talk) 15:23, 14 April 2015 (UTC)
 * Zermelo's notion was initially vague. He defined it better in a 1929 paper and it led his to try and base set theory on infinitary languages (and I think 2nd order logic) in opposition to Skolem. In Zermelo's biography (by Ebbinghaus) there are 50-100 pages (somewhat spread out) that cover his dispute with Skolem. The fact that these things have become obscure (to the general mathematical public) by the passage of time are perhaps what makes Ebbinghaus' biography of Zermelo a worthwhile reading... 86.127.138.67 (talk) 15:30, 14 April 2015 (UTC)
 * You seem to be familiar with this material more than most editors here, so I would like to warmly encourage you to give some details either at Zermelo set theory or at Zermelo himself. Tkuvho (talk) 16:03, 14 April 2015 (UTC)

The axiom schema of Boundedness
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 Zuhair: You are correct that B cannot be free in φ.
 * However, I think that the problem is that you are interpreting the phrase "without any restrictions on the predicate, φ" differently than intended. It is supposed to mean that the hypothesis containing φ occurs after the "∃B" rather than before it.
 * I am sorry, but I cannot think of any better wording that would make that more clear. JRSpriggs (talk) 06:17, 21 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)

 * Feel free to correct it as you see fit. JRSpriggs (talk) 08:19, 21 September 2015 (UTC)

Axiom schema of collection deserves its own article
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)

title: Talk:Axiom schema of replacement


text:
Talk:Power-to-weight ratio

Untitled
Since we have the power/weight ratio of batteries and fuel cells, it would be interesting to compare this with petrol and diesel fuels, too. Also could add other common forms of transport such as motorbikes, trains, boats. Milliondead (talk) 23:15, 16 March 2009 (UTC)

 * Fuels don't have a power to weight ratio, since you can generate power from them at arbitrary rates by using them up at essentially arbitrary rates, it's the engine that has the power to weight ratio.- (User) Wolfkeeper (Talk) 01:47, 17 March 2009 (UTC)

 * For example, a fuel with 42 MJ/kg burnt in one second gives 42MW. If burnt in half a second it is 84MW.- (User) Wolfkeeper (Talk) 01:53, 17 March 2009 (UTC)

 * They have a fixed energy/weight ratio though.- (User) Wolfkeeper (Talk) 01:47, 17 March 2009 (UTC)

A lot of these could be also applied to cars.

 * Done. --Robert Merkel 01:11 Jan 6, 2003 (UTC)

Is square of the square a typo? If not, we can call it fourth power. Patrick 01:21 Jan 6, 2003 (UTC)

 * Yes, it's fourth power. I was in "keep it simple for the plebs" mode, which is probably inappropriate here. --Robert Merkel 01:34 Jan 6, 2003 (UTC)

I'm not so familiar with this term but let me ask. Is it correct that "power loading = weight / power"? (I found this on D.P.Raymer's "Aircraft Design") If so, it seems to me better to clarify this point. - Marsian // talk 14:20, 2005 Jun 17 (UTC)

Sukhoi T-50
According to russian wikipedia charachteristics of this plane are understated. It weights a tonn less and produces more thrust with the new engine.

Aircraft
The section about "in an aircraft it's more critical than in any other vehicle" could reworded a bit. As far as I can tell, much of the information there applies to other vehicles as well... "power-to-weight greatly affects top speed...  if two engines produce the same power, the lighter one will produce a better car". The basic premise isn't incorrect, but some of the explanations don't seem to clearly differentiate aircraft from other vehicles. --Interiot 13:00, 20 April 2006 (UTC)

 * Induced drag is proportional to weight, so a heavier aircraft will consume more power for the same airspeed compared to a lighter one. — Preceding unsigned comment added by 2.29.18.184 (talk) 09:44, 1 May 2015 (UTC)

flight power (hamish)
Can we go neculer with aircraft using less fuel. Or can we use the sun to harness the power for flight —The preceding unsigned comment was added by 68.154.210.39 (talk) 14:20, 23 February 2007 (UTC).

flight power (hamish)
Can we go neculer with aircraft using less fuel. Or can we use the sun to harness the power for flight. —The preceding unsigned comment was added by 68.154.210.39 (talk) 14:21, 23 February 2007 (UTC).

Table
If we're going to have a table to give people ideas of typical values, anyone else think it'd be more useful to have the power/weight ratio of the car rather than just an engine. Automotive mags often write about power/weight ratios of cars- I haven't seen them talk about it in reference to just the engine much. Also, anyone else think a sampling of typical cars is more informative than a bunch of exotic high-powered cars? Friday (talk) 15:11, 29 May 2007 (UTC)

Under the heading "Notable low marginal power", the tables list power-to-weight ratio in lb/hp. This should be hp/lb —Preceding unsigned comment added by 148.163.178.11 (talk) 22:19, 11 January 2010 (UTC)

 * Would someone be keen to fix the long standing anomaly of lb/hp rather than hp/lb in the lists (not just the notable low ratio one). It seems a heap of values need inverting? 124.170.53.76 (talk) 05:37, 14 May 2010 (UTC)

In the "Electric Motors/Electromotive Generators" section, the values in the table for the Prius 2004 are wrong. Just by intuition there's no way the Prius 2004 motor mass is 183 kg. Go to the link at http://www.magnets.bham.ac.uk/documents/Jewell.pdf. "Total active mass = 36.3kg; Power density = 1.37kW/kg" I'm too lazy to figure out how to edit the table, so somebody please fix it. 69.226.238.225 (talk) 05:58, 5 March 2010 (UTC) RWconsult

More cars to compare + powers/weights
Added some more cars to the list. More mainstream cars should make the comparisons more valid to most users. Also added the weights and powers for additional info. Keppelk (talk) 11:55, 31 August 2008 (UTC)

Ultima
The Ultima GTR 720 makes 720 bhp. —Preceding unsigned comment added by 99.59.26.101 (talk) 03:41, 19 July 2009 (UTC)

Torque?
This article makes no mention of torque, I know the industry standard (For motor vehicles at least) is power-to-weight ratio, but torque-to-weight ratio is at least as relevant. For example from the article:

Turbocharged V-8 diesel engine Power to weight ratio: 0.25 hp/lb / 410 W/kg Total Power Output: 250 hp / 186 kW

So the peak power is respectable but it isn't amazing for a V8, but being a) turbo charged, b) V8 and c) diesel, I'd hazard a guess that the torque is going to be quite impressive (I know this is probably a fictional engine and there are many other factors, but I'm grossly generalising here). It may even have a higher peak torque than the F1 car:

BMW P84/5 2005 (Formula 1) Power to weight ratio: 4.6 hp/lb / 7.5 kW/kg Total Power Output: 925 hp / 690 kW

Also no mention of power curves is made, for example a V8 may have a very shallow power curve but stays above 150 kW for half of it with a peak of 200 kW, but it will have a worse power-to-weight ratio of a same weight 4 cylinder with a large turbo, sharp peak power of 250kW and average power of say 50kW.

Anyway, sorry about the rant, my point is that I don't think this article mentions the other factors enough such as power curve, torque curve and even max rpm. Hullo exclamation mark (talk) 11:43, 14 September 2009 (UTC)

Hullo, yes, and for good reason. Power is torque * rpm. Torque is independent of power. With gears you can get as much torque as you want from any power. -Jason Arthur Taylor — Preceding unsigned comment added by 96.231.140.87 (talk) 14:42, 22 August 2015 (UTC)

Weight-to-power - Vandalism?
Power-to-weight ratio is commonly given in bhp/tonne or kW/tonne... Hence power divided by weight.

The tables in this article appear to quote weight-to-power ratios. Is this deliberate or has someone taken it upon themselves? —Preceding unsigned comment added by 80.6.35.235 (talk) 11:42, 8 May 2010 (UTC)

 * Looking at the logs, someone in the past pushed for weight-to-power ratio (as can be seen with the "power loading" mention). The United States customary units were at that time made weight-to-power.  This appears to have been maintained.  Should it be eliminated (it does seem wrong)?  The SI units appear correctly power-to-weight.  Anyone game to make all the conversions/inversions? 124.170.53.76 (talk) 05:50, 14 May 2010 (UTC)

'Flight vehicles'?
I've changed the table heading for 'Sports and Flight Vehicles' to read 'Sports vehicles and Aircraft', though really they need to be in separate tables. Can someone with the appropriate know-how do this?

I'm also unsure about the power specified for the Spitfire and Bf-109: these look like mid-war figures, not the figures for the prototypes as given. This needs confirmation elsewhere. AndyTheGrump (talk) 02:05, 6 November 2010 (UTC)

Jet Engines
Two problems with the jet engines in the power/weight table: 1) The engines (GE CF6-80C2 and GE90-115B) should not be referred to as "Brayton" jet engines. Just call them by the actual given name, e.g. GE90-115B turbofan. Drop the obscure, pedantic eponym. 2) The output of a jet engine is measured in thrust (units of force), not power (force*distance/time). If you look up the specs for any jet engine, the output will be given in lbf. or N. You cannot arbitrarily convert the thrust produced by a jet engine (or rocket engine) into horsepower or watts. Because the power output of a jet engine cannot be readily determined, but the thrust can easily be measured, the performance of a jet engine is given by thrust/weight, not power/weight. It is nonsensical to say that the GE90-115B produces 85,000 horsepower. A jet engine on a test stand, producing the maximum rated thrust, 513kN in the case of the GE90-115B, is producing no power because it is stationary. Zero power. When the airplane is in motion, then the engines are producing power, and it is theoretically possible to calculate the power, but you would have to somehow already know the thrust required for the given airspeed.157.182.105.1 (talk) 02:28, 7 March 2011 (UTC)

 * How about including some turboshaft engines instead? That sounds more reasonable. Martijn Meijering (talk) 13:28, 23 December 2012 (UTC)

 * It is mentioned in the article that "For jet engines there is often a cruise speed and power can be usefully calculated there, for rockets there is typically no cruise speed, so it is less meaningful.". This description could be expanded to better explain the problem with power/weight ratio as it applies to the broader set of jet propulsion engines (inc. rockets).  Elimination of obscure use of terms is also a good idea.   As for the power output from a jet engine on a test stand, the following analogy might be useful: A lithium ion battery at open circuit voltage is producing no power because it is not loaded.  Zero power.  When the battery is loaded, then it is producing power, and it is possible - given a known load and a current flow through an ammeter to calculate the power.  Would you need to know prior to the test the current flow?  No - it would be measured.  As for the GE90-115B and it's output power, look carefully at the listing for GE CF6-80C2 in the Boeing 747 which is also sold by General Electric as the aeroderivative LM6000.  The one of GE spec sheets cited (the LM6000 one) specifically describes the average output power of the turbine at rated mechanical load at sea level at 59°F.  Is it nonsensical to say that the LM6000 produces 59,900 hp?  Perhaps one could ask about the ratio of rotating power output to exhaust (jet) power output between the aeroderivative and aerotuned variants.  Just ask GE.  For the GE90-115B, based on the values at writing quoted for a  Boeing 777-200LR at "typical cruise speed" of 0.84 Mach, at 35000 ft, 512kN being the maximum loaded thrust (which is probably more than the thrust at typical cruise speed; thrust will vary with drag and reducing fuel load at cruise speed), -40°C being the prevailing temperature, my calculations suggest (a) speed of sound in surrounding air is 305.8 m/s and (b) thus, 132,000 kW ~ 176,000 hp maximum typical cruise power output (2 engines for redundancy, wear sharing and weight balancing, not power) so the original figure looks wrong. 124.149.47.244 (talk) 02:47, 16 April 2011 (UTC)

 *  More importantly, thrust varies with air density. The numbers in the table for the 747-300 at altitude are grossly over-estimated. Cruise power is only tens of thousands of hp. ( What is the drag? Answer: weight divided by lift/drag ratio!) 86.181.117.134 (talk) 05:25, 16 May 2012 (UTC)

 * Please note re: above comments that the L/D ratio of any object is not a fixed value but depends on it's relative velocity. The induced drag can be held constant with increasing aircraft weight by holding a constant angle of attack, but doing so requires an increase in speed.  This speed increase effects an increase in parasitic drag, which means that in general holding vehicle shape constant while increasing mass will affect a lower L/D ratio.

 * While a jet on a test stand remains stationary, the air around it does not. Since thrust specifications are typically quoted based on sea-level standard atmosphere (SLS) conditions, is there a formula to calculate the force applied to accelerate that SLS air from rest to the velocity needed for the given thrust? If so, could that be combined with the length of the engine (distance) to calculate power (F×d/t)? sn‾uǝɹɹɐʍɯ (talk) 23:03, 19 February 2013 (UTC)

 * To say that a stationary jet engine can have its thrust assessed (Newtons) but not its power (kilowatts) is nonsense. True, mechanically the jet engine is not moving and from that perspective does no work. As alluded above, the exhaust is moving and represents work even if not easily quantified. The most practical power assessment of any engine is its power consumption in terms of the fuel consumed!  The amount of fuel per second consumed represents the amount of chemical energy per second, thus power.  The tables should have a column to show this.

"Power" in this context refers to shaft power. So for a turbofan engine, that would be the shaft power available to the fan, torque times angular velocity in radians. That is non-zero even when the engine is bolted to a test stand. It is true that when looking at the larger system, the net mechanical power produced is zero as long as the test stand doesn't move, but this is irrelevant pedantry. The various diesel, electric and pneumatic motors listed on this page also produce zero power when spinning against a brake on a test stand, but their specifications show shaft power.--Yannick (talk) 22:53, 29 August 2015 (UTC)

power to weight ratio of one notable car – GM EV1
Consider adding electric car by General Motors – EV1. It's ratio equals 97.86 bhp/ton  — Preceding unsigned comment added by 83.26.66.28 (talk) 13:16, 26 March 2012 (UTC)

I think "Supersonic vehicles" should be deleted
I dont know what engineer wannabe wrote this table but its COMPLETE nonsense. Its obviously calculated by this simple formula : Power = (Engine Thrust in Newtons) x (Aircraft Mach number) x 1236 / 3.6 (km/h to m/s conversion).

1-In engine specifications, the engine thrust is stated as "uninstalled thrust". As soon as it is installed into airframe, it wont be giving its uninstalled thrust.

2-Even more importantly, intake design dictates how dynamic thrust of engines will be. A fixed inlet optimized for transonic regime wont be giving ANY thrust supersonic, no matter how powerful engine is(for example Su-25), but a optimized variable inlet can give even higher than uninstalled thrust at high supersonic speeds. To compare, a MiG-25 with 200kN total thrust 0.55 T/W, and a draggy airframe can reach M2.83 with 4 missiles, but a clean F-15C with 220kN total thrust, twice T/W and less draggy/lighter airframe cant. In short, its wrong to assume engine gives the same thrust at all speeds.

3-Engine thrust is also dependent on altitude, so its also wrong to assume sea level static thrust applies to all altitudes. (Obviously most aircraft reach their top speeds at 20000+ feet)

4-Mach number also changes with air altiude, so multiplying with 1236 is also wrong.

Most of these goes for rockets (space shuttle etc). In that case, thrust depends on altiude, airspeed, compressibility and nozzle design point. So unless anyone objects, I will be deleting all these aircraft relates bullshit from the article. Its a embarassing table for a site calles itself encyclopedia. Andraxxus (talk) 20:46, 3 June 2012 (UTC)

 * I wish to second the idea of deleting or significantly altering the "Supersonic Vehicles" section, jet engines and rockets because the link between power and weight for vehicles/engines in these classes is problematic towards meaningless. However I do see that ALL power plant forms have specific design considerations that prevent them delivering theoretical/uninstalled/laboratory performance specs.  It seems that this whole article needs a rethink.  An occasionally achieved peak power in a turbo small automobile is not directly comparable with the sustained power near peak of another multi-cylinder automobile designed to tow.  And then there is the aerodynamics of automobiles which are not even considered.  Comparing power-to-weight ratio seems only possible when comparing significantly similar vehicles under similar conditions.  In the aerospace arena, there are more variables that make significant effect on performance making comparisons virtually impossible and the power-to-weight ratio meaningless. 203.96.74.238 (talk) 05:39, 9 August 2012 (UTC)

 * I'd like to third the deletion...a quick unit conversion has the space shuttle producing 1 hp per 6 grams, which is patently absurd. The only way to squeeze that kind of energy out of that kind of mass is explosives.  I ran some more numbers, and it seems like whoever did the math is using the empty weight of the orbiter/boosters/external tank as the weight in the calculations.  This seems to be distorting the issue significantly, since at no point does the shuttle actually produce anywhere near that kind of power to weight ratio.  In a technical sense, it is correct in that fuel weight is not usually included in the power/weight formulas, but in this particular instance it leads to utterly nonsensical numbers.  One could easily argue that the SRB engine IS the fuel, and as the "engine" weight is changing during operation, the power/weight ratio becomes meaningless. It might make sense to run the calculations for a liquid fuel rocket, but for a solid fuel rocket it's like calculating the power to weight ratio of gasoline.  I vote for deletion on the simple basis that the numbers misrepresent reality, regardless of how they were calculated.  Or, for that matter, the "technical" correctness of the calculations. 66.42.152.225 (talk) 15:40, 8 November 2013 (UTC)

 * Actually the value for rockets depends on speed, and peaks at maximum thrust at maximum speed. Rockets are indeed insanely powerful. The power of a jet-propulsion engine is MAX(thrust x speed) where thrust is a function of speed, altitude. For a rocket thrust maximises in a vacuum as there's no aerostatic backpressure on the nozzle. Towards the end of the burn the space shuttle could accelerate at over 3g at a speed of 7.8km/s. That's over 30N per kg @ 7.8km/s, 234 kW/kg or ~300 horsepower/kg, 1 horsepower for every 3.2 grams, including (remaining) propellant, tanks, astronauts everything. So twice as good as 1 horsepower for every 6 grams. Hope this helps.GliderMaven (talk) 17:05, 4 December 2013 (UTC)

 * Concorde super-cruised across the Atlantic at Mach 2.0 on ~40,000lb of thrust, around the equivalent in power of a single early RB211. — Preceding unsigned comment added by 2.29.18.184 (talk) 09:37, 1 May 2015 (UTC)

 * This definition for "power" of a rocket is patently nonsense, as it depends on reference frame. How much power does the rocket produce relative to the surface of the sun?  How about relative to the center of the galaxy?  Does a simple model rocket produce nearly infinite power relative to red-shifted galaxies?  All accelerating vehicles push against something; in the case of a rocket, it is pushing against the fuel in it's tanks.  By calculating the power output of the space shuttle in the fashion used above, one ignores the power already delivered to the propellants in the fuel tanks earlier in the launch cycle to accelerate them to (nearly) orbital velocity.  A more reasonable definition of the power produced by a rocket is it's thrust multiplied by it's exhaust velocity.  — Preceding unsigned comment added by 71.174.93.74 (talk) 14:50, 22 March 2016 (UTC)

Ships?
Ships should be included in this article, as they are the most efficient movers of cargo, shown by the very low Power-to-weight ratio. I could not find references for the mass of an empty functional ship, but hopefully others have better luck. TGCP (talk) 14:37, 25 May 2014 (UTC)

External links modified
Hello fellow Wikipedians,

I have just added archive links to 6 one external links on Power-to-weight ratio. Please take a moment to review my edit. If necessary, add after the link to keep me from modifying it. Alternatively, you can add to keep me off the page altogether. I made the following changes:
 * Added archive https://web.archive.org/20090410050507/http://www.pmlflightlink.com:80/motors/hipa_drive.html to http://www.pmlflightlink.com/motors/hipa_drive.html
 * Added archive https://web.archive.org/20110722063309/http://www.die.unipd.it/personale/doc/Benato_Roberto/didattica/corsi/IMPIANTI_ELETTRICI_DI_BORDO_PER_IAS/2_zona_di_transizione/BATTERIE/Batt_SPV.pdf to http://www.die.unipd.it/personale/doc/Benato_Roberto/didattica/corsi/IMPIANTI_ELETTRICI_DI_BORDO_PER_IAS/2_zona_di_transizione/BATTERIE/Batt_SPV.pdf
 * Added archive https://web.archive.org/20090327125952/http://www.panasonic.com/industrial/battery/oem/images/pdf/Panasonic_LiIon_CGA103450A.pdf to http://www.panasonic.com/industrial/battery/oem/images/pdf/Panasonic_LiIon_CGA103450A.pdf
 * Added archive https://web.archive.org/20100601144233/http://www.a123systems.com:80/cms/product/pdf/1/_ANR26650M1A.pdf to http://www.a123systems.com/cms/product/pdf/1/_ANR26650M1A.pdf
 * Added archive https://web.archive.org/20081010022521/http://www.forcemotors.com:80/media/downloads/DIESEL3SEATER.pdf to http://www.forcemotors.com/media/downloads/DIESEL3SEATER.pdf
 * Added archive https://web.archive.org/20120312002705/http://www.autoindia.com/VehicleStyles/bike-car-details1086.html to http://www.autoindia.com/VehicleStyles/bike-car-details1086.html

When you have finished reviewing my changes, please set the checked parameter below to true to let others know.

Cheers. —cyberbot II  Talk to my owner :Online 03:33, 30 August 2015 (UTC)

External links modified
Hello fellow Wikipedians,

I have just modified 1 one external link on Power-to-weight ratio. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
 * Added archive https://web.archive.org/web/20131115181622/http://www.army.mil/factfiles/equipment/tracked/abrams.html to http://www.army.mil/factfiles/equipment/tracked/abrams.html

When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at ).

Cheers.— InternetArchiveBot  (Report bug) 12:19, 14 September 2016 (UTC)

External links modified
Hello fellow Wikipedians,

I have just modified 28 external links on Power-to-weight ratio. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
 * Added archive https://web.archive.org/web/20121102194334/http://eogld.ecomm.gm.com/images/mediumduty/techspecs/engine.pdf to http://eogld.ecomm.gm.com/images/mediumduty/techspecs/engine.pdf
 * Added archive https://web.archive.org/web/20100131071546/http://www.suzukimarine.com/sr_09/df25/features/ to http://www.suzukimarine.com/sr_09/df25/features/
 * Added archive https://web.archive.org/web/20100117211438/http://www.mazda.com/mazdaspirit/rotary/about/ to http://www.mazda.com/mazdaspirit/rotary/about/
 * Added archive https://web.archive.org/web/20100104164033/http://osengines.com/engines/osmg1401.html to http://www.osengines.com/engines/osmg1401.html
 * Added tag to http://www.geae.com/engines/commercial/ge90/ge90-115b.html
 * Corrected formatting/usage for http://www.nasa.gov/offices/oce/llis/0750.html
 * Added archive https://web.archive.org/web/20081209114436/http://industrial.panasonic.com/ww/i_e/25000/fa_pro_acs_minas_a4_e/fa_pro_acs_minas_a4_e/a4_16.pdf to http://industrial.panasonic.com/ww/i_e/25000/fa_pro_acs_minas_a4_e/fa_pro_acs_minas_a4_e/a4_16.pdf
 * Added archive https://web.archive.org/web/20120428153054/http://www.compactpower.com/Documents/MicrosoftWord-LG_Chem_pressrelease_finalon20080110.pdf to http://www.compactpower.com/Documents/MicrosoftWord-LG_Chem_pressrelease_finalon20080110.pdf
 * Added archive https://web.archive.org/web/20101122071429/http://www.saftbatteries.com/doc/Documents/defence/Cube769/VL45EFe.e3741a09-74fd-4df4-8687-12997f445ef5.pdf to http://www.saftbatteries.com/doc/Documents/defence/Cube769/VL45EFe.e3741a09-74fd-4df4-8687-12997f445ef5.pdf
 * Added archive https://web.archive.org/web/20100827142749/http://www.scib.jp/en/product/detail.htm to http://www.scib.jp/en/product/detail.htm
 * Added archive https://web.archive.org/web/20100827142848/http://www.scib.jp/en/product/spec.htm to http://www.scib.jp/en/product/spec.htm
 * Added tag to http://www.a123systems.com/a123/products
 * Added archive https://web.archive.org/web/20110718205602/http://www.saftbatteries.com/doc/Documents/defence/Cube769/VL6A_data_sheet.9ea09188-84ad-4c54-989b-a2206dc28da2.pdf to http://www.saftbatteries.com/doc/Documents/defence/Cube769/VL6A_data_sheet.9ea09188-84ad-4c54-989b-a2206dc28da2.pdf
 * Added tag to http://www.nesscap.com/data_nesscap/spec_sheets/Spec%2009.pdf
 * Added archive https://web.archive.org/web/20100206022503/http://www.nesscap.com/products_edlc.htm to http://www.nesscap.com/products_edlc.htm
 * Added archive https://web.archive.org/web/20130329161712/http://www.ga-esi.com/EP/capacitors/series-CMX-high-energy.php to http://www.ga-esi.com/EP/capacitors/series-CMX-high-energy.php
 * Added archive https://web.archive.org/web/20100802114428/http://www.redflow.com.au/Files/PowerBOSZB600%20-%20Limited%20Warranty.pdf to http://www.redflow.com.au/Files/PowerBOSZB600%20-%20Limited%20Warranty.pdf
 * Added tag to http://www.cfcl.com.au/Assets/Files/BlueGen_Brochure%28ENG_GER%29_Mar-09.pdf
 * Added archive https://web.archive.org/web/20090824003547/http://www.utcpower.com/fs/com/Attachments/data_sheets/DS0112_093008.pdf to http://www.utcpower.com/fs/com/Attachments/data_sheets/DS0112_093008.pdf
 * Added tag to http://www.fuelcells.org/info/charts/TransTechnical.pdf
 * Added archive https://web.archive.org/web/20090905173435/http://www.utcpower.com/fs/com/bin/fs_com_Page/0%2C11491%2C0115%2C00.html to http://www.utcpower.com/fs/com/bin/fs_com_Page/0%2C11491%2C0115%2C00.html
 * Added archive https://web.archive.org/web/20110707205935/http://www.ballard.com/files/pdf/Spec_Sheets/PEM_FC_Product_Portfolio_docmetrics.pdf to http://www.ballard.com/files/pdf/Spec_Sheets/PEM_FC_Product_Portfolio_docmetrics.pdf
 * Added tag to http://www.suntech-power.com/images/stories/2010_datasheets/EN/suntech_hiperforma_udm_en.pdf
 * Added archive https://web.archive.org/web/20091012184203/http://www.cyclingfitness.net/what-is-vam-and-how-to-calculate-it/ to http://www.cyclingfitness.net/what-is-vam-and-how-to-calculate-it/
 * Added tag to http://asmcommunity.asminternational.org/vgn-ext-templating/views/ASM/OpenDocument.jsp?vcmid=b6b1a538b5c81210VgnVCM100000621e010aRCRD
 * Added archive https://web.archive.org/web/20100922130438/http://www.thinkev.com/The-THINK-City/Specifications/Technical-data to http://www.thinkev.com/The-THINK-City/Specifications/Technical-data/
 * Added archive https://web.archive.org/web/20081121205210/http://www.mitsubishi-motors.com/special/ev/whatis/index.html to http://www.mitsubishi-motors.com/special/ev/whatis/index.html
 * Added archive https://web.archive.org/web/20110520033728/http://corporate.honda.com/environment/fuel_cells.aspx?id=fuel_cells_fcx to http://corporate.honda.com/environment/fuel_cells.aspx?id=fuel_cells_fcx
 * Added archive https://web.archive.org/web/20100701233257/http://www.internetautoguide.com/car-specifications/09-int/2006/hummer/h1/index.html to http://www.internetautoguide.com/car-specifications/09-int/2006/hummer/h1/index.html
 * Added archive https://web.archive.org/web/20061207091333/http://dieselmotorcycles.com/PDF/M1030M1_JP8_Diesel_Military_US.pdf to http://www.dieselmotorcycles.com/PDF/M1030M1_JP8_Diesel_Military_US.pdf
 * Added archive https://web.archive.org/web/20110708082559/http://www.bmwblog.com/docs/BMW_760i_760Li.pdf to http://www.bmwblog.com/docs/BMW_760i_760Li.pdf
 * Added archive https://web.archive.org/web/20111213171437/http://www2.mercedes-benz.com.au/content/australia/mpc/mpc_australia__website/en/home_mpc/passengercars/home/passenger_cars_world/news/September_2011/dtm_amg.html to http://www.mercedes-benz.com.au/content/australia/mpc/mpc_australia__website/en/home_mpc/passengercars/home/passenger_cars_world/news/September_2011/dtm_amg.html
 * Added archive https://web.archive.org/web/20100211102549/http://www2.bombardier.com/q400/en/specifications.jsp to http://www2.bombardier.com/q400/en/specifications.jsp
 * Added archive https://web.archive.org/web/20090407075947/http://www.marineturbine.com/downloads/2008_Turbine_SUPERBIKE_brochure.pdf to http://marineturbine.com/downloads/2008_Turbine_SUPERBIKE_brochure.pdf
 * Added archive https://web.archive.org/web/20110707191715/http://automobile.automotive.com/70233/0805-john-force-funny-car-legend/index.html to http://automobile.automotive.com/70233/0805-john-force-funny-car-legend/index.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

Cheers.— InternetArchiveBot  (Report bug) 18:00, 27 July 2017 (UTC)

Formula 1 engine BMW M12
I checked the reference, there was no weight and the power was just 850 bhp. I did not find anything about 1400 bhp org weight inArrows A10 or BMW M12. --Fisch4Fun (talk) 06:35, 17 October 2017 (UTC)
 * I inserted a reference for 1400 hp --Fisch4Fun (talk) 07:12, 17 October 2017 (UTC)

Toshiba SCiB cell 4.2Ah Li2TiO3 Lithium-ion battery Comment
I've removed the C/12 rating for the Toshiba SciB cell. The math was wrong (50A at 2.4V is 120 W, not 600W), and the cited source doesn't mention a 50A discharge at all. What it does mention is charging at 50A:

More than 90 percent of the SCiBTM cell capacity can be charged in just 5 minutes using a large charging current (max. 50A). Dominik Honnef (talk) 20:27, 8 September 2020 (UTC)

Split
This article is now 78 pages long and has ~500 refs in it. How about we split the examples into another article for people who want to see the details and leave this article to explain the definition and interpretation of the concept? Lfstevens (talk) 19:12, 13 May 2021 (UTC)

Electric motors and electromotive generators : Data Problems
Hi, the section on electric motors appears poorly sourced and unreliable. When the links are followed, they don't go to specific product pages and the products that are there don't seem to match the claimed results for H3X and Integral. I was trying to verify claims and power levels and weights didn't seem to match up let alone Power/Weight ratios. Perhaps an Editor should assess wether this is [UNRELIABLE] and wether it should remain in the article? Patbahn (talk) 17:40, 8 July 2022 (UTC)

Point of the lists?
What's the point of the lists? I do not think it passes WP:NLIST. X750. Spin a yarn? Articles I've screwed over? 21:48, 5 April 2023 (UTC)

Humans Power
Remove any mention of any athletic achievement since most professional, if not all, cyclists are 'doped up to the eyeballs' and does not accurately portray their power but how well their team doctor can concoct something 'good' and undetectable to enbale them to cheat. The issue is that the cyclist mentioned was caught doping with asthma medication and collapsed from excessive use. 210.84.5.219 (talk) 14:04, 23 March 2024 (UTC)

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Talk:Power-to-weight ratio