Re: Coming soon -- new proof checking software

"Dan Christensen" <[EMAIL PROTECTED]> wrote in message news:<[EMAIL PROTECTED]>...

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

No, actually, if the set is infinite, YOU CAN'T.
It's just not intellectually doable.
For "most" of the available subsets, it requires
an infinite amount of information (and therefore of
effort).  For all of them in toto it's an even bigger
infinity.  Before you can have a set theory, you have
to have a logic.  If you are postulating that this is doable
then you are in 2nd (as opposed to 1st) order logic.

You really do sort of need to advertise that in advance.
What do you REALLY mean by "arbitrary"?  If you mean
"that subset where all the elements satisfy some arbitrary free-
variable expression", then that IS doable.  In ZF they call it
the axiom of separation (it separates any set into 2 subsets,
1 for which the free-variable-expression comes up false and
another for which it comes up true).

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

Again, even if it is an infinite number?  In that case, what
is  a number?

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

Unfortunately, if the set is infinite, you can do this in
more than 1 way.

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

You don't need the axiom of choice.  If 1. is true then
the axiom of choice is true.  You can't deny it.

> >
> 
> 
> I forgot one:  If x is a free variable expression, then x = x.
> 
> Dan