The Information Flow Framework (IFF)
Table of Contents  What is an Ontology?
 (definition)
 (dictionaries)
 (distinctions)
 The SUOIFF Project
 Origins and Influences
 The Categorical Manifesto
 IFF Design Guidelines
 IFF Development Phases
 Principle of Conceptual Warrant
 Principle of Categorical Design
Part I. The IFF Metatheory  The IFF Architecture
 (old version)
 (new version)
 The IFF Metastack
 Four Fundamental Relations
 The IFF Code
 The IFF (meta) Ontologies
 Some Example IFF Terms
 The Basic IFF Terms
 The IFF Metalanguages
 (old version)
 (new version)
Part 0. Introduction to the IFF What is an Ontology?  (definition)
 (dictionaries)
 (distinctions)
The SUOIFF Project Origins and Influences The Categorical Manifesto IFF Design Guidelines IFF Development Phases  Principle of Conceptual Warrant
 Principle of Categorical Design
What is an Ontology? (definition) Example. Consider the ecommerce example (Figure 1) of a schema (ontology).  concepts are represented as nodes,
 relationships are represented as edges,
 constraints are represented as parallel pairs of edge paths, limits and coproducts.
What is an Ontology? (dictionaries) Dictionaries and Ontologies. An ontology is similar to a dictionary, but has greater detail and structure. In the IFF there is a strong analogy between dictionaries and metaontologies.  Builders. There is a correspondence between the builders of dictionaries and those of metaontologies. Corresponding to the lexicographers, who create dictionaries, are the ontologicians (mathematicians, particularly categorytheorists) who create metaontologies.
 Source material. There is a correspondence between the source material used by dictionaries and that used by metaontologies. The entries placed and described in dictionaries have three sources:
 terms borrowed from other dictionaries,
 new terms used to express concepts in works of literature, and
 new terms used to express concepts in everyday speech.
 By analogy, the concepts axiomatized in metaontologies originate from three sources:
 terms borrowed from other metaontologies,
 new metalevel terms used to express concepts in objectlevel ontologies, and
 new metalevel terms used to express the conceptual structure of a community.
 For both dictionaries and ontologies, the second source is most important.
 Source creators. There is a correspondence between the source creators used by dictionaries and those used by metaontologies. Corresponding to the literary figures who originate new terms in works of literature are the knowledge engineers who originate and use new metalevel terms in objectlevel ontologies.
What is an Ontology? (distinctions) The object/meta distinction.  An objectlevel ontology represents some aspect of the “real world”. We distinguish between populated and unpopulated ontologies.
 Unpopulated ontologies have only type information [aka schemas or theories].
 Populated ontologies have both type and instance information, plus the classification relationship between these two kinds of things [aka databases or logics].
 A metalevel ontology is an ontology about ontologies. It represents some aspect of the organization of objectlevel ontologies.
The prescriptive/descriptive distinction.  Both dictionaries and ontologies come in two basic philosophies: prescriptive or descriptive. A descriptive dictionary or ontology describes actual usage. Most modern dictionaries are descriptive. The IFF is a descriptive metatheory, since it uses the constraint called “conceptual warrant”.
The monolithic/modular distinction.  The monolithicmodular distinction is important for the maintenance of objectlevel ontologies. A monolithic ontology is onesizefitsall. The monolithic approach is not compatible with the need for continual revision and consistency checking. The modular approach, which advocates the lattice and category of theories constructions, is very compatible with these needs.
The SUOIFF Project
Origins and Influences
The Categorical Manifesto Mathematical Context (~ Category)  “To each species of mathematical structure, there corresponds a category whose objects have that structure, and whose morphisms preserve it.”
Passage (Construction) between Contexts (~ Functor)  “To any natural construction on structures of one species, yielding structures of another species, there corresponds a functor from the category of the first species to the category of the second.”
Generalized Inverse (~ Adjunction)  “To any canonical construction from one species of structure to another corresponds an adjunction between the corresponding categories.”
 Two special cases:
 Reflection: G ◦ F = IdB “G is rali to F” “B reflective subcategory A”
 Coreflection: IdA = F ◦ G “G is rari to F” “A coreflective subcategory B”
Sums, Quotients and Fusions (~ Colimit)  “Given a species of structure, say widgets, then the result of interconnecting a system of widgets to form a superwidget corresponds to taking the colimit of the diagram of widgets in which the morphisms show how they are interconnected.”
IFF Design Guidelines In the development of the IFF, certain guidelines have proven to be very important. Goal. The IFF metatheory was designed to represent first order logic, its languages, theories, modeltheoretic structures and (local) logics, including satisfaction. This metatheory incorporates the theory of institutions of Goguen and Burstall. Metaguideline. Follow the intuitions of the working categorytheorist. Such intuitions represent naive category theory. The meaning of naive here is not pejorative. It means primitive, natural, intuitive, firstformed, primary, not evolved or elemental. Practice. Initially formulate any IFF module as a settheoretic axiomatization using a first order expression. Eventually, by eliminating quantifiers and logical connectives, move, morph or transform this settheoretic axiomatization toward a categorytheoretic axiomatization. Ruleofthumb. Keep it simple! From the foundational standpoint, this means that we start with no assumptions at all. However, in view of the Cantor diagonal argument, as a first step we assume a slender hierarchy called the IFF metastack.
IFF Development Phases Phase 1: (20002001)  First ontology axiomatized: The IFF Category Theory (meta) Ontology (IFFCAT).
 A nonstarter: a topos axiomatization. Objections due to its lack of warrant.
 Warrant means evidence for or token of authorization.
 Conceptual warrant is an adaptation of the librarianship notion of literary warrant.
Phase 2: (20012003)  Designed bottomup; Require conceptual warrant; Follow categorical design principle.
 Important metalogic concept incorporated: finite limits; for example, composition of class functions requires the pullback concept.
Phase 3: (20042006)  Central task: reorganization of the IFF metastack using "adjunctive axiomatization".
 This will provide the metastack with better structure.
 This will simplify the IFFKIF metalanguage core by not requiring the definite descriptive operator.
 Important metalogic concept incorporated: exponents.
 Fibrations and indexed categories will also be central.
 Institutions will be fully axiomatized.
Principles. During the IFF development, four concepts have eventually emerged as important. One of these concepts, the IFF metastack, is discussed elsewhere. The other three concepts are principles for IFF development. In chronological order these are  the principle of conceptual warrant,
 the principle of categorical design and
 the principle of institutional logic.
Conceptual warrant restricts the introduction of upper metalevel terminology, whereas categorical design forces the introduction of this terminology, principally in the core.
The Principle of Conceptual Warrant Principle: All IFF terminology should require conceptual warrant for their existence: any term that appears in (and is axiomatized by) a metalanguage should reference a concept needed in a lower metalevel or object level axiomatization. Note: The terminology appearing in any standardization metaontology will exert authority. Because of this, in selecting which terminology to specify in the IFF, we utilize the notion of “conceptual warrant”. Warrant means evidence for, or token of, authorization. Analogue: Conceptual warrant is an adaptation of the librarianship notion of literary warrant. According to the Library of Congress, its collections serve as the literary warrant (i.e., the literature on which the controlled vocabulary is based) for the Library of Congress subject headings system. In the same fashion, the objectlevel (n = 0) and lower metalevel (n = 1) terminology of the IFF serves as the conceptual warrant for the IFF upper metalevel (n = 2) axiomatization.
The Principle of Categorical Design Principle: The design of a module at any particular metalevel should adhere to the property that its axiomatic representation is strictly categorytheoretic:  All axioms use terms from the metalanguage at that metalevel.
 All axioms are atomic: no axioms use explicit logical notation; no variables, quantification (‘forall’, ‘exists’) or logical connectives (‘and’, ‘or’, ‘not’, ‘implies’,‘iff’) are used.
Note: The peripheral (noncore) modules in the lower IFF metalevel (n = 1) have the tripartite form: outer category namespace, inner object and morphism namespaces.  Currently, the outer namespace follows the categorical design principle exactly.
 And the inner namespaces follow it to a great extent (80–90%).
Part I. The IFF Metatheory The IFF Architecture  (old version)
 (new version)
 The IFF Metastack
 Four Fundamental Relations
The IFF Code  IFF (meta) Ontologies
 Some Example IFF Terms
 The Basic IFF Terms
The IFF Metalanguages  (old version)
 (new version)
The IFF Architecture (old version)
The IFF Architecture (new version)
The IFF Metastack There are axiomatizations for categories, finite (and general) limits/colimits, exponents and subobject classifiers. The IFF metastack represents the chain of categories (toposes) Set1 Set2 Set3 ... Setn ... Set
Four Fundamental Relations The chain of categories (toposes)  Set1 Set2 … Setn … Set
are axiomatized in the IFF Core (meta) Ontology (IFFCORE). These inclusions represent the fact that axiomatization at level n includes specialization of the axiomatization at level n+1. Specialization (technical term) means the exact adaptation of the core terminology and axiomatization at level n+1 to level n by use of four fundamental relations: subset, (function) (optimal)restriction and (relation) abridgment (plus intersection).
Some Example IFF Terms
The Basic IFF Terms
The IFF Metalanguages (old version) Each metalevel has an associated metalanguage  It contains the metalanguage directly above it.
 Its terminology is defined by the metaontologies at that level.
 It is used to axiomatize the (meta)ontologies at all lower levels.
Introductions  IFFUr – axiomatization for categories
 IFFTop – axiomatization for finite limits
 IFFUpper – axiomatization for exponents and finite colimits
 IFFLower – axiomatization for subobjects and general limits/colimits
IFFKIF enables lisplike firstorder expression: functions, binary relations, connectives and quantifiers. Uses restricted quantification.
The IFF Metalanguages (new version) Each metalevel has an associated metalanguage  It contains the metalanguage directly above it.
 Its terminology is defined by the metaontologies at that level.
 It is used to axiomatize the (meta)ontologies at all lower levels.
IFF metashell  Logical part: enables lisplike firstorder expression: sets, unary functions, binary relations, connectives and quantifiers. Uses restricted quantification with guards and definite description.
 Mathematical part: (IFFMETA namespace) metaterminology allowing IFFCORE to conform to the principle of categorical design.
IFF metaur & IFF metan: (IFFCORE ontology) introduces axiomatization for toposes; that is, for categories, finite limits/colimits, exponents, subobjects and general limits/colimits
Part II. The IFF Institutional Application Two IFF Efforts to Represent FOL  The IFFONT
 (old version)
 (new version)
 The IFFFOL
Logical Environments  Languages
 Language Expressions
 Language Colimits
 Models
 Theories
 The Category of Theories
 Theory Colimits (fusion)
 Truth Classification & Truth Concept Lattice
 Truth Concept Lattice Functionality
Institutions  The Grothendieck Construction
 The Truthful Connection
Two IFF Efforts to Represent FOL NonTraditional FOL  The IFF Ontology (meta) Ontology (IFFONT)
Traditional FOL  The IFF First Order Logic (meta) Ontology (IFFFOL)
The IFF Ontology (meta) Ontology (IFFONT) (old version) Nontraditional. Home page: http://suo.ieee.org/IFF/metalevel/lower/ontology/ontology/version20021205.htm. Based on view that nary relations incorporate a notion of hypergraphs. Also, novel definition of models via classifications: t  r instead of r(t). Completely axiomatized: Language, Theory, Model and Logic. Language and Theory are cocomplete. Free models and logics exist. Models are nonstandard: they have a subset of abstract tuples. Problem:  Model fiber functions must be restricted to bijective variable functions.
 Must limit Language and Theory to corresponding subcategories Language≐ and Theory≐
 Language≐ (hence, Theory≐) is not cocomplete; in fact, does not have coproducts.
 Analysis: reference (sort) function is too inflexible (Note: such a sort function is recommended in Enderton's text!).
The IFF Ontology (meta) Ontology (IFFONT) (new version) Traditional. Discussion and links at http://suo.ieee.org/IFF/workinprogress/#IFFOO. Still based on view that nary relations incorporate a notion of hypergraphs. In fact, identifies languages with hypergraphs (of a certain kind). This kind of hypergraph does not use a reference (sort) function. Languages (hence, theories) are cocomplete. Model fiber function exists. Special advantage: hypergraphs are equivalent to spangraphs.  Spangraphs are a more flexible definition of logical language (in terms of relational arity).
 Spangraphs nicely model the SCL "roleset syntax", where arguments form a set of rolevalue pairs.
 Example: ‘(Married (roleset: (wife Jill) (husband Jack)))’
 This notion has been advocated in SCL development by Pat Hayes. Position and argument order are not needed. According to Hayes, this provides some insurance against communication errors.
The IFF First Order Logic (meta) Ontology (IFFFOL)
Logical Environments Distinctions  Potential versus actual
 Formal versus interpretive
Four Fundamental Notions  Language
 Theory
 Model
 actual or interpretive semantics
 Logic
Languages We assume that each language has an adequate, possibly denumerable, set of variables X. This generalizes the usual case where sequences are used – the advantage for this generality is elimination of the dependency on sequences and natural numbers. Cardinal numbers represent a skeletal quotient. A language L = rel(L), ent(L), arity(L), sign(L):  a relation type set rel(L),
 an entity type set ent(L),
 a reference set pair L = refer(L) = X, ent(L),
 an arity function L = arity(L) = sign(L) · tuplearity(L) : rel(L) X, and
 a signature function L = sign(L) : rel(L) tuple(refer(L)).
 For any relation type ρ rel(L)
 arity(L)(ρ) = {x, x, … xn X is its arity with external form ρ, x, x, … xn,
 L(ρ) : arity(L)(ρ) ent(L) is its signature with external form ρ, x : ε, x : ε, … xn : εn,
 where L(ρ)(xk) = εk for < k < n.
Language Expressions Associated with any language L = ent(L), rel(L), L, L, L is an expression language expr(L) = ent(L), rel(expr(L)), L, expr(L), expr(L) that extends L.  The set of entity types and the reference set pair of expr(L) are the same as L.
 The relation types of expr(L) are Lexpressions. The set rel(expr(L)) of Lexpressions is inductively defined on relation types rel(L) using the logical quantifiers and connectives.
 The arity and signature functions
 expr(L) = arity(expr(L)) : rel(expr(L)) X
 expr(L) = sign(expr(L)) : rel(expr(L)) tuple(refer(L))
 are recursivelydefined extensions from the relation types of L to the expressions of L. Sentences are expressions with empty arity .
Associated with any language morphism f = rel(f), ent(f) : L L is an expression language morphism expr(f) = rel(expr(f)), ent(f) : expr(L) expr(L) that extends f.  The entity type function is identity.
 The relation function rel(f) : rel(L) rel(L) is recursively extended to an expression function rel(expr(f)) : rel(expr(L)) rel(expr(L)).
There is a language morphism L = embed(L) : L expr(L) that embeds any language into its associated expression language.  The entity function is the identity.
 The relation function rel(L) : rel(L) rel(expr(L)) embeds relation types as expressions.
There is a language morphism L = collapse(L) : expr(expr(L)) expr(L) that collapses the expression of expression language of any language into its expression language.  The entity function is identity.
 The relation function rel(L) : rel(expr(expr(L))) rel(expr(L)) collapses expressions.
Language Colimits Language colimits are important:  they are the basis for theory colimits.
They involve two opposed processes:  “summing” “keeping things apart” “preserving distinctness”
 “quotienting” “putting things together” “identification” “synonymy”
The “things” involved here are symbols:  relation type symbols
 entity type symbols
 and the concepts they denote.
Models A model M is a product of a language (= hypergraph) and a classification.  rel(M) is a relation classification; instances are abstract “tuples”.
 ent(M) is an entity classification; types are “sorts”. Entity types are unary relation types.
 The type aspect typ(M) = typ(rel(M)), typ(ent(M)), arity(M), sign(M) is a language.
 The instance aspect inst(M) is a hypergraph.
This approach is comparable to the structure of Aristotle's ontological framework.  The two distinctions in Aristotle's ontological framework of “universal versus particular” and of “quality versus substance” are analogous to the two distinctions in the semantic architecture of the IFF between “type versus instance” and “relation versus entity”.
There is a type functor from models to languages typ : Model Language. There is a model functor from languages to classes mod = typ : Language SET.  For fixed language L we denote by mod(L) the class of models of that type.
 For any language morphism f : L L, we can define a model fiber function
 mod(f) : mod(L) mod(L).
 There is a satisfaction relation
 between models M mod(L) and expressions expr(L) (hence, sentences).

Theories A theory T = base(T) axm(T) consists of an underlying language L = base(T) and a set of sentences axm(T) sen(L) called the axioms of T. Theories represents formal or axiomatic semantics. We assume a fixed common variable set X for all languages.  An Lmodel M is a model of the theory T, denoted M LT, when M satisfies each axiom axm(T); that is, when M L for all axioms axm(T).
 A theory T entails a sentence sen(L) when M LT implies M L for any model M. Such a sentence is called a theorem of T. Any axiom is a theorem. The set of theorems of T is denoted by thm(T). The theory clo(T) = T = L, thm(T) is called the closure of T. A theory is closed when it equals its closure.
 Two theories T and T are compatible when they share the same type language: base(T) = base(T). A theory T is a specialization of a compatible theory T when T entails every theorem of T; that is, when thm(T) thm(T). Then we also say that T is a generalization of T, and denote this by T T. This is a preorder on theories over L – any theory T is equivalent to its closure T clo(T).
The Category of Theories Contexts:  Theory
 Closed Theory
 Language
Theory Colimits (Fusion) Informally, identify the theories to be used in the construction. Alignment: Formally, create a diagram of theories T of shape (indexing) graph G that indicates this selection. This diagram of theories is transient, since it will be used only for this computation. Other diagrams could be used for other fusion constructions.
Truth Classification & Truth Concept Lattice Truth classification of 1storder language L  Instances are Lmodels.
 Types are Lsentences.
 Incidence is satisfaction: M = when is true in M.
Truth concept lattice of L  In the IFF approach, this is the appropriate
 “lattice of ontological theories.”
 Formal concept is a pair c = ext(c), int(c) where:
 The int(c) is a closed theory (set of sentences).
 The ext(c) is the collection of all models for that theory.
 Lattice order is the opposite of theory inclusion.
 The join or supremum of two theories is the intersection of the theories.
 The meet or infimum of two theories is the theory of the common models.
 Both Lmodels and Lsentences generate formal truth concepts (theories).
 An object concept is the theory of a model.
 An attribute concept is the models of a sentence.
Truth Concept Lattice Functionality
Institutions I = Sign, Mod, Sen, ⊨  http://www.cs.ucsd.edu/users/goguen/projs/inst.html
Sign: an abstract category of signatures . Sen : Sign Set: a sentence functor indexing abstract sentences Sen() by signatures . Mod : Sign SETop: a model functor indexing abstract models Mod() by signatures .  Mod()Sen(): a signature parameterized satisfaction relation. Satisfaction Condition (expresses the invariance of truth under change of notation): For any signature morphism f : ', any 'model M' and any sentence e, M' ' Sen(f)(e) iff Mod(f)(M')  e. Spec : Sign Set: a specification functor indexing abstract theories (specifications) Spec() by signatures . A specification is a set of sentences. I : Sign CLSN: a classification functor is a concise definition of an institution. But CLSN CLG. Î : Sign CLG: a concept lattice functor is an alternate definition of an institution. Example institutions  first order logic (with first order structures as models)
 many sorted equational logic (with abstract algebras as models)
 Horn clause logic
 variants of higher order and of modal logic
The Grothendieck Construction
The Truthful Connection
Summary The IFF is a descriptive category metatheory whose architecture contains nested metalanguages. The main institutional application of the IFF is axiomatized in the Ontology (meta) Ontology (IFFONT) and the First Order Logic (meta) Ontology (IFFFOL). These form flexible and general institutions for first order logic. Institutions formally express semantic integration as an ontological fusion process. Each community represents their conceptual space in their own terms, and connects with others via morphisms that enable ontological alignment specification. Institutions represent logical environments and institution morphisms connect logical environments. Amongst other things, the IFF is in the process of axiomatizing the theory of institutions.
Appendix What is an Ontology?  (other views)
 (other views)
Language Morphisms Language Sums Language Endorelations Language Quotients Theory Morphisms Theory Sums Theory Endorelations and Quotients
What is an Ontology? (other views) B. Chandrasekaran, Jorn R. Josephson, V. and Richard Benjamins.  "Ontological analysis clarifies the structure of knowledge. Given a domain, its ontology forms the heart of any system of knowledge representation for that domain. Without ontologies, or the conceptualizations that underlie knowledge, there cannot be a vocabulary for representing knowledge …. Second, ontologies enable knowledge sharing."
Tom Gruber.  "An ontology is an explicit specification of a conceptualization. The term is borrowed from philosophy, where an ontology is a systematic account of existence. For AI systems, what 'exists' is that which can be represented."
Jeff Heflin.  "An ontology defines the terms used to describe and represent an area of knowledge. Ontologies are used by people, databases, and applications that need to share domain information (a domain is just a specific subject area or area of knowledge, like medicine, tool manufacturing, real estate, automobile repair, financial management, etc.). Ontologies include computerusable definitions of basic concepts in the domain and the relationships among them (note that here and throughout this document, definition is not used in the technical sense understood by logicians). They encode knowledge in a domain and also knowledge that spans domains. In this way, they make that knowledge reusable.... Ontologies are usually expressed in a logicbased language, so that detailed, accurate, consistent, sound, and meaningful distinctions can be made among the classes, properties, and relations."
What is an Ontology? (other views) Christopher Welty.  "Ontology is a discipline of philosophy whose name dates back to 1613 and whose practice dates back to Aristotle. It is the science of what is, the kinds and structures of objects, properties, events, processes, and relations in every area of reality. … [W]hat the field of ontology research attempts to capture is a notion that is common to a number of disciplines: software engineering, databases, and AI to name but a few. In each of these areas, developers are faced with the problem of building an artifact that represents some portion of the world in a fashion that can be processed by a machine."
John F. Sowa.  "The subject of ontology is the study of the categories of things that exist or may exist in some domain. The product of such a study, called an ontology, is a catalog of the types of things that are assumed to exist in a domain of interest D from the perspective of a person who uses a language L for the purpose of talking about D."
Tim BernersLess, James Hendler, and Ora Lassila.  "In philosophy, an ontology is a theory about the nature of existence, of what types of things exist; ontology as a discipline studies such theories. Artificialintelligence and Web researchers have coopted the term for their own jargon, and for them an ontology is a document or file that formally defines the relations among terms. The most typical kind of ontology for the Web has a taxonomy and a set of inference rules."
SUO WG.  "An ontology is similar to a dictionary or glossary, but with greater detail and structure that enables computers to process its content. An ontology consists of a set of concepts, axioms, and relationships that describe a domain of interest. … An upper ontology is limited to concepts that are meta, generic, abstract and philosophical, and therefore are general enough to address (at a high level) a broad range of domain areas."
Language Morphisms A language morphism f = rel(f), ent(f) : L L:  a relation type function rel(f) : rel(L) rel(L), and
 an entity type function ent(f) : ent(L) ent(L).
 These must preserve arity and signature:
 preservation of arity:
 rel(f) · arity(L) = arity(L)
 L(rel(f)(ρ)) = var(f)(L(ρ)) for any relation type ρ rel(L)
 if ρ, x, x, … xn then rel(f)(ρ), x, x, … xn
 preservation of signature:
 rel(f) · sign(L) = sign(L) · tuple(refer(f))
 L(rel(f)(ρ)) = tuple(refer(f))(L(ρ)) for any relation ρ rel(L)
 if ρ, x : ε, x : ε, … xn : εn then rel(f)(ρ), x : ent(f)(ε), … xn : ent(f)(εn)
Language Sums – “keeping things apart” Let L1 and L be two languages with common variable set X. The sum language L1+L:  The relation type and entity type sets are the disjoint unions of their components
 rel(L1+L) = rel(L1)+rel(L) and ent(L1+L) = ent(L1)+ent(L).
 The variable set is the fixed set X, var(L1+L) = var(L1) = var(L) = X.
 The arity function is the pairing
 arityL1L = L1L = L1, L : rel(L1)rel(L) X
 with L1L(1) = L1(1) for 1 rel(L1) and L1L() = L() for rel(L).
 The signature function is the pairing
 signL1L = L1L = L1, L : rel(L1)rel(L) tuple(refer(L1L))
 with L1L(1) = L1(1) for 1 rel(L1) and L1L() = L() for rel(L).
The sum injection language morphism in(L1) = inrel(L1), inent(L1) : L1 L1L:  The relation function is the disjoint union injection
 inrel(L1) : rel(L1) rel(L1L) = rel(L1)rel(L);
 the entity function is the sum injection
 inent(L1) : ent(L1) ent(L1L) = ent(L1)ent(L).
Language Endorelations Let X be any set representing a fixed set of variables. Let endo(X) denote the class of all language endorelations at X. A language endorelation is a triple J = lang(J), rel(J), ent(J) consisting of  a language lang(J) = L with variable set X,
 a binary endorelation rel(J) = R rel(L)rel(L) on relation types of L, and
 a binary endorelation ent(J) = E ent(L)ent(L) on entity types of L.
These must satisfy the following constraints on arity and signature functions of L. Here R is the equivalence relation generated by rel(J) = R and E is the equivalence relation generated by ent(J) = E. For any pair of relation types ρ1, ρ2 rel(L), if (ρ, ρ) rel(J) = R, then  arity(L)(ρ) = arity(L)(ρ) and sign(L)(ρ) sign(L)(ρ),
where sign(refer(L))sign(refer(L)) is the equivalence relation on tuples defined as follows: τ τ when arity(refer(L))(τ) = arity(refer(L))(τ) and τ(x) E τ(x) for all x arity(refer(L))(τ) = arity(refer(L))(τ). Often, the endorelations rel(J) = R and ent(J) = E are equivalence relations on relation types and entity types. However, it is not only convenient but also very important not to require this. In particular, the endorelations defined by parallel pairs of language morphisms (coequalizer diagrams) do not have component equivalence relations. A simple inductive proof shows that the triple Ĵ = L, R, E is also a language endorelation.
Language Quotients – “putting things together” The quotient L/J of an endorelation J = L, R, E = lang(J), rel(J), ent(J) on a variable set X is the language defined as follows:  The set of relation types are the equivalence classes rel(L/J) = rel(L)/R.
 The set of entity types are the equivalence classes ent(L/J) = ent(L)/E.
 The set of variables is var(L/J) = var(L) = X.
 The arity function L/J = arity(L/J) : rel(L)/R X is defined pointwise: L/J(ρR) = L(ρ) for all relation types ρ rel(L).
 The signature function L/J = sign(L/J) : rel(L)/R tuple(refer(L/J)) is defined pointwise: L/J(ρR)(x) = L(ρ)(x)E for all relation types ρ rel(L) and variables x L(ρ).
There is a canonical quotient language morphism  J = rel(J), ent(J) : L L/J
whose relation type function is the canonical surjection  rel(J) = canon(rel(J)) = R : rel(L) rel(L)/R, and
whose entity type function is the canonical surjection  ent(J) = canon(ent(J)) = E : ent(L) ent(L)/E.
The fundamental property for this language morphism is trivial, given the definition of the quotient language above.
Theory Morphisms Theories are related through theory morphisms. A morphism of theories f : T T is a language morphism f : L L that maps source axioms to target theorems: sen(f)(axm(T)) thm(T). Then, a morphism of theories maps source theorems to target theorems: sen(f)(thm(T)) thm(T). When the source and target share the same base language (they are compatible) and the base language morphism is the identity, a morphism of theories f : T T is equivalent to a theory ordering T T, which states that theory T generalizes theory T or theory T specializes theory T. The composition and identities for theory morphisms are defined in terms of their base type language morphisms. Theories and theory morphisms form the category Theory.
Theory Sums
Theory Endorelations and Quotients Given a theory T = base(T), axm(T), a theory endorelation J is a language endorelation J = ent(J), rel(J) over L = base(T) . Recall that J has an associated type language endorelation expr(J) = ent(J), expr(J) over expr(L). The entity, relation and expression endorelations generate equivalence relations  E ent(L)ent(L),
 R rel(L)rel(L), and
 R* expr(L)expr(L).
The set of expressions on the quotient base language is expr(T/J) = expr(L)/R*. The quotient T/J = base(T/J), axm(T/J) of an endorelation J on a theory T has  base(T/J) = base(T)/base(J) , the quotient of the base language of the base endorelation,
 axm(T/J) = φR* φ axm(T), the collection of equivalence classes of axioms of T.
There is a canonical quotient theory morphism J : T T/J whose base is the canonical quotient type language morphism  base(J) = base(base(J)) : base(T) base(T/J) = base(T)/base(J) .
This morphism clearly maps axioms of T to axioms of T/J.
Do'stlaringiz bilan baham: 