Zermelo-Fraenkel axioms
Primary tabs
Zermelo-Fraenkel axioms
Ernst Zermelo and Abraham Fraenkel proposed the following axioms as a foundation for what is now called Zermelo-Fraenkel set theory, or ZF. If this set of axioms are accepted along with the Axiom of Choice, it is often denoted ZFC.
-
Pair set: If and are sets, then there is a set containing only and .
-
Axiom of power set: If is a set, then there exists a set with the property that iff any element is also in .
-
Replacement axiom: Let be some formula. If, for all , there is exactly one such that is true, then for any set there exists a set with the property that iff there exists some such that is true.
-
Regularity axiom: Let be some formula. If there is some that makes true, then there is a set such that is true, but for no is true.
-
Existence of an infinite set: There exists a non-empty set with the property that, for any , there is some such that but .
-
Separation axiom: If is a set and is a condition on sets, there exists a set whose members are precisely the members of satisfying . (This axiom is also occasionally referred to as the subset axiom).
Mathematics Subject Classification
03E99 None of the above, but in MSC2010 section 03Exx
Comments
effective procedure to determine sethood?
I'm trying to write some code that will test an object for
sethood. I'm not sure where to start with this. I could,
for example, assume that every object was a set. Seems sort
of silly, but it is definitely simple. On the other hand, I
suppose I could in theory work up a program that would encode
these axioms (or some other set theoretic axioms) that test
for sethood in a nontrivial way. Does anyone have pointers
for anything like this that is out there already?
Re: effective procedure to determine sethood?
Of course, some sets are going to be pretty weird -- and
massively infinite in particular -- so the definition of
"effective procedure" should be tempered accordingly.
Re: effective procedure to determine sethood?
In what form is the object to be tested represented? It seems to me that, before I could instruct a computer to check if an object is a set, I need to know what sorts of objects are to be tested for sethood and have some idea how they can be represented as input data to the sethood-testing program.
Re: effective procedure to determine sethood?
Sure. I'll have to think more about it. But I know of at least
one language/system that would work as a foundation (*). Thanks for the reminder!
*: "A Theory of Sets" by A. P. Morse.
Re: effective procedure to determine sethood?
You might look here:
http://us.metamath.org/mpegif/mmset.html
or here:
http://www.mizar.org/project/
Re: effective procedure to determine sethood?
Wow, I'd never heard of the metamath project before.
Pretty cool, especially the fact that pretty much everything they have is public domain or Free.
http://us.metamath.org/copyright.html
Thanks!
The ZF Axioms of set theory
I looked at some of these ZF axioms of set theory to know what a set is, and they mention property. I clicked on property, it goes to function. I clicked on functions , it goes to relations. I clicked to relations, it goes to cartesian products. I clicked on cartesian products, it goes to ordered pairs. I clicked on ordered pairs, it goes to back to sets.
lol.
Re: The ZF Axioms of set theory
The study of axiomatic set theory, like, say, the "axiomatic" theory of groups, takes place in informal set theory. In the formal theory of ZF, the notion of "property" corresponds to that of "first-order definable in the language of ZF". For example, a set s has the property of being nonempty if and only if s satisfies the formula "Ey(y \in x)".
Re: The ZF Axioms of set theory
Ah yes, this is probably unavoidable.
My advice, take "set" to be something like Euclide's "point" and
"line." I think the phrase was "point: that which has no breadth"
What?!
A more serious response would be to refer you to Tarski's "Introduction to Logic" There is a Dover reprint now so it is very accessible.
What I like about that book is that Tarski avoids the usual problems of books like "Axiomatic Set Theory" and "Naive Set Theory" because he uses language, not symbols definitions and axioms (well he does eventually but the thrust is to convince you of logic by...logic). At first I thought this was cheap. Why can't math be written with precise axioms and symbols, so every step is proved by connecting these symbols according to their rules, I thought?
Now looking back I realize how wise Tarski was. He answered what a proof really is: a proof is any argument which convinces others that they too believe the claim. In this way a proof is completely language, it cannot be just connected symbols. It has to rely on some assumption that the other person believes and understands something fundamental already. If no one alive could read Greek, then the books of Euclid would not be full of proofs.
So if you want to start a theory, you have to start with an assumption of language. ZF assumes "property" makes sense. Even if we don't all have the exact same idea of what is a "property," the subtle differences so far haven't lead to a major conflict. We seem to know when something is a property and usually when something isn't a property. That makes it a good place to start.
Re: The ZF Axioms of set theory
Good point Ratboy, perhaps this could be added to the entry as a subentry? Fleshed out out a little of course. This might help future circular journeys.