[FOM] A ... cute? ... axiomatic system

[A.P. Hazen]

    In the course of discussing some very weak set theories in
correspondence with John Burgess, I notice a way of describing models that
seemed to have wider applicability.  Herewith a description of a system of
axiomatic set theory which SUPERFICIALLY seems very strong (but which I
suspect offers few advantages in practice over the usual one).  I suspect
it has been discovered before: hence the question at the end.  (A: axioms,
B: model, C: proposed name, D: QUESTION)
-
	(A) Language: the standard language of (First-Order) set theory
with an additional monadic predicate, G.  (I'm 90% sure this is definable,
but formulating the axioms without it would be LOTS less perspicuous.)
	Axioms: --All the axioms of ZFC **restricted to G sets,** plus
      ---Every set has a complement
      ---Pairs of arbitrary sets exist
      ---FINITE unions always exist
      ---Replacement scheme generalized to: the image of any G set under
any definable function exists

	(B) Models: Every set in the (Well-Founded) ZF universe is
"depicted" by a well founded tree whose nodes represent the sets in its
transitive closure-- the root node represents the set in question, and the
successors of a given node represent members of the set represented by the
given node.
	The sets in a model of the axioms given are similarly depicted by
well-founded trees with COLORED nodes, using two colors.  The successors of
a GREEN node represent its members (as in the ZF case), but the successors
of a RED node represent its NON-members.
	Membership in the model is defined by cases (x is a member of y  iff
(i) the  root node of x is a successor of the root of y, y having a green
root, or (ii) the root node of x is NOT a successor of the root of y, y
having a red root).  The extension of G comprises those sets represented by
trees in which EVERY node is green.

	(C) Proposed name: if this system doesn't already have a name in
the literature, I propose UDZF, for Up-and-Down ZF.

	(D) I suspect this is closely related to the system of set theory
with a universal set proposed by Church in 1974, but the one time I looked
at Church's paper I found the presentation of the technical details...
detailed and technical (Grin!).  Enough people on the FoM forum are
interested in set theories with universal sets that I'm sure someone can
tell me what the relation of UDZF and Church's system is.

--
Allen Hazen
Philosophy Department
University of Melbourne