(define-theory metaontology (kif-sets frame-ontology))
(in-theory 'metaontology)

(DEFINE-CLASS CATEGORY (?SELF)
 "This is a meta-level predicate for distinguishing very 
general classes, which in the analytic philosophy literature are taken to be 'uncountable' 
(cf. Griffin, 1977: a part of something belonging to the class c belongs to c as well; 
in other terms, an instance of a category class is internally homogeneous). 
A problem is that such a description is applicable to 'mass' objects (a piece of 
gold, an amount of water, etc.) as well, which are not exactly very general in the 
common intuition.
Cognitive semantics provides us a criterion for further intuition: a category
class is (cognitively) reidentifiable by means of a single image-schema (container,
path, etc., cf. Mark Johnson, 1989), while masses are reidentified on the basis 
of material properties.
Another way for distinguishing masses from categories at meta-level is granularity (see theory:
layers): a mass has homogeneous parts as far as the same granularity (or an adjacent one)
is maintained: for example, a part of a piece of gold is gold until the atomic granularity, 
but not at sub-atomic granularity; a part of a food is the same food till molar granularity,
but not at molecular granularity, etc."
 :DEF (STRUCTURAL-CONCEPT ?SELF)
 :CONSTRAINTS
 (AND (THE-ARCHETYPE ?SELF CATEGORY)
      (FORALL (?HOMOG ?X ?Y)
       (=>
        (AND (ISA ?HOMOG ENTITY)
             (INSTANCE-OF ?X ?SELF)
             (INSTANCE-OF ?Y ?HOMOG)
             (PART-OF ?Y ?X))
        (IDENTITY ?SELF ?HOMOG)))))
(DEFINE-CLASS META-LEVEL-CATEGORY (?SELF)
 "In this library, meta-level-categories are 
neither structuring nor structural concepts, since they are used as meta-predicates 
(as well as 'structuring-concept' and 'structural-concept' themselves). In fact, the 
theory: metaontology is a representation ontology."
 :DEF (UNARY-RELATION ?SELF))
(DEFINE-CLASS REIFIED-PROPERTY (?SELF)
 "This is the meta-level predicate for 'non-rigid' classes of 
a theory (cf. Wiggins, 1980: within a given theory, if A is an instance of a !type class C 
in a conceivable situation s1, there can be a conceivable s2 temporally different from s1 in 
which A is not an instance of C). From a modellistic viewpoint, such predicate identifies the 
classes which are defined as a 'reification' of a property or of a domain or range of a  
relation: for example definitions made by means of 'named' lambda formulas. This is also 
useful for the reification of complex constraints, e.g. applications of a composition of 
relations of heterogeneous arity, applications of a disjunction of relational expressions, 
etc. By convention, reified-property predicate names begin with a * (star) to be easily 
distinguished from other kinds of monadic predicates."
 :DEF
 (AND (THE-ARCHETYPE ?SELF REIFIED-PROPERTY)
      (EXISTS ?SIT1
       (AND (SITUATION ?SIT1)
            (CONTEXT-OF ?SIT1 ?SELF)
            (FORALL ?X
             (=> (INSTANCE-OF ?X ?SELF)
              (EXISTS (?SIT2)
               (AND (SITUATION ?SIT2)
                    (CONTEXT-OF ?SIT2 ?SELF)
                    (CONTEXT-OF ?SIT2 ?X)
                    (DIFFERENT ?SIT2 ?SIT1)
                    (FOLLOWS ?SIT2 ?SIT1)
                    (EXISTS (?A)
                     (AND (NOT (INSTANCE-OF ?X ?SELF))
                          (HOLDS-AT ?SIT2 ?A)))))))))
      (STRUCTURAL-CONCEPT ?SELF)))
(DEFINE-CLASS REIFIED-ROLE (?SELF)
 "This is for reified-property classes which reify an 
actantial concept. It implements the common sense notion of 'role' (such as student, 
agent, etc.)."
 :DEF (REIFIED-PROPERTY ?SELF) :CONSTRAINTS
 (AND (THE-ARCHETYPE ?SELF REIFIED-PROPERTY)
      (FORALL ?X
       (=> (INSTANCE-OF ?X ?SELF)
        (EXISTS (?Y ?S)
         (AND (INSTANCE-OF ?Y ENTITY)
              (INSTANCE-OF ?S RELATION)
              (SUPERRELATIONS ?S ACTANTIAL-RELATION)
              (HOLDS-TRUE-3 ?S ?X ?Y)))))))
(DEFINE-CLASS STRUCTURAL-CONCEPT (?SELF)
 "The meta category including the concepts in any 
conceptualization, as opposed to 'structuring-concept', which is the meta category 
to which the dimensions which structure the concepts in any conceptualization belong 
(are instance of). In Loom, this includes the concepts (but not the properties)."
 :IFF-DEF
 (AND (META-LEVEL-CATEGORY ?SELF)
      (EXISTS (?A) (AND (ARCHETYPE ?SELF ?A) (UNARY-RELATION ?A)))
      (VALUE-TYPE ?SELF ARCHETYPE INCOHERENT)
      (VALUE-TYPE ?SELF ARCHETYPE INCOHERENT)))
(DEFINE-CLASS STRUCTURING-CONCEPT (?SELF)
 "The meta category to which the dimensions which 
structure the concepts in any conceptualization belong (are instance of), as opposed 
to structural-concept, which is the meta category which includes the concepts in any 
conceptualization. In Loom, this includes both relations and properties, but what
is meant to be modelled as property is explained in a dedicated annotation."
 :IFF-DEF
 (AND (META-LEVEL-CATEGORY ?SELF)
      (EXISTS (?A)
              (AND (ARCHETYPE ?SELF ?A) (OR (RELATION ?A) (PROPERTY ?A))))))
(DEFINE-CLASS TERNARY (?SELF)
:IFF-DEF
 (AND (RELATION ?SELF)
      (ARITY ?SELF 3)
      (FORALL (?A ?B)
       (=> (AND (ARITY ?SELF ?A) (ARITY ?SELF ?B)) (= ?A ?B)))))
;;;:AXIOM-DEF
;;; (ARITY TERNARY 3))
(DEFINE-CLASS TYPE (?SELF)
 "This is the meta-level predicate for the 'rigid' classes of 
a theory (cf. Wiggins, 1980: within a given theory, if A is an instance of a !type class C 
in a conceivable situation s1, there is no conceivable s2 different from s1 in which A is 
not an instance of C). A type class is also countable (there is a part of something belonging to
the class c which does not belong to c as well; in other terms, an instance of a !type class
can be internally dishomogeneous). The first axiom implements rigidity, while the 
second implements countability."
 :DEF
 (AND (THE-ARCHETYPE ?SELF TYPE)
      (EXISTS (?SIT1)
       (AND (SITUATION ?SIT1)
            (CONTEXT-OF ?SIT1 ?SELF)
            (FORALL (?X)
             (=> (INSTANCE-OF ?X ?SELF)
              (NOT
               (EXISTS (?SIT2)
                (AND (SITUATION ?SIT2)
                     (CONTEXT-OF ?SIT2 ?SELF)
                     (CONTEXT-OF ?SIT2 ?X)
                     (DIFFERENT ?SIT2 ?SIT1)
                     (EXISTS (?A)
                      (AND (NOT (INSTANCE-OF ?X ?SELF))
                           (HOLDS-AT ?SIT2 ?A))))))))))
      (FORALL (?Y)
       (=> (INSTANCE-OF ?Y ?SELF)
        (EXISTS (?Z ?DISHOMOG)
         (AND (INSTANCE-OF ?Z ?DISHOMOG)
              (PART-OF ?Z ?Y)
              (CONCEPTUALLY-DIFFERENT ?SELF ?DISHOMOG)))))
      (STRUCTURAL-CONCEPT ?SELF)))