Re: Coming soon -- new proof checking software

On Mon, 1 Dec 2003 01:22:21 -0500, "Dan Christensen"
<[EMAIL PROTECTED]> wrote:

I'll try a formalization. Please correct me if I got something wrong.

>
> 1. You can select an arbitrary subset from any set.
> 
        Az(Set z -> Ey(Set y & Ax(x e y <-> x e z & phi x)))

> 
> 4. Sets are equal if they contain the same elements.
> 

        AxAy(Set(x) & Set(y) -> (Az(z e x <-> z e y) -> x = y))

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

        Az(Set(z) -> Ey(Set y & Ax(x e y <-> x c z)).

>
> 2. You can form the Cartesian product of any number of sets.
>
        Ay_1...Ay_n(Set(y_1) & ... & Set(y_n) 
                    -> Ex(Set x &  x = y_1 x ... x y_n)). 
                                   ^^^^^^^^^^^^^^^^^^^^
        ok?                    [ "Simplified" formulation. ]

>
> 6. I define what functional notation means in terms of ordered n-tuples
> and equality.
> 
        ...

Now since the axioms "Empty Set", "Pairs", "Unions" and the "replacement
scheme" are not part of your system, it certainly would be nice if you
would show how to derive them from your system. The existence of the
empty set, pairs and unions (guaranteed by the related axioms) is
certainly a minimal requirement for any set theory. On the other hand,
we m a y leave out "replacement", we said.


-------------------


Actually [or usually] a rule of logic, isn't it? ("Substitution of
identities" -- Greeting George Greene! :-):
>
> 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))

Same with "reflexivity":
>
> If x is a free variable ..., then x = x.
>
        x = x.


F.