Re: The definition of finite set

On Mar 8, 10:43 pm, Zaljo...@xxxxxxxxx wrote:
There are many definition of 'finite set'.

However I shall come with the following definition:

Oh, let's call this "z-finite", seeing as the term "finite" already
has a meaning.

Define: y<<x <-> [y<x & ~Ez (y<z<x)]

Are x and y cardinals? What does "y<x" mean for sets x and y?

'<< ' is read as 'immediatly smaller than'

Define:

x is finite  iff  [ card(x) = 0  or
(exists y (y << card(x)) and
for all y ((y < card(x) and y neq 0) implies exists z( z << y)))]

Using the conventional notation in this usenet:

x is finite<->[|x|=0 v (Ey(y<<|x|) & Ay((y<|x| & ~y=0)->Ez(z<<y)))].

Using my alternative notation:

x is finite <-> [|x|=0 || (/y(y<<|x|) & \y((y<|x| & ~y=0)->/
z(z<<y)))].

It's probably just my poor reading skills, but I find your definition
incomprehensible, mainly because I can't figure out whether your
variables are supposed to range over sets or cardinals. I'm going to
*guess* that you mean something like this:

A cardinal x is z-finite iff every nonzero cardinal, which is less
than or equal to x, has an immediate predecessor.

Now the question is the following: Is this definition equivalent to
Dedekind definition of 'finite set'?

I'm not sure about *your* definition, but my interpretation above is
trivially equivalent to "x is a Dedekind-finite cardinal". The trivial
argument does not use Choice or Regularity. If x is a Dedekind-finite
cardinal, then any cardinal y which is less than or equal to x is also
Dedekind-finite; if y is not zero, then y has an immediate
predecessor, namely y-1, the cardinality of a set obtained by removing
one element from a set of cardinality y. On the other hand, if x is
*not* Dedekind-finite, then the cardinal aleph_0 is less than or equal
to x; aleph_0 is a nonzero cardinal with no immediate predecessor.


.