Function RELATION-UNIVERSE

Slots on this function:

Documentation:
A relation-universe of a relation of any arity is a class from which is drawn every item in every tuple of the relation. Like EXACT-DOMAIN, it is exactly those items and no other. Thus, to state that the universe of a relation is covered by some class, one can state that the relation-universe is a subclass of the covering class.
Instance-Of: Function
Arity: 2
Domain: Relation
Range: Class

Equivalence Axioms:

(<=> (Relation-Universe ?Relation)
     (And (Relation ?Relation)
          (Class ?Type-Class)
          (Forall (?X)
                  (<=> (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (Item ?X ?Tuple)))
                       (Instance-Of ?X ?Type-Class)))))

Other Related Axioms:

(=> (Relation-Universe $X $Y) (Class $Y))

(=> (Relation-Universe $X $Y) (Relation $X))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Forall (?X)
            (<=> (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (Item ?X ?Tuple)))
                 (Instance-Of ?X ?Type-Class))))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Class ?Type-Class))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Relation ?Relation))

Notes: