set or class (SetOrClass)

The SetOrClass of Sets and Classes, i.e. any instance of Abstract that has elements or instances.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

entity

abstract

set or class

Subclass(es)

class set pairwise disjoint class mutually disjoint class

Coordinate term(s)

attribute graph graph element proposition quantity relation

Constrains relations

cardinality fn complement fn generalized intersection fn generalized union fn intersection fn kappa fn power set fn relative complement fn union fn closed on disjoint domain domain subclass equivalence relation on instance irreflexive on partial ordering on range range subclass reflexive on subclass total ordering on trichotomizing on

Axioms (4)

subclass is a subclass of class if and only if

subclass is an instance of set or class
class is an instance of set or class
for all inst holds: if inst is an instance of subclass, then inst is an instance of class

(<=>
      (subclass ?SUBCLASS ?CLASS)
      (and
            (instance ?SUBCLASS SetOrClass)
            (instance ?CLASS SetOrClass)
            (forall
                  (?INST)
                  (=>
                        (instance ?INST ?SUBCLASS)
                        (instance ?INST ?CLASS)))))

class1 is disjoint from class2 if and only if

class1 is an instance of set or class
class2 is an instance of set or class
for all inst holds: inst is not an instance of class1 or inst is not an instance of class2

(<=>
      (disjoint ?CLASS1 ?CLASS2)
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass)
            (forall
                  (?INST)
                  (not
                        (and
                              (instance ?INST ?CLASS1)
                              (instance ?INST ?CLASS2))))))

set or class is exhaustively partitioned into set,class.

(partition SetOrClass Set Class)

If class1 is an instance of set or class and class2 is an instance of set or class, then "the difference between class1 and class2" is equal to "the union of class1 and "the complement of class2"".

(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))