Class Class-Partition

Arity: 1
Documentation:
A set of mutually disjoint classes. Disjointness of classes is a special case of disjointness of sets.

Notes:

  • Why not just use the set machinery?

    We want to localize the relationship between sets and classes to just a few axioms, so we use the instance-of machinery here.

Instance-Of: Class, Relation, Set
Range-Of: Subclass-Partition
Subclass-Of: Set


Slots:


Implication Axioms for Class-Partition:

(=> (Class-Partition ?Set-Of-Classes)
    (Forall (?C1 ?C2)
            (=> (And (Member ?C1 ?Set-Of-Classes)
                     (Member ?C2 ?Set-Of-Classes)
                     (Not (= ?C1 ?C2)))
                (Forall (?I)
                        (=> (Instance-Of ?I ?C1)
                            (Not (Instance-Of ?I ?C2)))))))

(=> (Class-Partition ?Set-Of-Classes)
    (Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C))))


Equivalence Axioms for Class-Partition:

(<=> (Class-Partition ?Set-Of-Classes)
     (And (Set ?Set-Of-Classes)
          (Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C)))
          (Forall (?C1 ?C2)
                  (=> (And (Member ?C1 ?Set-Of-Classes)
                           (Member ?C2 ?Set-Of-Classes)
                           (Not (= ?C1 ?C2)))
                      (Forall (?I)
                              (=> (Instance-Of ?I ?C1)
                                  (Not (Instance-Of ?I ?C2))))))))


Equivalence Axioms mentioning Class-Partition:

(<=> (Subclass-Partition ?C ?Class-Partition)
     (And (Class ?C)
          (Class-Partition ?Class-Partition)
          (Forall (?Subclass)
                  (=> (Member ?Subclass ?Class-Partition)
                      (Subclass-Of ?Subclass ?C)))))