Re: Coming soon -- new proof checking software

"G. Frege" <[EMAIL PROTECTED]> wrote in message
news:[EMAIL PROTECTED]
> 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/.)

True. Is that a problem?


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

Let p be the power set of s. Let x and y be elements of p. Then we can
construct a subset of s, selecting those elements that are in both x and y.
That subset would be an element of p and the union of x and y.


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

Pairwise union is the union of two sets. As distinguished from the arbitrary
union of a set of sets. Perhaps I am not using the standard terminology?


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

Can you give me an example of each?

Dan