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


(DEFINE-RELATION CONCEPTUALLY-DEPENDS-ON (?A ?B)
 "The proper ontological dependence between two classes; 
this is a 'de dicto' dependence."
 :DEF
 (AND (FORALL (?Z ?W) (=> (HOLDS-TRUE-2 ?A ?Z) (HOLDS-TRUE-2 ?B ?W)))
      (EXTRINSIC-STRUCTURING-RELATION ?A ?B)
      (META-THING ?A)
      (META-THING ?B)))
(DEFINE-RELATION FINE-PROPERLY-DEPENDS-ON (?A ?B)
 "The rigid ontological dependence, but excluding the 
trivial case of self-dependence, and in which the depender is external to the dependent."
 :DEF (AND (NOT (PART-OF ?B ?A)) (PROPERLY-DEPENDS-ON ?A ?B)))
(DEFINE-RELATION FINE-PROPERLY-NECESSARY-TO (?A ?B) :IFF-DEF
 (AND (= (INVERSE FINE-PROPERLY-DEPENDS-ON)
         FINE-PROPERLY-NECESSARY-TO)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE FINE-PROPERLY-NECESSARY-TO ENTITY)
      (DOMAIN FINE-PROPERLY-NECESSARY-TO ENTITY)))
(DEFINE-RELATION GENERICALLY-DEPENDS-ON (?A ?B)
 "The proper ontological dependence between an individual 
and a class; the next and this one are 'de re' dependences."
 :DEF
 (AND (=> (HOLDS-TRUE-2 ?B ?A) (HAS-EXISTENCE ?A TRUE))
      (EXTRINSIC-STRUCTURING-RELATION ?A ?B)
      (ENTITY ?A)
      (META-THING ?B)))
(DEFINE-RELATION HAS-EXISTENCE (?A ?B)
 "This is the predicative alternative for stating ontological 
existence, without admitting being as possible."
 :DEF (DEPENDENCE-PROPERTY ?A ?B))
(DEFINE-RELATION HAS-POSSIBILITY (?A ?B)
 "This is the predicative alternative for stating ontological 
existence, admitting being as possible."
 :DEF (DEPENDENCE-PROPERTY ?A ?B))
(DEFINE-RELATION ONTOLOGICALLY-DEPENDS-ON (?A ?B))
(DEFINE-RELATION PREDICATIVELY-DEPENDS-ON (?A ?B))
(DEFINE-RELATION PROPERLY-DEPENDS-ON (?A ?B)
 "The rigid ontological dependence, but excluding the 
trivial case of self-dependence."
 :DEF (AND (RIGIDLY-DEPENDS-ON ?A ?B) (DIFFERENT ?A ?B)))
(DEFINE-RELATION PROPERLY-NECESSARY-TO (?A ?B) :IFF-DEF
 (AND (= (INVERSE PROPERLY-DEPENDS-ON) PROPERLY-NECESSARY-TO)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE PROPERLY-NECESSARY-TO ENTITY)
      (DOMAIN PROPERLY-NECESSARY-TO ENTITY)))
(DEFINE-RELATION RIGIDLY-DEPENDS-ON (?A ?B)
 "The strongest proper ontological dependence: between 
individuals (Simons)."
 :DEF
 (AND (=> (HAS-EXISTENCE ?A TRUE) (HAS-EXISTENCE ?B TRUE))
      (DEPENDENCE-RELATION ?A ?B)))
(DEFINE-RELATION RIGIDLY-NECESSARY-TO (?A ?B) :IFF-DEF
 (= (INVERSE RIGIDLY-DEPENDS-ON) RIGIDLY-NECESSARY-TO))
(DEFINE-RELATION STRICTLY-DEPENDS-ON (?A ?B)
 "The proper ontological dependence, without 
postulating the necessity of existence for y (not rigid)."
 :DEF (AND (DEPENDENCE-RELATION ?A ?B) (DIFFERENT ?A ?B)))
(DEFINE-RELATION STRICTLY-NECESSARY-TO (?A ?B) :IFF-DEF
 (AND (= (INVERSE STRICTLY-DEPENDS-ON) STRICTLY-NECESSARY-TO)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE STRICTLY-NECESSARY-TO ENTITY)
      (DOMAIN STRICTLY-NECESSARY-TO ENTITY)))
(DEFINE-RELATION STRONGLY-DEPENDS-ON (?A ?B)
 "The proper ontological dependence, in which the depender 
is external to the dependent (Stumpf, Husserl)."
 :DEF (AND (NOT (PART-OF ?B ?A)) (STRICTLY-DEPENDS-ON ?A ?B)))
(DEFINE-RELATION STRONGLY-NECESSARY-TO (?A ?B) :IFF-DEF
 (AND (= (INVERSE STRONGLY-DEPENDS-ON) STRONGLY-NECESSARY-TO)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE STRONGLY-NECESSARY-TO ENTITY)
      (DOMAIN STRONGLY-NECESSARY-TO ENTITY)))
(DEFINE-RELATION _CONTINGENT (?A ?B) :DEF
 (DEPENDENCE-PROPERTY ?A ?B))