[FOM] geometry and non-well-founded sets

[Dana Scott]

Robert Black <Mongre at gmx.de> asked:

> Someone once said to me (and it sounds true) that using a
> non-well-founded set theory you could so axiomatize projective
> geometry that *both* a line is identified with the set of points
> lying on it *and* a point is identified with the pencil of lines
> passing through it. Can anyone give me a reference for somewhere this
> is actually done?

It is not too hard.  Set theory with urelemente (= atoms) is familiar.
One can redefine membership so that an atom u = {u} under the new
membership convention, and in this non-well-founded universe, this
equation DEFINES the atoms.

Equally well start with any crazy proto-set-structure <U, E, Q>, where
U is the "universe", E is "membership", Q is an equivalence relation,
and the "axioms" (which are not very powerful) are:

(Ext)  (all x, y)[(all z)[ z E x <==> z E y ] <==> x Q y ]

(Id)  (all x, y, z)[ x Q y /\ x E z ==> y E z ]

The relation Q then behaves like identity (but does not have to be
the real identity relation), and the elements of U behave like (some)
of the subsets of U.

We can now pass to the powerset P(U) of U and note that E could have
been thought of as a mapping  E*: U --> P(U) by the definition:

	E*(x) = {z in U | z E x}.

Clearly, x Q y <==> E*(x) = E*(y).

Next, for X, Y in P(U), define

	X Q' Y <==> (all x in X)(exists y in Y). x Q y /\
                     (all y in Y)(exists x in X). x Q y
and
	X E' Y <==> (exists x in U)[ X Q' E*(x) /\ x in Y ]

I think it is easy to prove that <P(U), E', Q'> satisfies
the axioms (Ext) and (Id) and the mapping E* is a substructure
embedding.  (Someone should check this, please.)

Continuing in this way, we get a tower

	U, P(U), P(P(U)), P(P(P(U))), ...

of bigger and bigger powersets.  As membership structures
each is embedded into the next.  The direct limit satisfies
the Zermelo axioms (without infinity or well-foundedness).
Keep iterating the powerset operation in this way, going
through all ordinals, and you will have a model for
ZFC (without well-foundedness).

Now, if U is the union of the points and lines of an
abstract model of projective geometry, then define Q
as identity, and define x E y as either the point x is
on the line y or the line x passes through the point y.
(The sets of points and lines are disjoint.)  Because
every line has a point and every point is on some line,
the axioms (Ext) and (Id) hold.

Does this this make sense?