Re: Coming soon -- new proof checking software

On Tue, 2 Dec 2003 10:46:06 -0500, "Dan Christensen"
<[EMAIL PROTECTED]> wrote:

> 
> The empty set can be shown to be a subset of any given set. Just apply an
> "impossible" selection criteria (e.g. ~ x = x).
> 
Sure. But in this case you need AT LEAST o n e given set. (Otherwise you
can't use the /axiom of subsets/.)
        
>
> ...unions can be defined on the power set of any given set.
>
Huh? What do you mean?

>
> It is quite easy using the subset axiom.
>
Please demonstrate.

>
> The "axiom" for [...] pairwise union [is] built into my program 
> (the Sets menu, Set Operations option:
> 
Ah. That's valuable information. What's with pairs?



"Substitution of identities" ...

> > >
> > > If x and y are free variable[s] and x = y, then y can be
> > > substituted for x in any other expression.
> > >
> > x = y -> (phi(x) -> phi(y))
> >
> 
> Is this not what you mean by replacement?
> 
No. "Replacement" is "set theoretic", and "Substitution of identities"
is part of "identity theory" (i.e. of the logical framework).


F.