Re: Coming soon -- new proof checking software

[EMAIL PROTECTED] (George Greene) wrote in message news:<[EMAIL PROTECTED]>...
> "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.

Sorry, that IS what I mean.


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

With the Cartesian rule, as a shortcut, I prompt the user for the
number of dimensions (the order of the n-tuples to be used). I guess
it could also have been done recursively, adding an extra dimension
with each application of the rule. This seems a bit awkward though.

Again, this system was not meant to supplant ZF. It is a learning tool
with a number of such compromises to make it easier to use. I does,
however, seem to avoid the difficulties of niave set theory, and to be
applicable to a wide range of mathematical theory.


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

Do they not all produce the same 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.
> 
> 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 will have to think about that. It is not immediately obvious to me.
Anyway, the current version does not have AC.


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


Dan