Ontology today is in many ways in a state similar to that of analysis in the late 18th century prior to arithmetization: it lacks the sort rigorous theoretical foundations needed to elevate ontology to the level of a genuine scientific discipline. This paper attempts to make some first steps toward te development of such foundations. Specifically, starting with some basic intuitions about ontologies and their content, I develop an expressively rich framework capable of treating ontologies as theoretical objects whose properties and logical interconnections - notably, potential for integration - we can clearly define and study. Ontology today is in a state similar to that of analysis in the late 18th century. The practical power of the calculus had been convincingly demonstrated in the work or Newton and his great successors. Moreover, the field of real analysis itself had seen an explosion of creativity, exemplified most notably in the work of Euler. However, Euler's own work also revealed worrisome foundational problems. For techniques used with great success in one instance to prove deep and dramatic theorems in another instance could lead to absurdities, e.g., that the value of certain monotonically increasing infinite series was 1. Such results led to a conceptual crisis - how can any results be trusted when the methods that generate them can lead to error? This crisis was addressed, and successfully eliminated, by the development of rigorous foundation for analysis - widely known as the arithmetization of analysis - by Cauchy, Weierstrass, Bolzano, and others in the early 19th century. Building on the sound foundation of number theory, mathematicians replaced the intuitive but undefined notions of analysis - limit, continuity, series, integration, real number etc. - with clearly defined counterparts (e.g., the now-familiar ; definition of limit) and banished unruly notions like that of an infinitesimal altogether.2 With these solid underpinnings in place, mathematicians were able to identify clear conditions of applicability for their analytic methods that prevented the derivation of absurdities without limiting their ability to prove desirable results. A similar foundation is needed in the study of ontologies. As with analysis prior to arithmetization, the potential of ontologies is evident, but the fundamental notions remain largely intuitive; notably, there is no precise characterization of the notion of an ontology, nor what it is for two ontologies to be intergrated. What we need, then, is our own “arithmetization” - in a nutshell, we need ontology theory: a mathematical framework, akin to number theory or modern analysis, that enables us to characterize the notion of an ontology formally and develop accounts of their properties and the various ways in which one ontology can be related to another. Note also that the framework itself might not be used as it stands for any actual ontology integration work. It is in the respect analogous to computability theory. No one actually programs turing machines (except as a heuristic exercise). Rather, the notion provides a model of computation that serves as a foundation for both theoretical and, therefore, indirectly, applied computer science. In this brief paper we can only make some first halting steps toward a general ontology theory. The bulk of this paper will be to argue for, and lay out in varying degrees of detail, a formal framework with the representational horsepower adequate for a robust ontology theory.
I begin with some intuitions to motivate the design of a framework for ontology theory. 1. Ontologies consist of propositions. 2. Propositions are not sentences, they are what sentences express; different sentences in different languages (or possibly the same language) can express the same proposition. 3. Propositions can be equivalent without being identical. 4. Propositions and ontologies are objects, things we can talk about. 5. The content of an ontology consists of the propositions involving concepts in the ontology that are entailed by the constituent propositions of the ontology. 6. Ontologies are comparable in terms of their content. In particular, two ontologies are equivalent if they have the same content. 3
In developing a general ontology theory our concern is describe the phenomenon, just as in the development of number theory or real analysis or, for that matter, computability theory. We therefore place no computational restrictions on expressiveness, and hence will avail ourselves of at least full first-order logic.3
However, we will need quite a lot more than that to satisfy the intuitions in the preceding section. Notably:
Re (
Re (
Re (
Re (
Re (
Re (
I will satisfy these desiderata by developing a first-order theory of
structured relations, of which propositions will be one species.
Ontologies will be identified with 1-place relations, which for most
purposes can play the role of classes. This theory will satisfy desiderata
(
A Formal Framework for Ontology Theory In this section I will define a language with appropriate expressive power for ontology theory and a corresponding semantics. 4.1
To accomodate the narrow columns of the ECAI 2-column format, as much as anything, I will simply use the basic apparatus of standard Principia Mathematica-style first-order language, augmented with a number of useful constructs. I will call the language “L”.
Note that the unfriendliness of such languages in regard to computer processability is no more to the point here than it is with respect to group theory or computability theory. Our goal is theoretical — a mathematical theory of ontologies. Such work, of course, if sound, should lead to developments wherein computer processable languages are critical, but at this point processability is not an issue. 4.1.1
The lexicon consists of a countable set of individual constants, a denumerable set of individual variables, for each n 0, a countable set of n-place predicate constants and a denumerable set of n-place predicate variables (jointly called n-place predicates), the reserved logical symbols :, ^, _, !, $, 8, 9, , and 2, and parentheses and brackets. Individual variables will consist of lower case letters, typically x, y, z, possibly with numerical subscripts. n-place predicate variables will consist of upper case letters with numerical superscripts (suppressed where context serves to indicate the arity of an n-place predicate), typically F n, Gn, and Hn, possibly also with numerical subscripts. For purposes here, constants will consist of alphanumeric strings — other than the single-character strings already in use for the variables — beginning with an upper or lower case letter; dashes are also permitted to join alphanumeric strings. Typically, I will use a strings beginning with a lower case letter for constants that are intended to denote individual objects and strings beginning with an upper case letter for constants intended to denote relations. 4.1.2
We define formulas and terms by a simultaneous recursion: 1. Any constant or variable (individual or predicate) is a term. 2. If is an n-place predicate and 1, . . . , n are any terms, n 0, then ( 1; : : : ; n) is an (atomic) formula of L. is said to occur in predicate position, and each i in argument position, in ( 1; : : : ; n). In the case where n = 0, we omit the empty parentheses and say that standing alone is an atomic formula. 3. If ', are formulas, so are :', 2', and (' ! ). 4. If ' is any formula and 1, . . . , n any variables, then (8 1 : : : n)' is a formula. 5. If ' is a formula containing no occurrences of 2, no bound variables occurring in predicate position, and no bound predicate variables, and 1, . . . , n are any individual variables that do not occur free in any term occurring in ', then [ 1 : : : n '] is an n-place predicate. 6. Nothing else is a term or formula of L
The usual definitions of ^, _, $, and 9 will be assumed.
There are two particularly distinctive features of L. First, although
the language of L contains so-called “higher-order” variables, unlike
standard higher-order languages, these variables, and n-place
predicates generally, are considered terms; they can occur as arguments
to other predicates. Semantically speaking, as we will see
explicitly below, this means that our universe is type-free — everything
is an object; the quantifiers of the language will range over
everything alike. Note this does not mean that there is no distinction
between kinds of things. Notably, as noted already, our basic ontology
includes relations as well as ordinary individuals. Rather, in
accordance with intuition (
Perhaps the strongest linguistic evidence for type freedom is the phenomenon of nominalization, whereby any verb phrase can be transformed into a noun phrase of one sort or another, most commonly, a gerund. So, for example, the verb phrase ‘is famous’ indicates a property that can be predicated of individuals, as in ‘Quentin is famous’. Its gerundive counterpart, however, ‘being famous’, serves to denote a subject of further predication, as in, e.g., ‘Being famous is all Quentin thinks about’. Intuitively, the verb phrase indicating the property predicated and the gerund indicating the object of Quentin’s thoughts (i.e., the object possessing the property of being thought by Quentin) are the very same thing, the property of being famous.
In L, this “dual role” of properties and relations — thing
predicated vs. object of predication — is reflected in the fact that the same
constant can play both traditional syntactic roles of predicate symbol
and individual constant. Thus, in L, we can write both
(
Because all objects are of the same logical type, it follows that
any property can be predicated of any property and, in particular,
a property can be predicated of (and, indeed, can exemplify) itself.
Again, this comports with natural language; the property of being a
property, for instance, is a property, and hence exemplifies itself. This
is naturally represented in L in the obvious way:
(
It must be emphasized that the fact that we will be quantifying over properties, propositions, and relations generally does not in and of itself mean that L is higher-order. For that, one’s semantics must involve higher-order quantifiers whose range includes a power set construction of some ilk over a domain of logical individuals. In our semantics, there is no such construction; there is but a single domain over which a single type of quantifier ranges.
The second distinctive feature of L, and arguably the most
prominent, is the presence of complex terms [ 1 : : : n ']. Intuitively,
these terms denote complex relations. For instance, the term
(
Clause (
Clause (
The requirement that -bound variables all occur free in ' rules out such terms as [ xy P x] that contain vacuous -bound variables;4 The restriction on free occurrences of -bound variables within complex terms occurring in ' rules out such terms as [ xy P [ zQxz]y];5 The restriction on bound occurrences of predicate variables within complex terms occurring in ' rules out such terms as [ y (9F 1)y = F 1];6
However, the terms that would be permitted without these restrictions are inessential to our purposes here and hence allowing them would introduce unnecessary technical complexity.
While the restrictions to non-modal formulas in the formation of terms is, like the two above, also inessential, it has a certain intuitive warrant. For, unlike the three restrictions above, this restriction reflects an important feature of the intended domain guiding the development of the current framework. Specifically, we are formulating a theory of first-order ontologies, that is, ontologies whose constituent propositions are expressible by sentences in a non-modal first-order language (hence in any weaker sublanguage thereof). This is, of course, not to say that there are no modal (or higher-order) ontologies. However, the vast majority of existing ontologies are first-order, and it seems quite unlikely that this will change with the development of the Semantic Web if the expressiveness of its basic language is to be on the order of DAML+OIL. Therefore, to provide the capacity to express modal propositions, at this point, seems unwarranted.
A theory of ontologies, however, does need this expressive power. Specifically, modality is useful for characterizing the nature of ontologies and their logical connections. Most notably, perhaps, as will be seen explicitly in Section 7 below, the modal component of the language of our theory enables us to define a robust notion of entailment which, in turn, can be used to formulate a correspondingly robust notion of ontological content. 4.2
In this section I will build upon work by Bealer [1], Zalta [7], and Menzel [5] to develop a rich “meta-ontology” of structured relations. 4.2.1
A model structure M for L is a 5-tuple hD; W; dom; Op; ext i. Here D = SfA; Rg is the domain of M, and consists of the union of two mutually disjoint sets A and R. A is the set of individuals of D and R is the set of relations, of which we consider propositions a species. R itself can be partitioned in two significant ways. First, R is the union of two mutually disjoint nonempty sets Rp and Rc , intuitively, the sets of logically primitive and logically complex relations, respectively. Additionally, R is the union of denumerably many nonempty sets R0, R1, . . . , each Rn being, intuitively, the class of n-place relations. We let Rnp and Rnc be Rp \ Rn and Rc \ Rn, respectively. W 4 Such terms are easily accommodated by means of a further set of logical operations Vaci that insert vacuous argument places into the ith “slot” in the argument structure of a relation. 5 See Menzel [5] for an account of the semantics of such terms and surrounding philosophical issues. 6 Again, see [5] for the semantics of such terms. is a nonempty set, intuitively, a set of “possible worlds” or “possible situations.” More formally, W provides us with a model of modality that enables us to represent entailment and other logical relations between ontologies. Accordingly, dom is a function that maps every element w of W to a subset dom(w) of D representing, intuitively, the set of things that “exist” in the possible world w.
The next element of a model structure, Op is a set of five sets of logical operations: a set of predication operations, fPred in1:::ik : 0 < i1 < : : : < ik n; k 07g; a set of two boolean operations, fNeg ; Impl g; a set of universalization operations, fUniv i1:::ik : 1 i1 < : : : < ik n; g; a set of conversion operations, fConv ij : 1 i < j < !g; and a set of reflection operations, fRe ij : 1 i < j < !g. These operations “construct” logically complex relations from individuals and less complex relations in D. Specifically, for all n: : Rn
Dk
c ! Rn k (1 i1 < : : : < ik Pred in1:::ik n; k 1); Neg : Rn Impl : Rn
c ! Rn;
Rm ! Rnc+m; Univ i1:::ik : Rn ! Rnc k, for k Conv ij : Rn ! Rnc (1 i < j Re ij : Rn ! Rnc 1 (1 i < j n. n); n);
We stipulate that Pred n (i.e., Pred in1:::ik for k = 0) is just the identity relation on Rn,8 and that Rc is just the union of the ranges of the logical operations, i.e., Rc = fS Range(f ) : f 2 SOpg. To capture fine-grainedness, it is assumed that all of these operations are one-to-one and that the ranges of all of the operations are pairwise disjoint — similar to their syntactic counterparts, the “logical forms” of relations formed from these operations are all distinct from one another.
Finally, let Dn be the set of all n-tuples over D and let D = S0<n<! Dn. ext is a function on R W such that for all r 2 Rn, w 2 W , ext (r; w) Dn. Note that, for r 2 R0, only two extensions are possible: fhig, i.e., D0 itself, and the empty set ?. In this case it is useful to think of the former as the truth value > (truth) and the latter as the truth value ? (falsity).
The behavior of ext is constrained further by the logical
operations in S Op. Some notational conventions will be helpful for
stating these constraints. For A Dn, let A be Dn A. Where s _ s0 is
the concatenation of two sequences (tuples) s; s0, for subsets A; B of
Dn and Dm, respectively, let A _ B = fa _ b : a 2 A; b 2 Bg.
Where 1 i1 < : : : < ij n, we let hb1; : : : ; bniia11::::::iajj be
result of replacing each bik with ak, and we let hb1; : : : ; bnii1:::ij
be the result of deleting each bik from hb1; : : : ; bni. Given this, let
r 2 Rn; q 2 Rm; then:
ext (Pred in1:::ik (r; a1; : : : ; ak); w) =
fhb1; : : : ; bnii1:::ik : hb1; : : : ; bniia11::::::iakk 2 ext (r; w)g;9
ext (Neg (r); w) = ext (r; w);
ext (Impl (q; r); w) = ext (q; w) _ Dn [ Dm _ ext (r; w)
ext (Univ i1;:::;ij (r); w) =
fha1; : : : ; anii1:::ij : 8b1; : : : ; bj 2 dom(w);
i1:::ij
ha1; : : : ; anib1:::bj 2 ext (r; w)g
7 If k = 0, then i1 : : : ik is the null sequence, which we want to allow here.
8 This stipulation will yield as logical truths all instances of =
[ 1 : : : n ( 1; : : : ; n)], for all n-place predicates .
9 Note that by the definition of the Pred functions, we always have k n in
Pred in1:::ik .
ext (Conv ij (r); w) =
fha1; : : : ; ai 1; aj ; : : : ; aj 1; ai; : : : ; ani
ext (r; w)g
ext (Re ij (r); w) =
fha1; : : : ; aj 1; aj+1; : : : ; ani :
ext (r; w) and ai = aj g
Constituency and Logical Form The intuitive picture here is a
“quasi-constructive” one similar to the intuitive picture that
underlies the iterative conception of sets. We begin with a set A of
individuals and a set Rp of logically simple relations. The logically
simple relations are thought of as the meanings of the primitive
predicates in an ontology. The predication functions applied to primitive
relations and individuals yield basic atomic relations — notably,
basic atomic propositions — and the remaining logical operations
applied to these yield logically complex relations. These in turn, can
be arguments to further applications of the logical operations,
yielding an “iterative hierarchy” of relations of increasing complexity.
Intuitively, then, relations in R are either primitive or are “built up”
from individuals and other relations via the logical operations, and
the manner in which a relation is so built up can be thought of as
its logical form. So, for example, our example proposition (
The manner in which a relation is built up from individuals and other relations can be thought of as its logical form. We can make this idea rigorous as follows. Say that a constituency tree for an element r 2 R is any labeled ordered tree T whose nodes are in D and whose root node is r, such that, for every node e of T , the daughter nodes e1; : : : ; ej of e are such that, for some operation F 2 S Op, F (e1; : : : ; ej ) = e. A constituency tree T for r is complete iff every leaf node o of T is an individual or a primitive relation, i.e., iff o 2 A [ Rp. Given the constraints on our logical operations it is easy to show that every r 2 R has exactly one complete constituency tree, which we can therefore identify with the logical form of r. We define an object o 2 D to be a constituent of a relation r 2 R just in case 10 I am of course using the term ‘[ y Larger (sun; y)]’ here, not mentioning it; I am not talking about the term itself, but rather the property it intuitively denotes under the standard English meanings of the constituent constants. e is a node in the complete constituency tree for r. o is a primitive constituent of r iff o is a constituent of r and o 2 A [ Rp. The notion of constituency will be important for defining the concept of ontological content in Section 7 below. 4.2.2
Denotations for the terms of L relative to a model structure M are determined by partitioning the class of complex terms according to their syntactic form. In brief, where is [ 1 : : : n '], if the order of the -bound variables in ' does not correspond to 1; : : : ; n, then is the conversionij of an appropriate term 0. Otherwise, if one of the -bound variables occurs free more than once in ', then is a reflectionij of an appropriate 0. Otherwise, is classified as the n universalizationi1;:::;ij , implication, negation, or predicationi1;:::;ik of the appropriate sort depending on the logical form of '. Complex terms of the form [ 1 : : : n ( 1; : : : ; n)], for any predicate — i.e., those of the form predicationn — are said to be trivial, as they indicate no more logical complexity than the constitutive predicate .
Given a model structure M, let d be a function assigning elements of the domain D of M to the individual constants and variables of L and elements of Rn to the n-place predicates of L. Such a d is known as a denotation function for L relative to M. Denotations for complex terms are then assigned by extending d in an obvious way that exploits the close parallel between the syntactic form of complex terms and the logical forms of complex relations:
If is the conversionij of 0, then d( ) = Conv ij (d( 0)). If is the reflectionij of 0, then d( ) = Re ij (d( 0)).
If is the universalizationi1;:::;ij of , then d( ) Univ i1;:::;ij (d( 0)).
If is the implication of 0 and 00, then d( ) Impl (d( 0); d( 00)).
If is the negation of 0, then d( ) = Neg (d( 0)).
n
If is the predicationi1;:::;ij of 0 of 1; : : : ; j , then d( ) =
Pred in1;:::;ij (d( 0); d(
We say that a denotation function d0 for L relative to M is a variant of d, for any variable , just in case, for all variables 6= , d0( ) = d( ).11
An interpretation A of L is a pair hM; di consisting of a model structure M = hD; W; dom; Op; ext i and a denotation function d for L relative to M. For any variable , a -variant of A = hM; di is any interpretation A0 = hM; d0i such that d0 is a -variant of d.
Let A = hM; di be an interpretation, where M = hD; W; dom; Op; ext i. Truth at a world w 2 W in A for the formulas of L is defined in the standard sort of way:
( 1; : : : ; n) is true at w in A iff hd(
The proof theory for this semantics is an extension of classical firstorder logic with identity. Notably, there are principles of identify for = = 2 complex terms that ensure fine-grainedness, e.g., that no universalization is an implication or a negation, that predications are identical iff they are predications of the same relation of exactly the same objects, and so on.
More relevant for ontology theory, however, is a principle of conversion that takes as axioms all instances of: (10) [
1 : : : n ']( 1; : : : ; n) $ ' 11;;::::::;; nn ; where ' 11;;::::::;; nn is the result of replacing every free occurrence of i in ' with i. This principle lets us move freely between statements about individuals and the attribution of complex properties and relations to those individuals, e.g., (11) [ x Enjoys(x; salmon) ^ Prefers(x; wine; beer )](jo) $ Enjoys(jo; salmon) ^ Prefers(jo; wine; beer ) Notably, as we will see below, this principle will give us the ability to move from talking about the propositions in an ontology to using them in logical inferences. Like the other axioms of our theory, (10) is easily shown to be valid relative to the semantics above. 6
The notion of constituency enables us to capture the intuitive fact that different ontologies contain different concepts: the concepts in an ontology are simply the properties and relations that are constituents of the propositions of that ontology. Our fine-grained, structured notion of properties, relations, and propositions gives us a rigorous foundation for analyzing and exploiting the notion of constituency. We have characterized constituency model theoretically above in Section 4.2.1. In this section we capture the notion axiomatically. We begin with a schema:12 (12)
Const ( ; 0); where 0 is a nontrivial complex term and occurs free in 0 That is, any term occurring free within a complex term indicates a constituent of the relation denoted by the complex term.
Next, we note that the constituency relation is a strict partial ordering, i.e., it is transitive and asymmetric (hence also irreflexive): (13) (Const (p; q) ^ Const (q; r)) ! Const (p; r) (14) Const (q; r) ! :Const (r; q)
Finally, we can define an object to be primitive just in case it has no constituents: (15) Prim(x) =df :(9q)Const (q; x) This reflects the model theoretic fact that the ranges of the logical operations (other than the “trivial” Pred n operations) are all subsets of Rc. 7
As indicated, content is best cashed out in terms of some notion of entailment. In classical first-order logic, entailment is usually understood model theoretically. Ciociou and Nau [3] have taken some steps in this direction in developing a formal notion of intertranslatability between ontologies. For them, ontologies are understood as sets of 11 Thus, as it is often informally put, d0 differs from d at most in what it assigns to . 12
Recall that a trivial [ 1 : : : n ( 1; : : : ; n)].
complex term is of the form sentences, and the content of an ontology is understood in terms of its formal models: the content of an ontology O consists in the set of its semantic consequences, i.e., the set of sentences that are true in all the models of O. This approach thus can yield a robust notion of common ontological content across different languages in terms of shared models.
This approach is clear and insightful, but suffers from two shortcomings. First, though a notion of common content is possible on this approach, the notion of ontology is still language-dependent; an ontology is a set of sentences in some language. This violates intuitions 1 and 2 above, which jointly imply that ontologies are classes of language-independent propositions. More seriously, however, the approach — as a basis for a general theory of ontologies — is unwieldy. Content is understood in terms of the models of a theory. Hence, on this approach, one has to import the full apparatus of firstorder model theory — basic set theory, formal languages, interpretations, model theoretic truth and entailment, etc — just to define a reasonable notion of ontological content. Moreover, the model theoretic approach makes for a rather austere and formal notion of content — to identify the meaning of a sentence with a set of models is rather far removed from ordinary semantic notions.
Though the present approach has a strong model theoretic component, that component serves only to ground a first-order theory of ontologies and their content; no linguistic or model theoretic entities, properties, or relations are introduced into the theory.13 Rather, it develops an account of ontologies and their content that is language independent and grounded in the intuitive notion of propositions — rather than the austere and abstract notion of a model — as the basic semantical unit of meaning.
To get at the relevant notion of entailment in our theory, recall once again that, intuitively, ontologies can be thought of as classes of propositions. The notion of a proposition is easily defined in terms of our “higher-order” quantifiers: (16) Proposition(p) =df (9F 0)p = F 0 Understanding classes as properties, we can now define an ontology to be a nonempty class of propositions: (17)
Ont (O) =df (9F 1)O = F 1 ^ (9x)F 1(x) ^ 8p(F 1(p) ! Proposition(p))
The notion of entailment we are after involves both modality and our notion of constituency. We first define a constituent of an ontology O to be a constituent of one of the propositions in O: (18) OntConst (x; O) =df Ont (O) ^ (9p)(O(p) ^ Const (x; p)) Next, say that an ontology O entails a proposition F 0 just in case F 0 must be true if all the propositions in O are true: (19)
Entails(O; F 0) =df
Ont (O)^ 2((8G0)(O(G0) ! G0) ! F 0) Now say that F 0 and O share primitives if every primitive constituent of F 0 is a constituent of O: (20)
ShPrim(F 0; O) =df Ont (O) ^ (8x)((Prim(x) ^ Const (x; F 0)) ! OntConst (x; O)) 13 Though of course we define a model theory for the language L of our theory, but that’s just a matter of our own metatheoretic housekeeping: it simply provides a proper theoretical foundation for the language we are using to express our theory; the model theory for L is not itself a part of ontology theory.
Thus, combining (19) and (20), we have the notion of entailment we are after: (21) StrEntails(O; F 0) =df Entails(O; F 0) ^ ShPrim(O; F 0): That is, an ontology O strongly entails a proposition F 0 just in case O entails F 0 and F 0 and O share primitives; that is, intuitively, if O entails F 0 and F 0 is “built up” from the same pool of concepts and objects — the same “conceptual vocabulary” — as the propositions in O. We will sometimes write “O ) F 0” for “StrEntails(O; F 0)”.
The content of an ontology, then, can be thought of as all of the propositions that it strongly entails. As it happens, we cannot strictly define the content of an ontology as an object. However, for theoretical purposes, strong entailment appears to be all we need. For example, we can say that one ontology O subsumes another O0 just in case the content of O0 is included in that of O, i.e., just in case O strongly entails every proposition that O0 does: (22)
Subsumes(O; O0) =df
Ont (O) ^ Ont (O0) ^ (8p)(O0 ) p ! O ) p) Ontologies can then be said to be equivalent just in case they subsume each other: (23) Equiv (O; O0) =df Subsumes(O; O0) ^ Subsumes(O0; O):
Subtler metrics for comparison are of course also possible, e.g., two non-equivalent ontologies might nonetheless share all or some of their primitives. More generally, the notions defined above provide a rich framework for analyzing a wide variety of notions relevant to understanding the nature of, and logical relations between, ontologies. 8
A major extension of this work that goes far beyond the current scope will consist in developing a theory of integration. At a purely abstract level, integration is fairly straightforward. One can import several ontologies into the language L of our approach by creating a separate namespace for the terms in each ontology and translating them from the language of the ontology into L. There will thus be, initially, no possibility of name conflicts. Because the principle ['] $ ' is valid, it will be possible to move seamlessly back and forth between using the axioms of a given ontology to investigate its properties and talking more generally about the ontology and its content.
Because distinct ontologies are imported with separate namespaces, there is no danger of logical inconsistency arising from incompatible ontologies. Integration can proceed by identifying or otherwise logically connecting the concepts (objects, properties, relations, and propositions) expressed across ontologies. Thus, for instance, it might be postulated that two concepts (properties) from different ontologies are identical; or that one concept subsumes the other; or that for every instance a of one there are two instances of the other that bear some relation to a; and so on. In this way the logical connections between ontologies can be mapped clearly and rigorously and with ever greater precision.
However, while this account of integration is theoretically adequate as far as it goes, a complete treatment will have to include a theory of languages that connects sets of sentences with the ontologies that they express, and which should lead to more practical applications of the theory. Investigating integration at this more applied level will be the next phase of this project. It will be possible for ontology to make significant progress toward the lofty goals workers in the area are pursuing only if it has proper theoretical foundations. For such goals can be reached only if there is a clear, generally shared understanding of the subject matter of ontology, one that makes it possible clearly to define the scope of the discipline, to identify its subject matter, and chart a course toward the resolution of its outstanding problems. The approach in this paper shows promise for providing these essential theoretical underpinnings