The Information Flow Framework
|
Metalevel |
Ontology |
|
|
Upper |
(44 pages) |
|
|
|
(64 pages) |
|
|
|
(93 pages) |
[The numbering of figures, diagrams and tables restarts in each top-level namespace.]
1. The Information Flow Framework (IFF)
|
The mission of the Information Flow Framework (IFF) is to further the development of the theory of Information Flow, and to apply Information Flow to distributed logic, ontologies, and knowledge representation. IFF provides mechanisms for a principled foundation for an ontological framework – a framework for sharing ontologies, manipulating ontologies as objects, partitioning ontologies, composing ontologies, discussing ontological structure, noting dependencies between ontologies, declaring the use of other ontologies, etc. IFF is primarily based upon the theory of Information Flow initiated by Barwise (Barwise and Seligman 1997), which is centered on the notion of a classification. Information Flow itself based upon the theory of the Chu construction of *-autonomous categories (Barr 1996), thus giving it a connection to concurrency and Linear Logic. IFF is secondarily based upon the theory of Formal Concept Analysis initiated by Wille (Ganter & Wille 1999), which is centered on the notion of a concept lattice. IFF represents metalogic, and as such operates at the structural level of ontologies. In IFF there is a precise boundary between the metalevel and the object level. The structure of IFF is illustrated in Figure 1. |
2. Architecture
|
This section describes an overall scheme for an “industrial strength” ontological framework for the SUO, which represents the SUO structural level in terms of IFF meta-ontologies. At the highest level of the SUO is the Top Core Ontology, whose purpose is to provide an interface between the new KIF and the SUO ontological structure. The Top Core Ontology provides an adequate foundation for representing ontologies in general and for defining the other metalevel ontologies (Figure 1) in particular. All upper metalevel ontologies import and use, either directly or indirectly, the Top Core Ontology. The Information Flow Framework represents the structural aspect of the SUO called the metalevel. The Information Flow Framework is rather large, but is highly structured. It is partitioned into two levels (upper/lower) corresponding to the large/small distinction in foundations – the upper level is for set-theoretically large notions and the lower level is for set-theoretically small notions. Each level is divided into about ten namespaces. The structure of the Information Flow Framework (Figure 1) is as follows. 1. Upper metalevel a. core namespace of set-theoretic classes and their functions b. Category Theory Ontology (~10 namespaces) 2. Lower metalevel a. Model Theory Ontology (~10 namespace) b. … The upper metalevel has a distinguished namespace (SET) for set-theoretic classes and their functions called the core namespace. The remainder of the upper metalevel, called the IFF Category Theory Ontology, represents in various namespaces standard ideas of category theory. Much of the content comes from well-known category-theoretic intuitions and some of the semi-standard notation used in papers and textbooks. The IFF Category Theory Ontology provides a framework for reasoning about metalogic, as represented in the lower metalevel ontologies. Examples of provable statements are: “the Classification namespace represents a category,” or “the IF classification functor is left adjoint to the IF theory functor” (Kent 2000). The IFF Category Theory Ontology is a KIF formalism for category theory in one of its normal presentations. Other presentations, such as home-set or arrows-only, may also have merit. The IFF Category Theory Ontology is based upon the namespace for large graphs and graph morphisms that includes horizontal multiplication of graphs and a theory of coherence – a category is a monoid in the monoidal category of large graphs. The upper metalevel is used to represent and axiomatize the lower metalevel. The notion of a topos, which is central to categorical foundations, is important in the Information Flow Framework, where it is encountered in at least three ways: there will be a namespace (TOP) in the upper metalevel that axiomatizes a topos; the namespace (set) for small sets and their functions in the lower metalevel can be proven to be a topos with the TOP axioms; and (see the section on Previous Foundations) the core namespace (SET) in the Information Flow Framework satisfies Colin McLarty's topos axioms. The TOP namespace logically depends (see the arrows in Figure 1) upon the namespace for categories (CAT), which in turn logically depends upon the core namespace (SET). This foundational approach should answer Solomon Feferman’s qualms about logical and psychological priority. The lower metalevel contains at present one module called the Model Theory Ontology consisting of about ten namespaces. This expression of model theory, somewhat novel since it is based upon the theory of Information Flow, is used to represent and axiomatize the object level. One main goal of the Model Theory Ontology is representation of a principled approach to ontology composition using colimits. Not unconnected to this is the principled support that the Model Theory Ontology gives to John Sowa’s notion of “an infinite lattice of all possible theories as the theoretical foundation of the SUO.” It does this by realizing another main goal – the representation of the truth classification and truth concept lattice[1]. The truth concept lattice provides “a framework that can support an open-ended collection of ontological theories (potentially infinite) organized in a lattice together with systematic metalevel techniques for moving from one to another, for testing their adequacy for any given problem, and for mixing, matching, combining, and transforming them to whatever form is appropriate for whatever problem anyone is trying to solve” (Sowa). A specific goal of the lower metalevel is to represent some central notions of model theory – models (first-order structures), expressions and satisfaction. In the IFF approach for structuring the SUO, models are 2-dimensional structures composed of small classifications along one dimension and small hypergraphs (or spans) along the other; here classifications represent the instance-type distinction, whereas hypergraphs represent the entity-relation distinction. The lower metalevel makes heavy use of the upper metalevel – indeed, a goal in modeling the lower metalevel is to abide by the following categorical property. CATEGORICAL PROPERTY: The (new-KIF)
axiomatization for the ontologies in the lower metalevel is strictly
category-theoretic – all axioms are expressed in terms of category-theoretic
notions, such as the composition and identity of large/small functions or the
pullback of diagrams of large/small functions; [no KIF] no axioms use
explicit KIF connectives or quantification; and [no basic KIF ontology] no
axioms use terms from the basic KIF ontology, other than pair bracketing '[-]' or pair projection '(-
1)', '(-
2)'. This would seem to extend to all ontologies for true categories
(not quasi-categories) – those categories whose object and morphism
collections are classes (not conglomerates). In the lower metalevel, ontologies are organized in two dimensions corresponding to this notion of IFF model. These two precise mathematical dimensions correspond to the intuitive distinctions of Heraclitus (the physical versus the abstract) and Peirce (1st-ness, 2nd-ness and 3rd-ness). In IFF the type-token distinction looms large. Along the instance-type dimension are the IF classification namespace that directly represents the instance-type distinction, the IF theory namespace that is connected by an adjunction to the IF classification namespace (Kent 2000), and the combining IF logic namespace. Terminology for the classification namespace is included in the SUO Coda and SUO Modules databases. The concept lattice namespace represents Formal Concept Analysis. In addition to formal concepts and their lattices, this also includes the idea of a collective concept. In the entity-relation dimension are the hypergraph namespace that represents multivalent relations and the language namespace (whose presentation is a little delicate) that represents logical expressions. Also at the lower level are the set namespace that models the topos of small sets, the combining model namespace and a derivative ontology namespace. The latter two namespaces are related to the fundamental truth between models and expressions. In addition, the lower metalevel namespaces have sufficient morphism and colimit structure to provide a principled approach for combining of ontologies at the object level. Other modules (namespaces or subontologies), in addition to the Model Theory Ontology, are perhaps possible at the lower metalevel. These might include modules for categorical model theory, modules for modal, tense and linear logic, modules for rough and fuzzy sets, modules for semiotics, etc. The object level is where the content ontologies reside. These could be very generic, such as a 4D ontology, or specific, such as ontologies for government or higher education. It should be noted that the object level satisfies a representation property similar to the categorical property satisfied by the lower metalevel – the ontological language used is not KIF; instead it is the terminology defined and axiomatized in the lower structural level (terms such as ‘subtype’, ‘instance’, ‘expression’, ‘model’, ‘ontology’, ‘relation’, ‘entity’, ‘role’, etc.). Since the Information Flow Framework represents abstract semantics, many applications are possible. Two, in particular, are being actively considered: ○ a representation for the categorical framework for the Specware system of the Kestrel Institute, which is based on category theory and supports creation and combination of specifications (ontology analogs) using colimits. ○ a semantics for DAML+OIL, the DARPA Agent Markup Language, whose goal is to develop language and tools to facilitate the concept of the semantic web. |
3. Programming Language Analogy
|
At the core the SUO is coded in the new KIF. As an ontological machine language, the Lisp-y style of logical expression of the new KIF is very useful, adequately expressive and conveniently terse. However, in the proposed IFF structure for the SUO the new KIF will not be used as an “industrial strength” ontological language. Instead, the SUO terminology will follow the following programming language analogy. ○ The new KIF is like an ontological machine language. ○ The Top Core Ontology is like an ontological assembly language. It provides a basic ontological apparatus for the SUO. The purpose of this kind of terminology is to be an interface between the KIF language and other ontological terminology, in general. Because of its function, the Top Core Ontology might also be called the bootstrap ontology. Hopefully, this will have only one namespace, perhaps with the namespace prefix ‘KIF’. ○ The metalevel or structural level of the SUO, as encoded in the Information Flow Framework, is like a high level programming language such as Lisp, Java, ML, etc. IFF is a building blocks approach to ontological structure – a rather elaborate categorical approach that uses some insight from the theory of distributed logic called Information Flow (Barwise and Seligman, 1997), and also uses ideas from the theory of Formal Concept Analysis (Ganter and Wille, 1999). The structural level of the SUO has many namespaces, such as a core namespace ‘SET’, a set namespace ‘set’, a category namespace ‘CAT’, a categorical colimit namespace ‘COL’, a classification ‘cls’ namespace, an IF theory namespace ‘th’, a concept lattice namespace ‘cl’, a language namespace ‘lang’, a model namespace ‘mod’, a truth namespace for the fundamental truth classification and concept lattice, and other supporting namespaces. ○ The object level of the SUO is like the various software applications, such as word processors, browsers, spreadsheet software, databases, etc. The ontologies in this component are specified using the terminology axiomatized in the lower structural level. The object level provides the content of the SUO coming from the various domain ontologies and philosophies with their own namespaces. The object level would include ontologies such as Casati and Varzi’s ontology of holes, John Sowa’s upper ontology, Barry Smith’s Formal Theory of Boundaries/Objects, Borgo, Guarino, and Masolo’s Formal Theory of Physical Objects, the public Cyc ontology, ontologies for organizations, ontologies for repositories, etc. Part of the purpose of the structural level of the SUO is to interrelate the various modules at the object level. It is important that a complete distinction and an explicit boundary is kept between the object level and the metalevel. This fundamental partition must be obviously manifest in the SUO. Some ontologies at the object level may choose to represent and discuss metalevel concepts, but they would still be doing so at the object level. |
4. Overview
|
The Information Flow Framework uses and imports the following terms from the Top Core Ontology: the KIF relational terms ‘KIF$class’ (otherwise known as unary relations or predicates) and ‘KIF$relation’ and ‘KIF$subclass’, the KIF functional term ‘KIF$function’, the generic type declaration term ‘KIF$signature’, and the sequence terminology ‘[-]’, ‘1’, ‘2’. The term ‘KIF$class’ is used in both a syntactic and a semantic sense – syntactically things that are of this type should function as KIF predicates, whereas semantically this denotes the largest kind of collection. Hence, semantically ‘KIF$class’ corresponds in general to collection and in particular to conglomerate. The Information Flow Framework uses the three-level set-theoretic hierarchy of sets – classes – conglomerates. Table 1 locates various collections and functions in this three-tiered framework. Functions between conglomerates are unary or binary KIF functions. To make this the root ontology vis-à-vis importation, we have renamed these as conglomerate (CNG) functions. As CNG functions, source and target type constraints are specified with the ‘CNG$signature’ relation. In contrast, functions between classes, otherwise called “SET functions,” have a more abstract, semantic representation, since they have explicitly specified source and target classes and an abstract composition operation with identities. Every SET function is represented as a unary CNG function. The signature of a SET function is given by its source and target. |
The
Information Flow Framework consists of an adequate amount of set theory
which, on the one hand, is sufficiently flexible for the categorical inquiry
involved in the Information Flow Framework (IFF) but, on the other hand, is
sufficiently restrictive that IFF be consistent (does not produce
contradictions). The approach to foundations used here is an adaptation of
that outlined in chapter 2 of the book Abstract and Concrete Categories
(Adámek, Herrlich & Strecker 1990). The basic concepts needed are those
of sets and classes. To this we add the notion of Cartesian
closure and topos structure at the level of classes.
Table 1: Kinds of Specific Collections
|
Conglomerates |
○ the collections of classes, functions, opspans and binary cones ○ the collections of large graphs and large graph morphisms ○ the collections of large categories and functors between large categories ○ the collection of natural transformations, and the collection of adjunctions |
|
Classes |
○ the object and morphism collections in any large category ○ the source and target of the component map of a natural transformation ○ the collections of algebras and homomorphisms of a monad ○ the collection of diagrams and cocones for each type of finite colimit in a category |
|
Sets |
○ sets as collections and the extent of their functions ○ the instance and type sets of classifications and the instance and type functions of infomorphisms ○ any small relation regarded as a collection |
5. Previous Foundations
Topos AxiomsThe core namespace in the Information Flow Framework axiomatizes the quasi-category of classes and their functions. When the axioms for a topos are in place in the Category Theory Ontology, then the category of sets and their functions, which is encoded in the set namespace in the Foundation Ontology as a restriction of the core namespace, can be proven to be a well-pointed topos with natural numbers and choice. As mentioned above, the Foundation Ontology should partially satisfy Solomon Feferman’s representational needs, as expressed in the FOM list thread Toposy-turvey. For purposes of comparison, and to show completeness, here is a presentation of Colin McLarty’s topos axioms that give a first order expression for the theory of a well-pointed topos with natural numbers and choice. McLarty makes the following claims. o The theory was given by Lawvere and Tierney over 25 years ago. o It is are equivalent to Zermelo set theory with bounded comprehension and the axiom of choice. o It is adequate to classical analysis. The axioms use a two sorted language – a sort for objects and a sort for arrows. The axioms are partitioned into subsections: category axioms, finite completeness axioms, and topos axioms. The lists of primitives include informal explications. The actual axioms are numbered. The connections between the topos axioms and the Information Flow Framework are indicated. Category Axioms To express the axioms for a category, we use the following terminology (primitives). o For any object A the identity morphism on A is denoted here by ‘Id(A)’. In the Foundation Ontology a class (an object in the quasi-category of classes and functions) is declared by the ‘(SET$class ?a)’ expression [axiom SET$1], and the identity is represented by the ‘(SET.FTN$identity ?a)’ expression [axiom SET.FTN$12]. o Any morphism f with source (domain) object A and target (codomain) object B is denoted by ‘f:A®B’. In the Foundation Ontology a function (a morphism in the quasi-category of classes and functions) is declared by the ‘(SET.FTN$function ?f)’ expression [axiom SET.FTN$1], and the source and target functions are represented by the ‘(SET.FTN$source ?f)’ and ‘(SET.FTN$target ?f)’ expressions [axioms SET.FTN$2 and SET.FTN$3]. o The composition of two composable morphisms ‘f:A®B’ and ‘g:B®C’ is denoted by ‘f·g’ in diagrammatic order. In the Foundation Ontology the composition of two composable functions is represented by the ‘(SET.FTN$composition ?f ?g)’ expression [axiom SET.FTN$11]. The axioms for a category are as follows. 1. Two morphisms are composable when the target of the first is identical to the source of the second ‘f:A®B’ and ‘g:B®C’. A composable pair of morphisms is expressed by the following axiom. "(f,g)
[ $(A,B,C)
(f:A®B
&
g:B®C)
Û $(h)(f·g
= h) ]. In the Foundation Ontology this equivalence for the case of composable functions is expressed in the axiom group SET.FTN$11. 2.
The following axiom expresses the law of associativity of
morphism composition. "(f,g,h,k,i,j) [
(f·g = k & k·h = j & g·h = i) Þ f·i = j ]. In the Foundation Ontology the associative law of function composition is expressed by the theorem below SET.FTN$11. 3. The following pair of axioms express the two identity laws for categorical composition. "(f,A,B) [ f:A®B Þ (Id(A)·f = f & f·Id(B) = f) ]. In the Foundation Ontology the identity laws for functions are expressed in the theorem below SET.FTN$12. Finite Completeness Axioms The terminology and axioms in this section extend those of the previous section to give a category with terminal object and finite products. For full finite completeness this relies upon the further topos axioms, which together with these axioms imply finite completeness and cocompleteness. McLarty’s goal was to present a minimal set of axioms for a topos. This differs from the goals for the Foundation Ontology and IFF in general, which aim for completeness and high expressiveness. In particular, it is very important for other IFF metalevel ontologies to have access to a completely expressive terminology for pullbacks, since these are very heavily used. o The terminal object is denoted by ‘1’. In the Foundation Ontology any singleton class is terminal. To be specific, the Foundation Ontology uses the unit class 1 = {0} as the terminal class. In the Foundation Ontology the terminal class (in the quasi-category of classes and functions) is declared by the ‘SET.LIM$terminal’ and the ‘SET.LIM$unit’ expressions [axiom SET.LIM$1]. o The binary Cartesian product for both objects and morphisms is denoted by ‘_´_’; in particular, for any two objects A1 and A2 the binary Cartesian product is denoted by ‘A1´A2’. In the Foundation Ontology the binary product CNG function for classes is represented by the term ‘SET.LIM.PRD$binary-product’ [axiom SET.LIM.PRD$6], and the binary product CNG function for SET functions is represented by the term ‘SET.LIM.PRD.FTN$binary-product’ [axiom SET.LIM.PRD.FTN$11]. o The two binary product projection morphisms are denoted by ‘p1(_,_)’ and ‘p2(_,_)’. In the Foundation Ontology the two CNG binary product projection functions are represented by the terms ‘SET.LIM.PRD$binary-product’ The axioms for a category with terminal object and finite products are as follows. 4. An object 1 is terminal in a category when for any other object A there is a unique morphism 1A : A ® 1 from the object to the terminal object. The existence of a terminal object is stated by the following axiom. "(A) [ $!(f)(f:A®1) ]. In the Foundation Ontology this universal property is expressed by the definition of the unique function ‘SET.LIM$unique’ in axiom SET.LIM$2. 5. The source and target typing for the two binary product projection functions is declared by the following axioms. "(A,B) [ p1(A,B):A´B®A & p2(A,B):A´B®B ]. In the Foundation Ontology declarations are is expressed by the binary Cartesian product projection axioms SET.LIM.PRD$12 and SET.LIM.PRD$13. 6. The universality for the binary product is asserted by the following axiom. "(f,g,A,B,C)
[ (f:C®A & g:C®B) Þ
$!(u)(u:C®A´B
&
u·p1(A,B) = f & u·p2(A,B) = g) ]. In the Foundation Ontology this universal property is expressed by the definition of the mediator function ‘SET.LIM.PRD$mediator’ in axiom SET.LIM.PRD$14. 7. The following axiom extends the binary product to functions. "(f,g,A,B,C,D)
[ (f:A®B & g:C®D) Þ ( (f´g):A´C®B´D &
(f´g)·p1(B,D)
= p1(A,C)·f &
(fxg)·p2(B,D) = p2(A,C)·g ) ]. In the Foundation Ontology this property is expressed by the definition of the function binary product ‘SET.LIM.PRD.FTN$binary-product’ in axiom SET.LIM.PRD.FTN$6. Topos Axioms The terminology and axioms in this section extend those of the previous sections to a non-trivial Boolean topos. o A monomorphism in a category corresponds to an injection. The assertion that a morphism is a monomorphism is denoted by ‘mono(f)’. An epimorphism in a category corresponds to a surjection. The assertion that a morphism is an epimorphism is denoted by ‘epi(f)’. In the setting of topos theory, monomorphisms are regarded as subobjects. In the Foundation Ontology the injection class is declared by the term ‘SET.FTN$injection’ [axiom SET.FTN$13] and monomorphism class is declared by the term ‘SET.FTN$monomorphism’ [axiom SET.FTN$14]; also, the surjection class is declared by the term ‘SET.FTN$surjection’ [axiom SET.FTN$15] and epimorphism class is declared by the term ‘SET.FTN$epimorphism’ [axiom SET.FTN$16]. o Given two objects A and B in a category the exponent ‘B^A’ is the collection of all morphisms from A to B. In the Foundation Ontology the exponent class is declared by the term ‘SET.TOP$exponent’ [axiom SET.TOP$1]. o Given two objects A and B in a Cartesian-closed category the evaluation morphism ‘ev(A,B)’ evaluates morphisms: when applied to a morphism f from A to B and a value a in A it returns the image f(a). In the Foundation Ontology the evaluation function is declared by the term ‘SET.TOP$evaluation’ [axiom SET.TOP$2]. o The truth object is denoted by ‘1+1’, a disjoint union of two copies of 1. In the Foundation Ontology the truth class is defined by 2 = {0, 1}, where the elements are regarded as the truth values 0 = false and 1 = true. It is isomorphic to the disjoint union 2 @ 1+1. In the Foundation Ontology the truth class is declared by the term ‘SET.TOP$truth’ [axiom SET.TOP$5]. o The binary coproduct injections in1 : 1 ® 1+1 and in2 : 1 ® 1+1 are (function) elements of 1+1 corresponding to the truth values false and true, respectively. In the Foundation Ontology the true function (second injection) is declared by the term ‘SET.TOP$true’ [axiom SET.TOP$6]. The axioms for a Boolean topos are as follows. 8. A morphism is a monomorphism when it can be cancelled on the right (in diagrammatic order). Dually, a morphism is an epimorphism when it can be cancelled on the left. The definitions of monomorphism and epimorphisms are given by the following axioms. "(f)
[ mono(f) Û "(g,h)(g·f = h·f Þ
g = h) ]. "(f) [ epi(f) Û "(g,h)(f·g
= f·h Þ g = h) ]. In the Foundation Ontology the first definition is expressed as the definition of the monomorphism class ‘SET.FTN$monomorphism’ in axiom SET.FTN$14, and the second definition is expressed as the definition of the epimorphism class ‘SET.FTN$epimorphism’ in axiom SET.FTN$16. 9. A Cartesian-closed category is a finitely-closed category whose binary product functor (needs a specific binary product here) is left adjoint to the exponent functor. This is expressed in the following axiom. "(f,A,B,C) [ f:CxA®B Þ $!(u)(u:C®B^A & (u´Id(A))·ev(A,B) = f) ]. In the Foundation Ontology the “right adjoint” map, that takes the function f and returns the function u, is expressed as the definition of the adjoint function ‘SET.TOP$adjoint’ in axiom SET.TOP$3. 10. An elementary topos is a Cartesian-closed category that has a subobject classifier – an object W and a morphism true : 1 ® W that satisfy the axiom below. A classical topos can use the Boolean truth object as subobject classifier 1+1 = W. The following subobject classifier axiom states that every subobject f of an object B has a unique characteristic function u of that object – a function that makes the Diagram 1 a pullback diagram. "(f,A,B)
[ (f:A®B & mono(f)) Þ $!(u)(u:B®1+1
& "(h,k)((k·i2
= h·u) Þ $!(v)(v·f = h)) ) ].
11. A topos is Boolean when the truth injections in1 : 1 ® 1+1 and in2 : 1 ® 1+1 (truth value elements false and true) are complements. Equivalently, a topos is Boolean when the collection of subobjects of any object forms a Boolean algebra. Ø(i1 = i2) & "(f,g,A)
[ (f:1®A & g:1®A) Þ $!(u)(u:(1+1)®A
& i1·u
= f &
i2·u = g) ]. In the Foundation Ontology the fact that the
quasi-topos of classes and function is Boolean follows from the fact that the
‘(el2ftn
?c)’ is bijective for each class C [axiom SET.TOP$7]. Classical Analysis The following axioms allow us to get classical analysis by using natural numbers in a well-pointed topos with choice. 12. A natural numbers object in a category with terminal object and binary coproducts is an initial algebra for the endofunctor T(-) = 1+(-) on the category. The following axiom encodes this idea. $(N,0,s) [ (0:1®N & s:N®N)
& "(A,x,f) [ (x:1®A & f:A®A)
Þ $!(u)(u:N®A & 0·u = x & s·u = u·f) ] ]. In the Foundation Ontology the natural numbers class ‘SET.TOP$natural-numbers’, zero element ‘SET.TOP$zero’ and successor endofunction ‘SET.TOP$successor’ satisfy the axiom for a natural numbers object in the quasi-topos of classes and functions [axiom SET.TOP$8]. 13. The following axiom is the extensionality principle for morphisms of a category with 1. It states that 1 is a generator; that is, that morphisms are determined by their effect on the source (domain) elements. A category is degenerate when all of its objects are isomorphic. A non-degenerate topos that satisfies extensionality for morphisms is called well-pointed. "(f,g,A,B) [ (f:A®B & g:A®B) Þ "(h) ( (h:1®A
& (h·f = h·g)) Þ (f = g) ) ]. In the Foundation Ontology axiom SET.TOP$9 states that functions (morphisms in the quasi-category of classes) satisfy the extensionality principle. 14. The following axiom is one variant of the axiom of choice – it uses the standard definition of an epimorphism. The axiom of choice implies Boolean-ness for any topos. "(f,A,B)
[ epi(f) Þ $(g)(g:B®A &
g·f = Id(B)) ]. In the Foundation Ontology axiom SET.TOP$10
states that the quasi-category of classes and functions satisfies the axiom of choice. SketchesHere is the paraphrase of a discussion of sketches by Vaughan Pratt. A sketch is the categorical counterpart of a first-order theory. It specifies the language of the theory in terms of limits and colimits of diagrams. The language of (finitary) quantifier-free logic is representable entirely with finite product (FP) sketches, i.e. no colimits and only discrete limits. Finite limit (FL) sketches allow all limits, e.g. pullbacks which come in handy if you want to axiomatize composition of morphisms as a total operation (not possible with ordinary first order logic or FP sketches). Colimits extend the expressive power of sketches in much the same way that least-fixpoint operators extend the expressive power of first order logic (made precise by a very nice theorem of Adamek and Rosicky), but completely dually to limits. (Fixpoint operators are not obviously dual to anything in first order logic.) The machinery of sketches is either appealingly economical and elegant or repulsively complex and daunting depending on whether you look at it from the perspective of category theory or set theory. As a formalism for categorical foundations sketches have the same weakness as Colin McLarty’s axiomatization of categories: they are based on ordinary categories, with no 2-cells. (Again let me stress the importance of 2-categories, i.e. not just line segments but surface patches, for foundations.) On the one hand I'm sure this is not an intrinsic limitation of sketches, on the other I don't know what's been done along those lines to date. Higher-dimensional sketches are surely well worth pursuing. It would be beneficial to develop sketches of the IFF metalevel for comparison and contrast. Fibrations
|
There
is a need to incorporate some aspect of fibrations and indexed categories in
the Foundation Ontology. For one example, the (small) classification
namespace represents the category 6. Correspondences
|
Table 2 lists the correspondence between standard mathematical notation and the ontological terminology in the namespace for logic. Table 2: Correspondence between Mathematical Notation and Ontological Terminology
Table 3 lists the correspondence between standard mathematical notation and the ontological terminology in the basic ontology. Table 3: Correspondence between Mathematical Notation and Ontological Terminology
|
References
|
Adámek, Jirí, Herrlich, Horst and Strecker, George E. 1990. Abstract and Concrete Categories. New York: Wiley and Sons. Barr, Michael. 1996. The Chu Construction. Theory and Applications of Categories 2. Barwise, Jon and Seligman, Jerry. 1997. Information Flow: The Logic of Distributed Systems. Cambridge Tracts in Theoretical Computer Science 44. Cambridge University Press. Davey, B.A. and Priestly, H.A. 1990. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press. Ganter,
Bernhard and Wille, Rudolf. 1999. Formal
Concept Analysis: Mathematical Foundations. Berlin/Heidelberg:
Springer-Verlag. Kent, Robert E. 2000. The Information Flow Foundation for Conceptual Knowledge Organization. Proceedings of the 6th International Conference of the International Society for Knowledge Organization (ISKO). Toronto, Canada. Mac Lane, Saunders. 1971. Categories for the Working Mathematician, New York/Heidelberg/Berlin: Springer-Verlag. New edition (1998). |