Can the Axiom Schema of Comprehension be omitted from ZFC since it is implied by the Axiom Schema of Replacement?
-
1$\begingroup$ Yes. It's normally included because it's interesting to consider Z and ZF as subtheories. $\endgroup$– arsmathCommented Jan 3, 2015 at 21:31
-
5$\begingroup$ That's a weird tag... $\endgroup$– Alain ValetteCommented Jan 3, 2015 at 21:43
-
$\begingroup$ @AlainValette Fixed $\endgroup$– Yemon ChoiCommented Jan 3, 2015 at 21:50
-
2$\begingroup$ Of course, it also matters exactly how replacement is stated. If it is stated in the form sometimes called "collection", it no longer implies the comprehension axioms (this form of replacement only says that the image of the function is a subset of some set). But if we already include the comprehension axioms, then it makes no difference which form of replacement is included. To see why this is particularly relevant: the axiom of replacement stated in Kunen's standard book is the "collection" form which does not imply the comprehension scheme. $\endgroup$– Carl MummertCommented Jan 4, 2015 at 1:42
1 Answer
Yes.
However, historically (prior to the earliest axiomatizations of set theory) it used to be almost the other way round. Comprehension, as we understand it today, allows to construct subsets of other sets based on a formula; in earliest (and inconsistent) set theories it was used to construct sets out of the blue. This is sometimes called "unlimited comprehension" and it can be consistently introduced into some fuzzy set theories (that is, set theories not built on classical, two-valued logic). Unlimited comprehension had to disappear from mainstream mathematics with the discovery of set theoretic paradoxes.
I'm not going to state mathematically what exactly gets implied by unlimited comprehension in classical logic (well, everything does), but I can still claim that in early Cantor's work, many principles that later appeared as separate axioms of ZF were seen (as a matter of course) as direct applications of unlimited comprehension: axiom of sum, power set, pairing, infinity, and of course also replacement. In those happy days if you could write a formula that uniquely defined the membership of a set, you had that set created.
Allow me one more remark. Comprehension isn't the only "non-essential" axiom in the traditional formulation of ZF. Pairing follows from replacement, too. Replacement is actually an axiom schema and many of its instances follow trivially from its other instances. The point of the traditional "ZF" formulation is that it is easy to explain (especially as a replacement for its inconsistent, non-axiomatic predecessor framework with unlimited comprehension and extensionality as the key two principles), not that it is a minimal theory in any technical sense.
-
$\begingroup$ Concerning the last paragraph, there is a related question here: mathoverflow.net/questions/48365/… $\endgroup$ Commented Jan 4, 2015 at 12:08