mutually disjoint class (MutuallyDisjointClass)

A SetOrClass of Classes is a MutuallyDisjointClass just in case there exists nothing which is an instance of all of the instances of the original SetOrClass.

Ontology

SUMO / SET/CLASS-THEORY

Superclass(es)

entity

abstract

set or class

mutually disjoint class

Coordinate term(s)

class pairwise disjoint class set

Axioms (1)

if class is an instance of mutually disjoint class,
then for all inst1,inst2 holds: if inst1 is an instance of class and inst2 is an instance of inst1, then there exists class inst3 so that inst2 is not an instance of inst3

(=>
      (instance ?CLASS MutuallyDisjointClass)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?INST1))
                  (exists
                        (?INST3)
                        (and
                              (instance ?INST3 ?CLASS)
                              (not
                                    (instance ?INST2 ?INST3)))))))