Re: Coming soon -- new proof checking software

"G. Frege" <[EMAIL PROTECTED]> wrote in message
news:[EMAIL PROTECTED]
> On Sun, 30 Nov 2003 18:38:03 -0500, "Dan Christensen"
> <[EMAIL PROTECTED]> wrote:
>
> > >
> > > ...large body of research in non-well-founded set theory.
> > >
> >
> > How so? What difficulties has it presented? Russell's Paradox seems
easily
> > disposed of in my system.
> >
> Would be nice if you could post the axioms of your set theory.
>
[snip]

Roughly as follows:

1. You can select an arbitrary subset from any set.

2. You can form the Cartesian product of any number of sets.

3. You can construct the power set of any set.

4. Sets are equal if they contain the same elements.

5. If x and y are free variable expressions and x = y, then y can be
substituted for x in any other expression.

6. I define what functional notatation means in terms of ordered n-tuples
and equality.

A later version may include the Axiom of Choice.

Dan