Re: Coming soon -- new proof checking software

"F. Fritsche" <[EMAIL PROTECTED]> wrote in message
news:[EMAIL PROTECTED]
> 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.
>

The empty set can be shown to be a subset of any given set. Just apply an
"impossible" selection criteria (e.g. ~ x = x).

Intersections and unions can be defined on the power set of any given set.
This requires a proof, of course. It is quite easy using the subset axiom.
The "axioms" for set complement and pairwise union and intersection are
built into my program (the Sets menu, Set Operations option:

` (left quote) is the set complement operator. && is pairwise intersection.
|| is pairwise union. I'm sorry if these are non-standard symbols, but I
wanted to be able to use the standard keyboard as much as possible. (I had
to give up, however, on epsilon, which is shift+2.) In addition to being
more convenient for the user -- after learning the notation -- it makes it
possible to send proofs by e-mail as relatively compact text (.txt) file
attachments.


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

Is this not what you mean by replacement?


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

Your formalizations are essentially correct, as I understand them.

Dan