which grew out of the attempt to distinguish formally between boundaries (in geography, geopolitics, and other domains) which reflect more or less arbitrary human demarcations and boundaries which reflect bona fide physical discontinuities (Smith 1995, 2001). Mereotopology is being applied by Salustri in the domain of digital manufacturing (Salustri, 2002) and by Smith and Varzi to the formalization of basic notions of ecology and environmental biology (Smith and Varzi, 1999, 2002). It has been applied also to deal with vague boundaries in geography (Smith and Mark, 2003), and in the study of vagueness and granularity (Smith and Brogaard, 2002, Bittner and Smith, 2001, 2001a<ref>Thomas Bittner and Barry Smith, “Granular Partitions and Vagueness” in Christopher Welty and Barry Smith (eds.), Formal Ontology in Information Systems, New York: ACM Press, 2001, 309–321.</ref>). Preferred approach of Casati & Varzi Casati and Varzi (1999: ch.4) set out a variety of mereotopological theories in a consistent notation. This section sets out several nested theories that culminate in their preferred theory GEMTC, and follows their exposition closely. The mereological part of GEMTC is the conventional theory GEM. Casati and Varzi do not say if the models of GEMTC include any conventional topological spaces. We begin with some domain of discourse, whose elements are called individuals (a synonym for mereology is "the calculus of individuals"). Casati and Varzi prefer limiting the ontology to physical objects, but others freely employ mereotopology to reason about geometric figures and events, and to solve problems posed by research in machine intelligence. An upper case Latin letter denotes both a relation and the predicate letter referring to that relation in first-order logic. Lower case letters from the end of the alphabet denote variables ranging over the domain; letters from the start of the alphabet are names of arbitrary individuals. If a formula begins with an atomic formula followed by the biconditional, the subformula to the right of the biconditional is a definition of the atomic formula, whose variables are unbound. Otherwise, variables not explicitly quantified are tacitly universally quantified. The axiom Cn below corresponds to axiom C.n in Casati and Varzi (1999: ch. 4). We begin with a topological primitive, a binary relation called connection; the atomic formula Cxy denotes that "x is connected to y." Connection is governed, at minimum, by the axioms: C1. (reflexive) C2. (symmetric) Let E, the binary relation of enclosure, be defined as:Exy is read as "y