Re: [KIF] Re: SUO: tuples
On Sat, Jul 06, 2002 at 09:43:43PM -0400, John Sowa wrote:
> 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.
It actually does a rather better job than the ramified type theory of
the Principia; see esp the work of Sobocinski and his Notre Dame
students.
> And functions can also be defined without assuming set theory.
Or, as I was arguing, you needn't define them (i.e., identify them with
certain constructions) in any foundational theory; you can take them as
primitive (albeit with some implicit or explicit understanding of their
properties).
> 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".
As I noted, functions needn't be represented as sets of ordered pairs,
even if one is using set theory. (Indeed, in von Neumann's original
theory that turned into VNBG set theory, functions were the primitive
objects.)
> Bottom line: It is not necessary to assume set theory in order to
> make sequences into first-class objects.
Nor does it follow that the use of set theory require that one represent
them as sets.
> 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.
You've lost me here, John. You seem to be suggesting that the
distinction between seq variables and ordinary variables in CL is some
sort of artifact foisted upon us by our use of set theory in the
metatheory, and hence one that we are better off clobbering. By no
means. Seq variables are there because they increase the expressive
power of the language in useful ways. They are there by choice.
As for doing without the uncountable, well, there is no law that sez one
has to use the power set axiom if one is going to use set theory. And
indeed, the metatheory for CL does not presuppose it (though of course
we need the axiom of infinite to get the finite ordinals -- but without
power set, that axiom only guarantees a denumerably infinite set).
Bottom line: Metatheoretic frameworks are chosen to do a certain job.
Ideological considerations (a faint redolence of which I detect in your
message) are irrelevant. For our purposes, in addition to its being
extremely well known and understood, set theory does its job very
capably. There is absolutely no non-ideological reason to move to a
different framework.
-chris