WikiDiscuss

---

wrote:

> --- Jorge Llambías <jjllambias@gmail.com>
> wrote:

> >
> > > > It would be nice to have the foundation
> > theses
> > > > expressed formally.
> > > > I'm not quite sure how that would go.
> > >
> > > How much more formal do you want than that
> > every
> > > bunch breaks down without remainder (or
> loss)
> > > into individuals? I even wrote it out in
> > > quasi-formal language and will — when I
> get
> > a
> > > symbolism I am comfortable with — do it
> > again in
> > > that formalism. What is obscure here?
> >
> > It's not exactly obscure, I can intuitively
> > understand
> > pretty well what it means. But I see nothing
>

> close to
> a formalization (of that particular thesis)
> yet.

<<As you are fond of saying in similar
situations,
what exactly do you want? I hope that, as I do,
you will give a fairly precise answer.

I gather that the point is that there is no
thesis that says directly "Every bunch breaks
down without remainder into individuals" although
(for finite bunches only, admittedly)the
foundation thesis (what I am calling ...) does
amount to that by induction. But even that
presupposes something to induce on and the
symbolism does not yet have that — the depth (or
cardinality) of a bunch. As noted, we could go
over to the corresponding sets and work it out
there but it would be nicer not to have to use
that apparatus. I have a few variant systems
which look promising for getting this point
across (and, if worse comes to worst, I can
always check out the various systems that batches
represent to see how they do it.)>>

And there is at a very simple level
Ax:x in a x in b => a in b
whence
Ax: x in ax in b & Ay: y in b y in a => a = b

This still may not be totally explicit, but it
does say that all that counts are individuals (if
there are other things they are wholly determined
by the indivuals and we have no other things
offered so far. I suppose we could have an array
of functions, one for each number such that, for
a bunch with n individual members, fn of those
members is also a member (and indeed, to really
work, fi for each i membered subunch). The
functions don't need ever make a difference but
they would mean that technically bunches don't
decompose into individuals without remainder -
not even the bunches called individuals,
apparently. It may be, of course, that what I
called foundations prevents that, since if we
take one individual out (even with its f1) what
remains would not be a bunch in these terms since
it would contain fns for subunches which are no
longer in it. Is that enough?