Re: Coming soon -- new proof checking software

"G. Frege" <[EMAIL PROTECTED]> wrote in message
news:[EMAIL PROTECTED]
> On Mon, 01 Dec 2003 07:55:37 +0100, G. Frege <[EMAIL PROTECTED]> wrote:
>
> > > >
> > > > Set(y) =df Ex(x e y) v y = 0.
> > > >
> > >
> > > How is it used?
> > >
> > We may use it for our formulation of "extensionality" in our theory:
> >
> > Set(a) & Set(b) -> (Ax(x e a <-> x e b) -> a = b).
> >
> > Otherwise there would only be ONE "Urelement". Since for any urelement u
> > we have Ax(x !e u). (Urelemente/individuals do not have any elements.)
> >
>
> Example. Assume that you want to treat the natural numbers as
> "Urements", i.e. not as sets but just as "individuals" (!= 0)
> with
>
> ~Ex(x e n)    [for any number n].
>
> With other words, we have
>
> An(n e N -> ~Set(n)). (*)
>
> Now we define 2 := next(1). Then we can derive from the Peano axioms
> that 1 != 2 (and 1,2 e N). Right.
>
> Now without the conjunction "Set(a) & Set(b)" in the antecedent of our
> axiom of extensionality, we would just have:
>
> Ax(x e 1 <-> x e 2) -> 1 = 2. (**)
>

You raise a VERY interesting point. Nowhere, however, do I say that Set(1)
or Set(2). I don't think you could then prove that  x e 1 <=> x e 2 for any
any x, since you can't prove or disprove that anything is an element of 1
(or 2). You would then never arrive at 1 = 2.

It seems my set predicate is really indespensible after all! I was using
more for clarity than anything else.


> And since we know that 1,2 e N, we would get from (*) and the definition
> of "Set()" that ~Ex(x e 1) and ~Ex(x e 2), or Ax~(x e 1) and Ax~(x e 2).
> But this means Ax(~(x e 1) <-> ~(x e 2)), or Ax(x e 1 <-> x e 2). Hence
> we get 1 = 2 from (**). Contradiction.
>
> That's why the USAGE of "Set()" actually is useful IF we allow for
> "Urelemente" (individuals that don't have any elements - not 0).
>

Do you really need a urelement predicate? From the above, it seems the set
predicate alone would do.

Dan