Re: SUO: power classes
Hi Chris,
Let me explain my motivation and particular problem. I am defining several
ontologies, some large dealing with things like classes (large sets), large
graphs and categories and some small dealing with things like small
classifications, small spans and small hypergraphs. Now I have ended up with
the following (in hindsight, not surprising) characteristic:
The axiomatization for spans (and hypergraphs) is strictly
category-theoretic - in the axiomatization of spans all axioms are expressed
in terms of category-theoretic (in my approach, foundational) notions, such
as the composition and identity of large (class to class) functions or the
pullback of small sets, and no axioms use explicit logical KIF connectives
or quantification! This seems to be a hallmark of the ontologies in the
lower-level structure -- the ontologies for true categories (not
quasi-categories), whose object and morphism collections are classes (not
conglomerates). In addition, no axioms in the Span Ontology use explicit KIF
terms from the basic KIF ontology.
So this is the motivation. And indeed I currently have 98% of the axioms for
the Classification Ontology translated to purely category-theoretic terms. I
ran up against this power class problem in translating what Barwise et al
call the "fundamental condition for infomorphisms." There seemed to be
several ways to approach this, but essentially what I needed to do was to
define the inverse image of a binary relation along a function.
Suppose f : B -> A is a small function (between small sets). I wanted to
define the inverse image along f of the class of all small binary relations
whose first coordinate set is the small set A to the class of all binary
relations whose first coordinate set is the small set B (and second
coordinate small set remains fixed): if R \subset AxC then f*(R) \subset BxC
is define bf*(R)c when f(b)Rc. But I did not want to do this from scratch.
All my ontology formulations are suppose to be very incremental.
I have since defined a successful approach to this, but originally I wanted
to define the power function associated with a large binary relation: let R
is a large binary relation between two classes A and B, and let f : A ->
P(B) be the power function f(a) = {b \member B | aRb}. Is this function
between classes? Is P(B) a class?
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "Chris Menzel" <cmenzel@philebus.tamu.edu>
To: "Robert E. Kent" <rekent@ontologos.org>
Cc: "IEEE Standard Upper Ontology List" <standard-upper-ontology@ieee.org>
Sent: Saturday, May 05, 2001 7:12 PM
Subject: Re: SUO: power classes
> > In formulating axioms the Classification Ontology I have come across a
> > foundation question about the "power operator". I am following the
> > small-large approach to foundations as advocated by Adamek, Herrlich and
> > Strecker in section 0.2 of their book "Abstract and Concrete Categories"
> > 1990, ISBN: 0-471-60922-6, QA169.A3199 1989. The basic concepts are
sets,
> > classes and conglomerates. One axiom is that sets are closed under
power;
> > that is, if A is a set then P(A), the collection of all subsets of A, is
> > also a set. They seem to indicate that classes are not closed under
power,
> > since they give P(U), the power of the universe, as an example of an
> > illegitimate conglomerate (legitimate conglomerates correspond to
classes; a
> > conglomerate X is *legitimate* when there is a class Y and a surjection
Y ->
> > X).
> >
> > So, is it ill-advised to assume that classes are closed under power?
What
> > precisely is the problem here?
>
> If by P(S), for a class S, you mean the class of all subSETs of S, then
> there is no problem with closing classes under power. In fact, in pure set
> theory, the set of all subSETs of U is just U, since every set is a set of
> sets and hence a subset of U. But the assertion that P(U) is illegitimate
> suggests they are talking about defining P(S) for a class S to be the
> class of all subCLASSes of S, in which case one runs afoul of Cantor's
> theorem when S = U. (By Cantor's theorem P(S) is larger than S, for any
> S. (The proof would go through for classes no less than sets if P(S) is
> taken to be the class of all subclasses of S.) So P(U) is larger than U.
> But, like any class, P(U) is a subset of U, and hence no larger than U,
> contradiction.)
>
> -chris
>
> --
>
> Christopher Menzel # web: philebus.tamu.edu/~cmenzel
> Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
> College Station, TX 77843-4237 # vox: (979) 845-8764
>
>