You are here
HomeZermeloFraenkel axioms
Primary tabs
ZermeloFraenkel axioms
Ernst Zermelo and Abraham Fraenkel proposed the following axioms as a foundation for what is now called ZermeloFraenkel 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 $X$ and $Y$ are sets, then there is a set $Z$ containing only $X$ and $Y$.

Axiom of power set: If $X$ is a set, then there exists a set $\mathcal{P}(x)$ with the property that $Y\in\mathcal{P}(x)$ iff any element $y\in Y$ is also in $X$.

Replacement axiom: Let $F(x,y)$ be some formula. If, for all $x$, there is exactly one $y$ such that $F(x,y)$ is true, then for any set $A$ there exists a set $B$ with the property that $b\in B$ iff there exists some $a\in A$ such that $F(a,b)$ is true.

Regularity axiom: Let $F(x)$ be some formula. If there is some $x$ that makes $F(x)$ true, then there is a set $Y$ such that $F(Y)$ is true, but for no $y\in Y$ is $F(y)$ true.

Existence of an infinite set: There exists a nonempty set $X$ with the property that, for any $x\in X$, there is some $y\in X$ such that $x\subseteq y$ but $x\neq y$.

Separation axiom: If $X$ is a set and $P$ is a condition on sets, there exists a set $Y$ whose members are precisely the members of $X$ satisfying $P$. (This axiom is also occasionally referred to as the subset axiom).
Mathematics Subject Classification
03E99 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
Recent Activity
new question: Harshad Number by pspss
Sep 14
new problem: Geometry by parag
Aug 24
new question: Scheduling Algorithm by ncovella
new question: Scheduling Algorithm by ncovella
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 sethoodtesting 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 "firstorder 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.