Re: [KIF] Re: SUO: tuples
Chris,
As you know, I have never been quite happy with set theory as
the "standard" way of representing mathematics. Of course, I
recognize that set theory is a widely used method for representing
the foundations of mathematics, but it is by no means the only
(or even the best) method.
CM> ... And that's what sequences would be if one were hung up on
> representing everything in pure set theory. But there's no reason
> why one couldn't think of "sequence" as a metatheoretic primitive.
> I reckon that way of looking at things would be more amenable to
> the abstract, category theoretic approach of IFF.
Lesniewski developed an alternative foundation for mathematics (at
least the same subset that Alfie and Bertie supported) using mereology
as the theory of collections. That gives you a much weaker foundation
that does not support Cantor's hierarchy, but it provides sufficient
material for introducing Peano's axioms. It also lets you define
ordered pairs and functions like CAR, CDR, and CONS, if you like.
And functions can also be defined without assuming set theory.
That is, in fact, the whole point of category theory: arrows are
primitives, which can be interpreted as functions, if you like,
but they are not defined as "sets of ordered pairs".
In that formulation, a sequence could be defined as an arrow
from the collection integers to any other collection of objects.
The only thing that's missing is the option of defining an operator
that gives you a "power set", which would take you into uncountable
realms.
Bottom line: It is not necessary to assume set theory in order
to make sequences into first-class objects. Therefore, it is
possible to eliminate the need for a distinction between
sequence variables and any other kind of variables without
introducing any axioms whose standard model is uncountable.
John