Need of exhaustiveDecomposition and disjointDecomposition axioms

[nordlow]

Aren't the axioms

(=>
   (disjointDecomposition @ROW)
   (=>
      (inList ?ELEMENT (ListFn @ROW))
      (instance ?ELEMENT Class)))

(=>
   (exhaustiveDecomposition @ROW)
   (=>
      (inList ?ELEMENT (ListFn @ROW))
      (instance ?ELEMENT Class)))

redundant with

(instance disjointDecomposition VariableArityRelation)
(domain disjointDecomposition 1 Class)
(domain disjointDecomposition 2 Class)

(instance exhaustiveDecomposition VariableArityRelation)
(domain exhaustiveDecomposition 1 Class)
(domain exhaustiveDecomposition 2 Class)

?

[apease]

For a VariableArityRelation we need to define the types of the arguments. That's what these axioms do.

[nordlow]

I see. Thanks.

[arademaker]

This is related to #173 and #181. In particular, note that these axioms may pose a problem to the ontology.

We are dealing with two types of 'typing': 1) post-typing a term, and 2) constraint on terms.

Case 1: the axioms that were cited by @nordlow. They basically say that terms used as arguments of these symbols are of type Class.

Case 2: see related issues. The FOL interpretation of SUMO, given by the transformation KIF to TPTP/FOL, add restrictions on the possible types for axioms like

(=>
 (exhaustiveDecomposition ?CLASS @ROW)
 (forall (?OBJ)
	 (=>
          (instance ?OBJ ?CLASS)
          (exists (?ITEM)
		  (and
		   (inList ?ITEM (ListFn @ROW))
		   (instance ?OBJ ?ITEM))))))

or

(=>
   (disjointDecomposition ?CLASS @ROW)
   (forall (?ITEM1 ?ITEM2)
      (=>
         (and
            (inList ?ITEM1 (ListFn @ROW))
            (inList ?ITEM2 (ListFn @ROW))
            (not (equal ?ITEM1 ?ITEM2)))
         (disjoint ?ITEM1 ?ITEM2))))

Both axioms, once transformed to TPTP/FOL, would result in a list of axioms such as:

(forall (?ROW1 ?ROW0 ?CLASS ?ROW2)
 (forall (?OBJ)
  (exists (?ITEM)
   (and (instance ?ITEM SetOrClass)
    (=> (instance ?OBJ Entity)
     (=>
      (and (instance ?CLASS SetOrClass) (instance ?CLASS Class)
       (instance ?ROW1 Class) (instance ?ROW1 Entity) (instance ?ROW0 Class)
       (instance ?ROW0 Entity) (instance ?ROW2 Entity))
      (=> (exhaustiveDecomposition3 ?CLASS ?ROW0 ?ROW1)
       (=> (instance ?OBJ ?CLASS)
        (and (inList ?ITEM (ListFn3 ?ROW0 ?ROW1 ?ROW2))
         (instance ?OBJ ?ITEM))))))))))

IMHO, I believe that considering case 1 and case 2, we would end up with α → β → α, which is a tautology. A tautology in the ontology is useless and does not help define the desire interpretations of exhaustiveDecomposition, right?