Fork me on GitHub
Math for the people, by the people.

User login

Zermelo-Fraenkel axioms

set theory
Zermelo-Fraenkel set theory, ZFC, ZF
Type of Math Object: 
Major Section: 

Mathematics Subject Classification

03E99 no label found


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?

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.

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.

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.

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.


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.

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)".

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"

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.

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.

Subscribe to Comments for "Zermelo-Fraenkel axioms"