Re: Coming soon -- new proof checking software

Dan Christensen wrote:

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

How about replacement? Can you prove in your system that given a set A 
and a function formula F, the image of A under F, i.e. F[A], is a set? 
Without this axiom much of the theory of ordinal numbers fails to get 
off the ground.

--
Aatu Koskensilta ([EMAIL PROTECTED])

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus