Regaining the Square of Opposition in Formal Ontology Development

Use of formal ontologies is becoming widespread in information systems. Forerunners of formal ontologies are scientific classification systems such as the Linnaean biological ones. Unlike biological classifications modern formal ontologies are often non-hierarchical. A formal ontology in its basic form simply specifies all direct inclusion relationships between a finite repertoire of classes. Individuals may be conceived of as singleton classes. An assertion "P sub Q" states that class P is an immediate subclass of Q. These given relationships are often rendered as directed graphs. The subclass relationship induces a partial order relation corresponding to the relationship "all P are Q" in the square of opposition. Accordingly, so far, formal ontologies provide only assertions of the form "all P are Q". However, it is our contention that the three other assertion forms in the square of opposition come about implicitly by appropriate, often tacitly assumed default conventions as to be explained. Assume existential import so that all classes are considered non-empty, implying that there is no empty null class. Defaults: 1) Overlapping (i.e. non-disjoint) classes, viz. "some P are Q", has at least one common subclass. 2) Dually, classes are disjoint ("no P is Q") if they do not have a common subclass. 3) The assertion form "some P are not Q" is -- analogously to class overlap -- achieved by requiring that there be a subclass of P which is disjoint with Q. More radically this assertion may be held simply in the case that "all P are Q" does not hold. These default rules are routinely adopted in ontology development without mentioning. Appealing to these conventions, the 4 sentence forms in the square are effectively made at disposal. We discuss a first order metalogical formalization of the 4 sentence forms with classes reified as individual constants elucidating the logical relationships between the sentence forms. Our formalization appeals to non-provability. Non-provability incurs non-monotonicity, implying that extension of an ontology with additional subclass relationships may call for 86 retraction of derived square of opposition relationships. This reflects the crucial distinction between the closed world assumption (CWA) and the open world assumption (OWA).