Source : Free On-Line Dictionary of Computing

axiomatic set theory
     
         One of several approaches to {set theory}, consisting
        of a {formal language} for talking about sets and a collection
        of {axioms} describing how they behave.
     
        There are many different {axiomatisations} for set theory.
        Each takes a slightly different approach to the problem of
        finding a theory that captures as much as possible of the
        intuitive idea of what a set is, while avoiding the
        {paradoxes} that result from accepting all of it, the most
        famous being {Russell's paradox}.
     
        The main source of trouble in naive set theory is the idea
        that you can specify a set by saying whether each object in
        the universe is in the "set" or not.  Accordingly, the most
        important differences between different axiomatisations of set
        theory concern the restrictions they place on this idea (known
        as "comprehension").
     
        {Zermelo Frankel set theory}, the most commonly used
        axiomatisation, gets round it by (in effect) saying that you
        can only use this principle to define subsets of existing
        sets.
     
        NBG (von Neumann-Bernays-Goedel) set theory sort of allows
        comprehension for all {formulae} without restriction, but
        distinguishes between two kinds of set, so that the sets
        produced by applying comprehension are only second-class sets.
        NBG is exactly as powerful as ZF, in the sense that any
        statement that can be formalised in both theories is a theorem
        of ZF if and only if it is a theorem of ZFC.
     
        MK (Morse-Kelley) set theory is a strengthened version of NBG,
        with a simpler axiom system.  It is strictly stronger than
        NBG, and it is possible that NBG might be consistent but MK
        inconsistent.
     
        {NF (http://math.boisestate.edu/~holmes/holmes/nf.html)} ("New
        Foundations"), a theory developed by Willard Van Orman Quine,
        places a very different restriction on comprehension: it only
        works when the formula describing the membership condition for
        your putative set is "stratified", which means that it could
        be made to make sense if you worked in a system where every
        set had a level attached to it, so that a level-n set could
        only be a member of sets of level n+1.  (This doesn't mean
        that there are actually levels attached to sets in NF).  NF is
        very different from ZF; for instance, in NF the universe is a
        set (which it isn't in ZF, because the whole point of ZF is
        that it forbids sets that are "too large"), and it can be
        proved that the {Axiom of Choice} is false in NF!
     
        ML ("Modern Logic") is to NF as NBG is to ZF.  (Its name
        derives from the title of the book in which Quine introduced
        an early, defective, form of it).  It is stronger than ZF (it
        can prove things that ZF can't), but if NF is consistent then
        ML is too.
     
        (2003-09-21)