(define-theory Topology (Mereology))

(in-theory 'Topology)

(DEFINE-FUNCTION BOUNDARY (?A) :-> ?B :DEF
 (TOPOLOGICAL-RELATION ?A ?B) :AXIOM-DEF (FUNCTION BOUNDARY))
(DEFINE-RELATION CONNECTED (?A ?B)
 "Here connection is done as primitive; some prefer 
to derive it from mereology (early Whitehead), some the opposite (late Whitehead, 
Clarke). In agreement with Varzi (and Tarski), we keep both theories as 
independent modules."
 :DEF (TOPOLOGICAL-RELATION ?A ?B))
(DEFINE-RELATION EXTERNALLY-CONNECTED (?A ?B)
 "This is for two objects sharing a boundary.
Using a negation of topo-overlaps in the definition would create an incoherence 
when defining 'true-part', since topo-overlaps is a composition of t-part and
its inverse, thus t-part would actually be negated, while it is used positively
in the definition of true-part. For this reason, 'common-part' from mereology
is used in place of topo-overlaps.
For naive external connection, see 'touches'. 
(AG) at the moment I am uncertain about the relevance of this issue for
general mereo-topology."
 :IFF-DEF
 (AND (NOT (COMMON-PART ?A ?B))
      (EXISTS (?C ?D)
       (AND (BOUNDARY ?B ?D) (BOUNDARY ?A ?C) (CONNECTED ?C ?D)))
      (CONNECTED ?A ?B)))
(DEFINE-FUNCTION INTERIOR (?A) :-> ?B :DEF
 (AND (TRUE-PART-OF ?B ?A)
      (NOT (EXISTS ?Z (AND (PART-OF ?Z ?A) (NOT (PART-OF ?Z ?B)))))
      (TOPOLOGICAL-RELATION ?A ?B)
      (LOCALIZED-ENTITY ?A)
      (REGION ?B))
 :AXIOM-DEF (FUNCTION INTERIOR))
(DEFINE-RELATION INTERIOR-OF (?A ?B) :IFF-DEF
 (= (INVERSE INTERIOR) INTERIOR-OF))
(DEFINE-RELATION INTERMEDIATE-CONTACT (?A ?B)
 "An object and its complement have a so-called 
'intermediate' contact: only their complements are connected. Under granularity 
refinement ('microscopization') this relation may not be defeasible."
 :DEF
 (AND (EXISTS (?C) (AND (T-COMPLEMENT ?A ?C) (IDENTITY ?C ?B)))
      (NOT (CONNECTED ?A ?B))
      (EXISTS (?D ?E)
       (AND (T-COMPLEMENT ?B ?E) (T-COMPLEMENT ?A ?D) (CONNECTED ?D ?E)))
      (TOPOLOGICAL-RELATION ?A ?B)
      (LOCALIZED-ENTITY ?A)
      (LOCALIZED-ENTITY ?B)))
(DEFINE-RELATION IS-BOUNDARY-OF (?A ?B) :IFF-DEF
 (= (INVERSE BOUNDARY) IS-BOUNDARY-OF))
(DEFINE-RELATION IS-NEIGHBORHOOD-OF (?A ?B) :IFF-DEF
 (= (INVERSE NEIGHBORHOOD) IS-NEIGHBORHOOD-OF))
(DEFINE-RELATION IS-T-COMPLEMENT-OF (?A ?B) :IFF-DEF
 (= (INVERSE T-COMPLEMENT) IS-T-COMPLEMENT-OF))
(DEFINE-FUNCTION NEIGHBORHOOD (?A) :-> ?B
 "x has a neighborhood y when x is part of 
the interior of y, which is part of any interior x is part of.
This function is not very useful without an account of regions, which states
the fundamental ontological distincion between objects and regions where
objects are localized. See also theory:positions."
 :DEF
 (AND (EXISTS (?C) (AND (INTERIOR ?B ?C) (PART-OF ?A ?C)))
      (FORALL ?Z
       (=> (EXISTS (?D) (AND (INTERIOR ?Z ?D) (PART-OF ?A ?D)))
        (PART-OF ?B ?Z)))
      (TOPOLOGICAL-RELATION ?A ?B))
 :AXIOM-DEF (FUNCTION NEIGHBORHOOD))
(DEFINE-RELATION NON-TRUE-PART (?A ?B) :IFF-DEF
 (AND (= (INVERSE NON-TRUE-PART-OF) NON-TRUE-PART)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE NON-TRUE-PART ENTITY)
      (DOMAIN NON-TRUE-PART ENTITY)))
(DEFINE-RELATION NON-TRUE-PART-OF (?A ?B)
 "This is for internal parts, not sharing their 
whole's boundary."
 :DEF
 (AND (NOT (EXISTS (?C ?D)
            (AND (BOUNDARY ?B ?D) (BOUNDARY ?A ?C) (CONNECTED ?C ?D))))
      (PART-OF ?A ?B)))
(DEFINE-FUNCTION T-COMPLEMENT (?A) :-> ?B :DEF
 (TOPOLOGICAL-RELATION ?A ?B) :AXIOM-DEF (FUNCTION T-COMPLEMENT))
(DEFINE-RELATION TOPOLOGICAL-OVERLAPS (?A ?B))
(DEFINE-RELATION TOPOLOGICAL-PART (?A ?B))
(DEFINE-RELATION TOPOLOGICAL-PART-OF (?A ?B))
(DEFINE-RELATION TOPOLOGICAL-PROPER-PART-OF (?A ?B))
(DEFINE-RELATION TOUCHED-BY (?A ?B) :IFF-DEF
 (= (INVERSE TOUCHES) TOUCHED-BY))
(DEFINE-RELATION TOUCHES (?A ?B)
 "This is for naive external connection, which
does not imply symmetricity, usually for granularity differences or morphological
heterogeneity."
 :DEF
 (AND (EXISTS (?C ?D)
       (AND (BOUNDARY ?B ?D) (BOUNDARY ?A ?C) (CONNECTED ?C ?D)))
      (TOPOLOGICAL-RELATION ?A ?B)))
(DEFINE-RELATION TRUE-PART (?A ?B) :IFF-DEF
 (AND (= (INVERSE TRUE-PART-OF) TRUE-PART) (ENTITY ?A) (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE TRUE-PART ENTITY)
      (DOMAIN TRUE-PART ENTITY)))
(DEFINE-RELATION TRUE-PART-OF (?A ?B)
 "This is for parts sharing their whole's boundary." :DEF
 (AND (EXISTS (?C ?D)
       (AND (BOUNDARY ?B ?D) (BOUNDARY ?A ?C) (CONNECTED ?C ?D)))
      (PART ?A ?B)))
(DEFINE-RELATION WEAK-CONTACT (?A ?B)
 "Two objects x and y have weak contact when their 
complements are not connected and y is connected to the complement of any interior 
which x is part of. Granularity refinement ('microscopization') eliminates weak 
contact relations, while this does not happen with external connection, which 
could be renamed 'strong-contact'."
 :DEF
 (AND (NOT (EXISTS (?C ?D)
            (AND (T-COMPLEMENT ?B ?D) (T-COMPLEMENT ?A ?C) (CONNECTED ?C ?D))))
      (FORALL ?Z
       (=> (EXISTS (?E) (AND (INTERIOR ?Z ?E) (PART-OF ?A ?E)))
        (EXISTS (?F) (AND (T-COMPLEMENT ?Z ?F) (CONNECTED ?F ?B)))))
      (TOPOLOGICAL-RELATION ?A ?B)))
(DEFINE-RELATION _CLOSED (?A ?B) :DEF
 (AND (NOT (EXISTS (?C ?D)
            (AND (T-COMPLEMENT ?A ?D) (INTERIOR ?A ?C) (CONNECTED ?C ?D))))
      (TOPOLOGICAL-PROPERTY ?A ?B))
 :AXIOM-CONSTRAINTS (DOMAIN _CLOSED MATERIAL-OBJECT))
(DEFINE-RELATION _CONCENTRATED (?A ?B)
 "We rename 'concentrated' the strictly mereological 
definition of 'whole': integral and self-connected. This because it seems more 
intuitive talking of concentrated and distributed wholes rather than of wholes and 
distributed ?object?, ?stuff?"
 :DEF
 (AND (FORALL (?Y ?Z)
       (=> (AND (PART-OF ?Y ?A) (PART-OF ?Z ?A)) (CONNECTED ?Y ?Z)))
      (TOPOLOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _WHOLE (?A ?B)
 "We rename 'concentrated' the strictly mereological 
definition of 'whole': integral and self-connected. This because it seems more 
intuitive talking of concentrated and distributed wholes rather than of wholes and 
distributed ?object?, ?stuff?"
 :IFF-DEF (_CONCENTRATED ?A ?B))
(DEFINE-RELATION _DISTRIBUTED (?A ?B)
 "The converse of _concentrated. Here 'part'
from mereology is used, because 'topological-part' has shown some formal problems
(see end of the source file)."
 :DEF
 (AND (EXISTS (?Y ?Z)
       (AND (PART-OF ?Y ?A) (PART-OF ?Z ?A) (NOT (CONNECTED ?Y ?Z))))
      (TOPOLOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _OPEN (?A ?B) :DEF
 (AND (EXISTS (?C ?D)
       (AND (T-COMPLEMENT ?A ?D) (INTERIOR ?A ?C) (CONNECTED ?C ?D)))
      (TOPOLOGICAL-PROPERTY ?A ?B))
 :AXIOM-CONSTRAINTS (DOMAIN _OPEN MATERIAL-OBJECT))
(DEFINE-RELATION _SELF-CONNECTED (?A ?B)
 "(self-)connectedness in an object (even a space) 
arises when it is the sum of two parts whose interiors have connected complements."
 :DEF
 (AND (EXISTS (?Y ?Z)
       (AND (OBJECT ?Y)
            (OBJECT ?Z)
            (EXISTS (?C) (AND (MEREO-SUM ?Y ?Z ?C) (IDENTITY ?A ?C)))
            (EXISTS (?D ?E ?F ?G)
             (AND (INTERIOR ?Z ?G)
                  (T-COMPLEMENT ?G ?F)
                  (INTERIOR ?Y ?E)
                  (T-COMPLEMENT ?E ?D)
                  (CONNECTED ?D ?F)))))
      (TOPOLOGICAL-PROPERTY ?A ?B)))