Re: Coming soon -- new proof checking software

On Wed, 3 Dec 2003 00:54:43 -0500, "Dan Christensen"
<[EMAIL PROTECTED]> wrote:

(Existence of at least one set)

> >
> > ...you need AT LEAST o n e given set. (Otherwise you can't use the 
> > /axiom of subsets/.)
> >
> True. Is that a problem?
> 
Huh? Actually it would be rather "nice" if your "system" would ensure
the existence of at least one set. :-)


(Unions)

> 
> 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.
> 
Huh??? I asked for a demonstration, and not for complete nonsense. 


(Pairs)

> 
> Pairwise union is the union of two sets.
>
Huh? You are confusing the /union of sets/ with a /pair/ consisting of
elements.

Given a,b the set {a,b} is a (unordered) pair, consisting of the
elements a and b.


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

"Replacement"

        Google for it.


F.