¹¹institutetext: Ontologos

FOLE Equivalence

Robert E. Kent

Abstract

The first-order logical environment FOLE provides a rigorous and principled approach to distributed interoperable first-order information systems. FOLE has been developed in two forms: a classification form and an interpretation form. Two papers represent FOLE in a classification form corresponding to ideas of the Information Flow Framework ([14],[15],[16]): the first paper [9] provides a foundation that connects elements of the ERA data model [2] with components of the first-order logical environment FOLE; the second paper [10] provides a superstructure that extends FOLE to the formalisms of first-order logic. The formalisms in the classification form of FOLE provide an appropriate framework for developing the relational calculus. Two other papers represent FOLE in an interpretation form: the first paper [11] develops the notion of the FOLE table following the relational model [3]; the second paper [12] discusses the notion of a FOLE relational database. All the operations of the relational algebra have been rigorously developed [13] using the interpretation form of FOLE. The present study demonstrates that the classification form of FOLE is informationally equivalent to the interpretation form of FOLE. In general, the FOLE representation uses a conceptual structures approach, that is completely compatible with the theory of institutions, formal concept analysis and information flow.

Keywords:

structures, specifications, sound logics, databases.

1 Preface.

The architecture for the first-order logical environment FOLE is displayed in Fig. 1. ¹¹1 FOLE is described in the following papers: “The ERA of FOLE: Foundation” [9], “The ERA of FOLE: Superstructure” [10], “The FOLE Table” [11], “The FOLE Database” [12], “FOLE Equivalence” [this paper], and “Relational Operations in FOLE” [13] . The left side of Fig. 1 represents FOLE in classification form. The right side of Fig. 1 represents FOLE in interpretation form.

Figure 1: FOLE Architecture

Classification form.

An ontology defines the primitives with which to model the knowledge resources for a community of discourse (Gruber [6]). These primitives, which consist of classes, relationships and properties, are represented by the entity-relationship-attribute ERA model (Chen [2]). An ontology uses formal axioms to constrain the interpretation of these primitives. In short, an ontology specifies a logical theory.

Two papers provide a rigorous mathematical representation for the ERA data model in particular, and ontologies in general, within the first-order logical environment FOLE. These papers represent the formalism and semantics of (many-sorted) first-order logic in a classification form corresponding to ideas discussed in the Information Flow Framework (IFF [16]). The paper (Kent [9]) develops the notion of a FOLE structure; this provides a foundation that connects elements of the ERA data model with components of the first-order logical environment FOLE. The paper (Kent [10]) develops the notion of a FOLE sound logic; this provides a superstructure that extends FOLE to the formalisms of first-order logic.

Interpretation form.

The relational model (Codd [3]) is an approach for the information management of a “community of discourse” ²²2Examples include: an academic discipline; a commercial enterprise; the genetics research community, library science; the legal profession; etc. using the semantics and formalism of (many-sorted) first-order predicate logic. The first-order logical environment FOLE (Kent [8]) is a category-theoretic representation for this logic. ³³3Following the original discussion of FOLE (Kent [8]), we use the term mathematical context for the concept of a category, the term passage for the concept of a functor, and the term bridge for the concept of a natural transformation. A context represents some “species of mathematical structure”. A passage is a “natural construction on structures of one species, yielding structures of another species” (Goguen [5]). Hence, the relational model can naturally be represented in FOLE. A series of papers is being developed to provide a rigorous mathematical basis for FOLE by defining an architectural semantics for the relational data model.

Two papers provide a precise mathematical basis for FOLE interpretation. Both of these papers expand on material found in the paper (Kent [7]). The paper (Kent [11]) develops the notion of a FOLE table following the relational model (Codd [3]). The paper (Kent [12]) develops the notion of a FOLE relational database, thus providing the foundation for the semantics of first-order logical/relational database systems.

Equivalence.

The current paper “FOLE Equivalence” defines an interpretation of FOLE in terms of the transformational passage, first described in (Kent [8]), from the classification form of first-order logic to an equivalent interpretation form, thereby defining the formalism and semantics of first-order logical/relational database systems. Although the classification form follows the entity-relationship-attribute data model of Chen [2], the interpretation form incorporates the relational data model of Codd [3]. Relational operations are described in the paper (Kent [13]). The relational calculus will be discussed in a future paper.

2 Introduction.

This paper defines the equivalence between two forms of the first-order logical environment FOLE, the classification form and the interpretation form. Equivalence sits between the top of both forms, pictured briefly on the right, and more completely in Fig.1 in the preface §1. The classification form hierarchy (left hand side) consists of “The FOLE Foundation” at the bottom and “The FOLE Superstructure” at the top. The interpretation form hierarchy (right hand side) consists of “The FOLE Table” at the bottom and “The FOLE Database” at the top.

2.1 First Order Logical Environment

This paper relates two forms of the first order logic environment FOLE: the classification form and the interpretation form. These two forms are shown to be “informationally equivalent” ⁴⁴4See Prop. 12 in § A.1 of the paper [11] “The FOLE Table”. to each other. Both forms have their own advantages: the classification form allows formalism ⁵⁵5See the paper [10] “The ERA of FOLE: Superstructure”. to be easily defined, whereas the interpretation form allows relational operations ⁶⁶6See the paper [13] “Relational Operations in FOLE”. to be easily defined. The classification form of FOLE is realized in the notion of a (lax) sound logic, whereas the interpretation form of FOLE is realized in the notion of a relational database. To demonstrate the equivalence of the classification form with the interpretation form, (lax) sound logics and relational databases are shown to be in a reflective relationship (Fig. 2). Although a FOLE relational database can be taken as a whole, a FOLE sound logic resolves into the two parts of structure and specification, plus the relationship of satisfaction. ⁷⁷7The satisfaction relation corresponds to the “truth classification” in Barwise and Seligman [1], where the conceptual intent $\mathcal{M}^{\mathcal{S}}$ corresponds to the “theory of $\mathcal{M}$ ”.

In more detail (Tbl. 1), the classification form of FOLE is represented by a (lax) sound logic consisting of two components, a (lax) structure and an abstract specification, which are connected by a satisfaction relation. The (lax) structure consists of a (lax) entity classification, an attribute classification (typed domain), a schema, and one of the two equivalent descriptions: either a tabular map from predicates to tables; or a bridge consisting of an indexed collection of table tuple functions. The abstract specification is the same as a the database schema. Satisfaction is defined by table interpretation using constraints. The interpretation form of FOLE is represented by a relational database with constant type domain, a tabular interpretation diagram, whose projective components consist of a database schema, a key diagram, and a tuple bridge. The tabular interpretation diagram is equivalent to the satisfaction relation between the (lax) structure and the abstract specification. ⁸⁸8See (Key) Prop. 3 in § 5.3.

Figure 2: FOLE Equivalence

2.2 Overview.

\mathring{\mathrmbf{Snd}}\xleftarrow{\mathrmbfit{im}}\mathrmbf{Db}

: A database resolves into a sound logic: the specification is the database schema projection; the (lax) structure is the constraint-free aspect of a database; and tabular interpretation defines satisfaction.

\mathring{\mathrmbf{Snd}}\xrightarrow{\mathrmbfit{inc}}\mathrmbf{Db}

: A sound logic assembles a database: the specification provides (is the same as) the database schema; the (lax) structure provides a constraint-free interpretation consisting of a collection of tables indexed by predicates; and satisfaction defines the tabular interpretation.

Table 1: FOLE Equivalence in Brief

Briefly, § 3 defines some basic concepts of FOLE (formula, interpretation and satisfaction); § 4 defines structures and converts them to a lax variety; § 5 defines formal and abstract specifications, and satisfaction of specifications by structures; § 6 defines (lax) sound logics and converts these to relational databases; and § 7 defines relational databases and converts these to (lax) sound logics. In overview, Table 2 lists the figures and tables used in this paper.

Basic Concepts.

§ 3 reviews some basic concepts (Tbl. 3) of the FOLE logical environment from § 2 of the paper [10] “Superstructure”. This covers the concepts of formalism, tabular interpretation, and satisfaction. § 3.1 recapitulates the definition of formalism in [10]. Formalism is defined in terms of the logical Boolean operations and quantifiers using syntactic flow (Tbl. 4). § 3.2 extends to tables the definition of logical interpretation in [10] using Boolean operations within fibers and quantifier flow between fibers (Tbl. 5). It represents the syntactic flow operators of Tbl. 4 by their associated semantic flow operators (Tbl. 6). § 3.3 reviews the notion of satisfaction in [10], which links formalism and semantics via satisfaction. Satisfaction is defined for both sequents and constraints. Satisfaction is reflective (Fig. 3) between relations and tables.

Structures.

§ 4 reviews and extends the basic concepts of FOLE structure and structure morphism from § 4.3 of the paper [9]“Foundation”. In § 4.1, Def. 1 defines a FOLE structure with both a classification and interpretation form. Fig. 4 illustrates this idea. Note the global key sets used in the entity classification of this definition. In § 4.2, Def. 2 defines an extended notion of FOLE structure morphism by adding internal bridges. Fig. 5 illustrates this idea. Note the global key function in the entity infomorphism of this definition. § 4.3 defines a transition from strict to lax structures and structure morphisms. This is accomplished by changing the entity classification and entity infomorphism to lax versions, thus changing the global key sets and key function to local versions. Note 1, Prop. 1 (Key) and Cor. 1 define a step-by-step process for this transition. Fig. 6 illustrates the steps of this transition. § 4.4 and § 4.5 introduce the idea of lax structures and lax structure morphisms. We generalize to lax structures and lax structure morphisms by eliminating the global key sets and key functions. Def. 3 defines a lax FOLE structure in terms of either a tabular interpretation function or a tuple bridge. Prop. 2 shows that a lax structure is the same as the constraint-free aspect of a database. Def. 4 defines a (lax) structure morphism. Cor. 2 shows that a (lax) structure morphism defines a tabular interpretation bridge function. Fig. 7 illustrates a (lax) structure morphism.

Specifications.

§ 5 reviews and extends the notion of a FOLE specification. Formal FOLE specifications are covered in § 3.1 of the paper [10] “Superstructure”. Here we extend to abstract FOLE specifications. § 5.1 defines a formal specification in Def. 5 and an abstract specification in Def. 6. Every abstract specification is closely linked to a companion formal specification. § 5.2 defines a abstract specification morphism in Def. 7 and illustrates this in Fig. 8. Abstract specifications and morphisms are the same as database schemas and morphisms. § 5.3 defines specification satisfaction. Def. 8 defines satisfaction for formal specifications, whereas Def. 9 defines satisfaction for abstract specifications in terms of satisfaction for rheir formal companion. Assuming satisfaction holds, Def. 10 defines the abstract table passage as the composition of the object-identical companion passage, the inclusion into the structure conceptual intent, and the relation interpretation passage of Lem. 2 in § 3.3. Prop. 3 is key: it proves that satisfaction is equivalent to tabular interpretation, This is central, since it binds together the two parts of a sound logic, its structure and its specification. It underpins the core idea that sound logics are equivalent to relational databases. Fig. 9 illustrates and compares specification passages, both in general and with satisfaction. Tbl. 7 illustrates and compares specifications with the sound logics defined in § 6.

Sound Logics.

§ 6 reviews the notion of a FOLE sound logic. § 6.1 discusses sound logics. Def. 11 defines (lax) sound logics in terms of satisfaction between its two components: structure and abstract specification. Prop. 4 proves that any (lax) sound logic defines a relational database. Tbl. 8 lists and illustrates the various components of a (lax) sound logic. § 6.2 discusses sound logic morphisms. Def. 12 defines the notion of a (lax) sound logic morphism. Prop. 5 shows how (lax) sound logic morphisms preserve and link satisfaction between their source and target logics. The large figure Fig. 10 expands in detail the naturality used in this proposition. Prop. 6 proves that a (lax) sound logic morphism defines a database morphism. Thm. 6.1 proves existence of a passage from the context of (lax) FOLE sound logics to the context of FOLE relational databases. Tbl. 9 illustrates the components of a (lax) sound logic morphism.

Relational Databases.

§ 7 reviews the notion of a FOLE relational database. § 7.1 discusses FOLE relational databases. Def. 13 defines a relational database as an interpretation diagram from predicates to tables for a fixed type domain. Fig. 11 illustrates this definition. Def. 14 defines relational databases using table projection passages. Tbl. 10 lists the components of a FOLE relational database. Prop. 7 shows that the constraint-free aspect of a database is the same as a (lax) structure. Prop. 8 proves that a FOLE database defines a (lax) FOLE sound logic. § 7.2 discusses FOLE relational database morphisms. Def. 15 defines a database morphism to consist of a tabular passage between source/target predicate contexts, an infomorphism between source/target type domains, and a bridge connecting the source/target tabular interpretations. Fig. 12 illustrates this definition. Def. 16 defines relational database morphisms using table projection passages. Tbl. 11 lists and Fig. 14 illustrates the components of a FOLE relational database. Prop. 9 shows that the constraint-free aspect of a FOLE database morphism is the same as a (lax) FOLE structure morphism. Prop. 10 proves that a FOLE database morphism defines a (lax) FOLE sound logic morphism. Thm. 7.1 proves existence of a passage from the context of FOLE relational databases to the context of (lax) FOLE sound logics. Thm. 7.2 proves that the contexts of FOLE relational databases and FOLE (lax) sound logics are “informationally equivelent” by way of a reflection.

Appendix.

§ 0.A.1 lists the FOLE components used in this paper. Tbl. 12 in § 0.A.1 lists the equivalent and adjoint versions of FOLE bridges. Tbl. 13 in § 0.A.1 lists the FOLE Morphisms. § 0.A.2 reviews the concepts of classifications and infomorphisms. Both are extended to lax versions.

§1	Fig. 1 :	FOLE Architecture
§2	Fig. 2 :	FOLE Equivalence
§3	Fig. 3 :	Table-Relation Reflection
§4	Fig. 4 :	FOLE Structure
	Fig. 5 :	Structure Morphism
	Fig. 6 :	Transition
	Fig. 7 :	Lax Structure Morphism
§5	Fig. 8 :	Specification Morphisms
	Fig. 9 :	Specification Passages
§6	Fig. 10 :	Naturality Combined
§7	Fig. 11 :	Database: Type Domain
	Fig. 12 :	Database Morphism
	Fig. 13 :	Inclusion Bridge: Tables
	Fig. 14 :	Database Morphism: Type Domain
§0.A	Fig. 15 :	Infomorphism
	Fig. 16 :	Lax Infomorphism

§ 2	Tbl. 1 :	FOLE Equivalence in Brief
	Tbl. 2 :	Figures and Tables
§ 3	Tbl. 3 :	Basic Concepts
	Tbl. 4 :	Syntactic Flow
	Tbl. 5 :	Formula Interpretation
	Tbl. 6 :	Formal/Semantics Reflection
§ 5	Tbl. 7 :	Comparisons
§ 6	Tbl. 8 :	Sound Logic
	Tbl. 9 :	Sound Logic Morphism
§ 7	Tbl. 10 :	Relational Database
	Tbl. 11 :	Database Morphism
§ 0.A	Tbl. 12 :	FOLE Adjoint Bridges
	Tbl. 13 :	FOLE Morphisms
	Tbl. 14 :	Lax Infomorphisms

Table 2: Figures and Tables

3 Basic Concepts

The basic concepts of FOLE are listed in Tbl. 3. ⁹⁹9Satisfaction for (abstract) specifications is define in Def. 9 of § 5.3. Except for the formula interpretation in Tbl.5, we can refer all the formal material to the paper “The ERA of FOLE: Superstructure” [10].

§ 2.1	Formalism (formulas, sequents, constraints)
	Axioms (Tbl. 3)
§ 2.2	Semantics (formula interpretation)
	Formal/Semantics Reflection (Tbl. 6)
§ 2.3	Satisfaction (sequents, constraints)

Table 3: Basic Concepts

3.1 Formalism

Formulas.

Let $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ be a fixed schema with a set of entity types $R$ , a set of sorts (attribute types) $X$ and a signature function $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ . The set of entity types $R$ is partitioned $R=\bigcup_{{\langle{I,s}\rangle}\in\mathrmbf{List}(X)}R(I,s)$ into fibers, where $R(I,s){\;\subseteq\;}R$ is the fiber (subset) of all entity types with signature ${\langle{I,s}\rangle}$ . These are called ${\langle{I,s}\rangle}$ -ary entity types. ¹⁰¹⁰10This is a slight misnomer, since the signature of $r$ is $\sigma(R)={\langle{I,s}\rangle}$ , whereas the arity of $r$ is $\alpha(R)=I$ . Here, we follow the tuple, domain, and relation calculi from database theory, using logical operations to extend the set of basic entity types $R$ to a set of defined entity types $\widehat{R}$ called formulas or queries.

Formulas, which are defined entity types corresponding to queries, are constructed by using logical connectives within a fiber and logical flow along signature morphisms between fibers (Tbl. 4). ¹¹¹¹11An $\mathcal{S}$ -signature morphism ${\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}$ in $\mathrmbf{List}(X)$ is an arity function $I^{\prime}\xrightarrow{\,h\,}I$ that preserves signature $s^{\prime}=h{\,\cdot\,}s$ . ¹²¹²12The full version of FOLE (Kent [8]) defines syntactic flow along term vectors. Logical connectives on formulas express intuitive notions of natural language operations on the interpretation (extent, view) of formulas. These connectives include: conjunction, disjunction, negation, implication, etc. For any signature ${\langle{I,s}\rangle}$ , let $\widehat{R}(I,s)\subseteq\widehat{R}$ denote the set of all formulas with this signature. There are called ${\langle{I,s}\rangle}$ -ary formulas. The set of $\mathcal{S}$ -formulas is partitioned as $\widehat{R}=\bigcup_{{\langle{I,s}\rangle}\in\mathrmbf{List}(X)}\widehat{R}(I,s)$ .

fiber:

Let ${\langle{I,s}\rangle}$ be any signature. Any ${\langle{I,s}\rangle}$ -ary entity type (relation symbol) is an ${\langle{I,s}\rangle}$ -ary formula; that is, $R(I,s)\subseteq\widehat{R}(I,s)$ . For a pair of ${\langle{I,s}\rangle}$ -ary formulas $\varphi$ and $\psi$ , there are the following ${\langle{I,s}\rangle}$ -ary formulas: meet $(\varphi{\,\wedge\,}\psi)$ , join $(\varphi{\,\vee\,}\psi)$ , implication $(\varphi{\,\rightarrowtriangle\,}\psi)$ and difference $(\varphi{\,\setminus\,}\psi)$ . For ${\langle{I,s}\rangle}$ -ary formula $\varphi$ , there is an ${\langle{I,s}\rangle}$ -ary negation formula $\neg\varphi$ . There are top/bottom ${\langle{I,s}\rangle}$ -ary formulas $\top_{{\langle{I,s}\rangle}}$ and $\bot_{{\langle{I,s}\rangle}}$ .
flow:

Let ${\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}$ be any signature morphism. For ${\langle{I,s}\rangle}$ -ary formula $\varphi$ , there are ${\langle{I^{\prime},s^{\prime}}\rangle}$ -ary existentially/universally quantified formulas ${\scriptstyle\sum}_{h}(\varphi)$ and ${\scriptstyle\prod}_{h}(\varphi)$ . ¹³¹³13For any index $i\in I$ , quantification for the complement inclusion signature function ${\langle{I\setminus\{i\},s^{\prime}}\rangle}\xrightarrow{\text{inc}_{i}}{\langle{I,s}\rangle}$ gives the traditional syntactic quantifiers $\forall_{i}\varphi,\exists_{i}{\varphi}$ . For an ${\langle{I^{\prime},s^{\prime}}\rangle}$ -ary formula $\varphi^{\prime}$ , there is an ${\langle{I,s}\rangle}$ -ary substitution formula ${h}^{\ast}(\varphi^{\prime})=\varphi^{\prime}(t)$ .

$\begin{array}[]{c}{\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}\\ {\begin{picture}(120.0,60.0)(0.0,-25.0)\put(0.0,0.0){\makebox(0.0,0.0)[]{\footnotesize{$\widehat{R}(I^{\prime},s^{\prime})$}}} \put(120.0,0.0){\makebox(0.0,0.0)[]{\footnotesize{$\widehat{R}(I,s)$}}} \put(60.0,20.0){\makebox(0.0,0.0)[]{\scriptsize{${\scriptstyle\sum}_{{h}}$}}} \put(62.0,2.0){\makebox(0.0,0.0)[]{\scriptsize{${h}^{\ast}$}}} \put(60.0,-22.0){\makebox(0.0,0.0)[]{\scriptsize{${\scriptstyle\prod}_{{h}}$}}} \put(85.0,12.0){\vector(-1,0){50.0}} \qbezier(35.0,0.0)(43.0,0.0)(51.0,0.0)\qbezier(69.0,0.0)(77.0,0.0)(85.0,0.0)\put(85.0,0.0){\vector(1,0){0.0}} \put(85.0,-12.0){\vector(-1,0){50.0}} \end{picture}}\end{array}$

Table 4: Syntactic Flow

In general, we regard formulas to be constructed entities or queries (defining views and interpretations; i.e., relations/tables), not assertions. Contrast this with the use of “asserted formulas” below. For example, in a corporation data model the conjunction $(\mathtt{Salaried}{\,\wedge\,}\mathtt{Married})$ is not an assertion, but a constructed entity type or query that defines the view “salaried employees that are married”. Formulas form a schema $\widehat{\mathcal{S}}={\langle{\widehat{R},\widehat{\sigma},X}\rangle}$ that extends $\mathcal{S}$ with $\mathcal{S}$ -formulas as entity types: with the inductive definitions above, the set of entity types is extended to a set of logical formulas $R\xhookrightarrow{\mathrmit{inc}_{\mathcal{S}}}\widehat{R}$ , and the entity type signature function is extended to a formula signature function $\widehat{R}\xrightarrow{\;\widehat{\sigma}\;}\mathrmbf{List}(X)$ with $\sigma=\mathrmit{inc}_{\mathcal{S}}{\;\cdot\;}\widehat{\sigma}$ .

Sequents.

To make an assertion about things, we use a sequent. Let $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ be a schema. A (binary) $\mathcal{S}$ -sequent ¹⁴¹⁴14Since FOLE formulas are not just types, but are constructed using, inter alia, conjunction and disjunction operations, we can restrict attention to binary sequents. is a pair of formulas $(\varphi,\psi){\,\in\,}\widehat{R}{\,\times}\widehat{R}$ with the same signature $\widehat{\sigma}(\varphi)={\langle{I,s}\rangle}=\widehat{\sigma}(\psi)$ . To be explicit that we are making an assertion, we use the turnstile notation $\varphi{\;\vdash\;}\psi$ for a sequent. Then, we are claiming that a specialization-generalization relationship exists between the formulas $\varphi$ and $\psi$ . A asserted sequent $\varphi{\;\vdash\;}\psi$ expresses interpretation widening, with the interpretation (view) of $\varphi$ required to be within the interpretation (view) of $\psi$ . An asserted formula $\varphi\in\widehat{R}$ can be identified with the sequent $\top{\;\vdash\;}\varphi$ in $\widehat{R}{\,\times}\widehat{R}$ , which asserts the universal view “all entities” of signature $\sigma(\varphi)={\langle{I,s}\rangle}$ . Hence, from an entailment viewpoint we can say that “formulas are sequents”. In the opposite direction, there is an enfolding map $\widehat{R}{\,\times}\widehat{R}\rightarrow\widehat{R}$ that maps $\mathcal{S}$ -sequents to $\mathcal{S}$ -formulas $({\varphi}{\;\vdash\;}{\psi})\mapsto(\varphi{\,\rightarrowtriangle\,}\psi)$ . The axioms in Tbl. 3 of the paper [10] make sequents into an order. Let $\mathrmbf{Con}_{\mathcal{S}}(I,s)={\langle{\widehat{R}(I,s),\vdash}\rangle}$ denote the fiber preorder of $\mathcal{S}$ -formulas.

Constraints.

Sequents only connect formulas within a particular fiber: an $\mathcal{S}$ -sequent $\varphi{\;\vdash\;}\psi$ is between two formulas with the same signature $\widehat{\sigma}(\varphi)={\langle{I,s}\rangle}=\widehat{\sigma}(\psi)$ , and hence between elements in the same fiber $\varphi,\psi{\;\in\;}\widehat{R}(I,s)$ . We now define a useful notion that connects formulas across fibers. An $\mathcal{S}$ -constraint $\varphi^{\prime}{\,\xrightarrow{h\,}\,}\varphi$ consists of a signature morphism $\widehat{\sigma}(\varphi^{\prime})={\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}=\widehat{\sigma}(\varphi)$ and a binary sequent ${\scriptstyle\sum}_{h}(\varphi){\;\vdash\;}\varphi^{\prime}$ in $\mathrmbf{Con}_{\mathcal{S}}(I^{\prime},s^{\prime})$ , or equivalently by the axioms in Tbl. 3 of the paper [10], a binary sequent $\varphi{\;\vdash\;}{h}^{\ast}(\varphi^{\prime})$ in $\mathrmbf{Con}_{\mathcal{S}}(I,s)$ . Hence, a constraint requires that the interpretation of the $h^{\mathrm{th}}$ -projection of $\varphi$ be within the interpretation of $\varphi^{\prime}$ , or equivalently, that the interpretation of $\varphi$ be within the interpretation of the $h^{\mathrm{th}}$ -substitution of $\varphi^{\prime}$ . ¹⁵¹⁵15In some sense, this formula/constraint approach to formalism turns the tuple calculus upside down, with atoms in the tuple calculus becoming constraints here.

Given any schema $\mathcal{S}$ , an $\mathcal{S}$ -constraint ${\varphi^{\prime}}\xrightarrow{h}{\varphi}$ has source formula ${\varphi^{\prime}}$ and target formula ${\varphi}$ . Constraints are closed under composition: ${\varphi^{\prime\prime}}\xrightarrow{h^{\prime}}{\varphi^{\prime}}\xrightarrow{h}{\varphi}={\varphi^{\prime\prime}}\xrightarrow{h^{\prime}{\,\cdot\,}h}{\varphi}$ . Let $\mathrmbf{Cons}(\mathcal{S})$ ¹⁶¹⁶16 $\mathrmbf{Cons}(\mathcal{S})$ , which stands for “ $\mathcal{S}$ -constraints”, was defined in the paper [10]. denote the mathematical context, whose set of objects are $\mathcal{S}$ -formulas and whose set of morphisms are $\mathcal{S}$ -constraints. This context is fibered over the projection passage $\mathrmbf{Cons}(\mathcal{S})\rightarrow\mathrmbf{List}(X):\bigl{(}\varphi^{\prime}{\,\xrightarrow{h\,}\,}\varphi\bigr{)}\mapsto\bigl{(}{\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}\bigr{)}$ . Formula formation is idempotent: $\widehat{{\widehat{R}}}=\widehat{R}$ and $\mathrmbf{Cons}(\widehat{\mathcal{S}})=\mathrmbf{Cons}(\mathcal{S})$ . ¹⁷¹⁷17Formulas form a schema $\widehat{\mathcal{S}}={\langle{\widehat{R},\widehat{\sigma},X}\rangle}$ that extends $\mathcal{S}$ with $\mathcal{S}$ -formulas as entity types (relation names): by induction, the set of entity types is extended to a set of logical formulas $R\xhookrightarrow{\mathrmit{inc}_{\mathcal{S}}}\widehat{R}$ , and the entity type signature function is extended to a formula signature function $\widehat{R}\xrightarrow{\;\widehat{\sigma}\;}\mathrmbf{List}(X)$ with $\sigma=\mathrmit{inc}_{\mathcal{S}}{\;\cdot\;}\widehat{\sigma}$ .

Sequents are special cases of constraints: a sequent $\varphi^{\prime}{\;\vdash\;}\varphi$ asserts a constraint ${\varphi}\xrightarrow{1}{\varphi^{\prime}}$ that uses an identity signature morphism. ¹⁸¹⁸18A constraint in the fiber $\mathrmbf{Con}_{\mathcal{S}}(I,s)$ uses an identity signature morphism ${\varphi}\xrightarrow{1}{\varphi^{\prime}}$ , and hence is a sequent $\varphi^{\prime}{\;\vdash\;}\varphi$ . Since an asserted formula $\varphi$ can be identified with the sequent $\top{\;\vdash\;}\varphi$ , it can also be identified with the constraint ${\varphi}\xrightarrow{1}{\top}$ . Thus, from an entailment viewpoint we can say that “formulas are sequents are constraints”. In the opposite direction, there are enfolding maps that map $\mathcal{S}$ -constraints to $\mathcal{S}$ -formulas: either $\bigl{(}{\varphi^{\prime}}\xrightarrow{h}{\varphi}\bigr{)}\mapsto\bigl{(}{\scriptstyle\sum}_{h}(\varphi){\,\rightarrowtriangle\,}\varphi^{\prime}\bigr{)}$ with signature ${\langle{I^{\prime},s^{\prime}}\rangle}$ , or $\bigl{(}{\varphi^{\prime}}\xrightarrow{h}{\varphi}\bigr{)}\mapsto\bigl{(}\varphi{\,\rightarrowtriangle\,}{h}^{\ast}(\varphi^{\prime})\bigr{)}$ with signature ${\langle{I,s}\rangle}$ .

3.2 Interpretation

The logical semantics of a structure $\mathcal{M}$ resides in its core, which is defined by its formula interpretation function

\mathrmbfit{T}_{\mathcal{M}}:\widehat{R}\rightarrow\mathrmbf{Tbl}(\mathcal{A}).

(1)

The formula interpretation function, which extends the traditional interpretation function $T_{\mathcal{M}}:R\rightarrow\mathrmbf{Tbl}(\mathcal{A})$ of a structure $\mathcal{M}$ (Def. 1 in § 4), is defined in Tbl. 5 by induction within fibers and flow between fibers. To respect the logical semantics, the formal flow operators ( ${\scriptstyle\sum}_{h}$ , ${\scriptstyle\prod}_{h}$ , ${h}^{\ast}$ ) for existential/universal quantification and substitution reflect the semantic flow operators ( ${\scriptstyle\sum}_{h}$ , ${\scriptstyle\prod}_{h}$ , ${h}^{\ast}$ ) via interpretation (Tbl. 6). ¹⁹¹⁹19The morphic aspect of Tbl. 6 anticipates the definition of satisfaction in §.3.3: for sequents within the fibers $\mathrmbfit{T}_{\mathcal{A}}(I,s)$ and for constraints using flow between fibers; ${\bigl{\langle}{{\scriptscriptstyle\sum}_{h}{\;\dashv\;}{h}^{\ast}{\;\dashv\;}{\scriptstyle\prod}_{{h}}\bigr{\rangle}}}:\mathrmbf{Tbl}_{\mathcal{A}}(I^{\prime},s^{\prime}){\;\leftrightarrows\;}\mathrmbf{Tbl}_{\mathcal{A}}(I,s)$ .

fiber:: For each signature ${\langle{I,s}\rangle}{\,\in\,}\mathrmbf{List}(X)$ , the fiber function $\widehat{R}(I,s)\xrightarrow{\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I\!,s}\rangle}}}\mathrmbf{Tbl}_{\mathcal{A}}(I,s)$ is defined in the top part of Tbl. 5 by induction on formulas. At the base step (first line in the top of Tbl. 5), it defines the formula interpretation of an entity type $r\in\widehat{R}$ as the traditional interpretation of that type: the $\mathcal{A}$ -table $T_{\mathcal{M}}(r)={\langle{\sigma(r),\mathrmbfit{K}(r),\tau_{r}}\rangle}\in\mathrmbf{Tbl}(\mathcal{A})$ (Fig. 4 of §4). At the induction step (remaining lines in the top of Tbl. 5), it represents the logical operations by their associated boolean operations: meet of interpretations for conjunction, join of interpretations for disjunction, etc.; see the boolean operations defined in § 3.2 of the paper “Relational Operations in FOLE” [13].
flow:: (bottom Tbl. 5), It represents the syntactic flow operators in Tbl. 4 by their associated semantic flow operators; see the adjoint flow for fixed type domain $\mathcal{A}$ defined in § 3.3.1 of the paper “Relational Operations in FOLE” [13]. ²⁰²⁰20The paper [13] used only two of the three operators in the fiber adjunction of tables (2) defined by composition/pullback: the left adjoint existential operation (called projection) and the right adjoint substitution or inverse image operation (called inflation). The function $\widehat{R}\xrightarrow{\mathrmbfit{T}_{\mathcal{M}}}\mathrmbf{Tbl}(\mathcal{A})$ is the parallel combination of its fiber functions $\biggl{\{}\widehat{R}(I,s)\xrightarrow{\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I\!,s}\rangle}}}\mathrmbf{Tbl}_{\mathcal{A}}(I,s)\mid{\langle{I,s}\rangle}{\,\in\,}\mathrmbf{List}(X)\biggr{\}}$ defined above. The function $\mathrmbfit{T}_{\mathcal{M}}$ is defined in terms of these fiber functions and the flow operators.

fiber: signature ${\langle{I,s}\rangle}$ with extent (tuple set) $\mathrmbfit{tup}_{\mathcal{A}}(I,s){\,=\,}\prod_{i\in{I}}\,\mathcal{A}_{s_{\!i}}$
operator	definition $\mathrmbfit{T}_{\mathcal{M}}(\varphi)\in\mathrmbf{Tbl}_{\mathcal{A}}(I,s)=\bigl{(}\mathrmbf{Set}{\,\downarrow\,}\mathrmbfit{tup}_{\mathcal{A}}(I,s)\bigr{)}$
entity type	$\mathrmbfit{T}_{\mathcal{M}}(r)=T_{\mathcal{M}}(r)={\langle{\sigma(r),\mathrmbfit{K}(r),\tau_{r}}\rangle}$ $r{\,\in\,}R(I,s)\subseteq\widehat{R}(I,s)$
meet	$\mathrmbfit{T}_{\mathcal{M}}(\varphi{\,\wedge\,}\psi)=\mathrmbfit{T}_{\mathcal{M}}(\varphi){\,\wedge\,}\mathrmbfit{T}_{\mathcal{M}}(\psi)$ $\varphi,\psi{\,\in\,}\widehat{R}(I,s)$
join	$\mathrmbfit{T}_{\mathcal{M}}(\varphi{\,\vee\,}\psi)=\mathrmbfit{T}_{\mathcal{M}}(\varphi){\,\vee\,}\mathrmbfit{T}_{\mathcal{M}}(\psi)$
top	$\mathrmbfit{T}_{\mathcal{M}}({\scriptstyle\top_{{\langle{I,s}\rangle}}})={\langle{\mathrmbfit{tup}_{\mathcal{A}}(I,s),1}\rangle}$ terminal table
bottom	$\mathrmbfit{T}_{\mathcal{M}}({\scriptstyle\bot_{{\langle{I,s}\rangle}}})={\langle{\emptyset,0}\rangle}$ initial table
negation	$\mathrmbfit{T}_{\mathcal{M}}(\neg\varphi)=\mathrmbfit{T}_{\mathcal{M}}(\top_{{\langle{I,s}\rangle}}{\,\setminus\,}\varphi)=\mathrmbfit{T}_{\mathcal{M}}(\top_{{\langle{I,s}\rangle}}){-}\mathrmbfit{T}_{\mathcal{M}}(\varphi)$
implication	$\mathrmbfit{T}_{\mathcal{M}}(\varphi{\,\rightarrowtriangle\,}\psi)=\mathrmbfit{T}_{\mathcal{M}}(\varphi){\,\rightarrowtriangle\,}\mathrmbfit{T}_{\mathcal{M}}(\psi)=(\neg\mathrmbfit{T}_{\mathcal{M}}(\varphi)){\,\vee\,}\mathrmbfit{T}_{\mathcal{M}}(\psi)$
difference	$\mathrmbfit{T}_{\mathcal{M}}(\varphi{\,\setminus\,}\psi)=\mathrmbfit{T}_{\mathcal{M}}(\varphi){-}\mathrmbfit{T}_{\mathcal{M}}(\psi)=\mathrmbfit{T}_{\mathcal{M}}(\varphi){\,\wedge\,}(\neg\mathrmbfit{T}_{\mathcal{M}}(\psi))$
flow: signature morphism ${\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}$
with tuple map $\mathrmbfit{tup}_{\mathcal{A}}(I^{\prime},s^{\prime})\xleftarrow{\mathrmbfit{tup}_{\mathcal{A}}(h)}\mathrmbfit{tup}_{\mathcal{A}}(I,s)$
operator	definition
existential	$\mathrmbfit{T}_{\mathcal{M}}({\scriptstyle\sum}_{h}(\varphi))={\scriptstyle\sum}_{h}(\mathrmbfit{T}_{\mathcal{M}}(\varphi))$ $\varphi{\,\in\,}\widehat{R}(I,s)$
universal	$\mathrmbfit{T}_{\mathcal{M}}({\scriptstyle\prod}_{h}(\varphi))={\scriptstyle\prod}_{h}(\mathrmbfit{T}_{\mathcal{M}}(\varphi))$
substitution	$\mathrmbfit{T}_{\mathcal{M}}({h}^{\ast}(\varphi^{\prime}))={h}^{\ast}(\mathrmbfit{I}_{\mathcal{M}}(\varphi^{\prime}))$ $\varphi^{\prime}{\,\in\,}\widehat{R}(I^{\prime},s^{\prime})$

Table 5: Formula Interpretation

\begin{array}[b]{l}{\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}\\ \mathrmbfit{tup}_{\mathcal{A}}(I^{\prime},s^{\prime})\xleftarrow{\mathrmbfit{tup}(h)}\mathrmbfit{tup}_{\mathcal{A}}(I,s)\end{array}

\begin{array}[b]{|@{\hspace{5pt}}l@{\hspace{2pt}}|}\hline\cr\hskip 5.0pt\lx@intercol{\scriptstyle\sum}_{{h}}\dashv{h}^{\ast}\dashv{\scriptstyle\prod}_{{h}}\hfil\hskip 2.0\\ \hline\cr\hskip 5.0pt\lx@intercol{\scriptstyle\sum}_{{h}}\circ\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I^{\prime}\!,s^{\prime}}\rangle}}=\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I\!,s}\rangle}}\circ{\scriptstyle\sum}_{{h}}\hfil\hskip 2.0\\ \hskip 5.0pt\lx@intercol{h}^{\ast}\circ\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I\!,s}\rangle}}=\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I^{\prime}\!,s^{\prime}}\rangle}}\circ{h}^{\ast}\hfil\hskip 2.0\\ \hskip 5.0pt\lx@intercol{\scriptstyle\prod}_{{h}}\circ\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I^{\prime}\!,s^{\prime}}\rangle}}=\mathrmbfit{T}^{\mathcal{M}}_{{\langle{I\!,s}\rangle}}\circ{\scriptstyle\prod}_{{h}}\hfil\hskip 2.0\\ \hline\cr\end{array}

Table 6: Formal/Semantics Reflection

3.3 Satisfaction.

Satisfaction is a fundamental classification between formalism and semantics. The atom of formalism used in satisfaction is the FOLE constraint, whereas the atom of semantics used in satisfaction is the FOLE structure. Satisfaction is defined in terms of the table formula interpretation function $\mathrmbfit{T}_{\mathcal{M}}:\widehat{R}\rightarrow\mathrmbf{Tbl}(\mathcal{A})$ of § 3.2 and the associated the relation formula interpretation function $\mathrmbfit{R}_{\mathcal{M}}:\widehat{R}\rightarrow\mathrmbf{Rel}(\mathcal{A})$ . ²¹²¹21Denoted by $\mathrmbfit{I}_{\mathcal{M}}:\widehat{R}\rightarrow\mathrmbf{Rel}(\mathcal{A})$ in § 2,2,1 of the paper “The ERA of FOLE: Superstructure” [10] Assume that we are given a structure schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a set of predicate symbols $R$ and a signature (header) map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ .

Sequent Satisfaction.

A (lax) $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies a formal $\mathcal{S}$ -sequent $\varphi{\;\vdash\;}\varphi^{\prime}$ , for a pair of formulas $(\varphi,\varphi^{\prime}){\,\in\,}\widehat{R}{\,\times}\widehat{R}$ with the same signature $\widehat{\sigma}(\varphi)={\langle{I,s}\rangle}=\widehat{\sigma}(\varphi^{\prime})$ , when the interpretation widening of views asserted by the sequent actually holds in $\mathcal{M}$ :

$\underset{\text{in}\;\mathrmbf{Rel}_{\mathcal{A}}(I,s)}{\mathrmbfit{R}_{\mathcal{M}}(\varphi){\;\subseteq\;}\mathrmbfit{R}_{\mathcal{M}}(\varphi^{\prime})}\;\;\;\text{\text@underline{reflectively}}\;\;\;\underset{\text{in}\;\mathrmbf{Tbl}_{\mathcal{A}}(I,s)}{\mathrmbfit{T}_{\mathcal{M}}(\varphi){\;\xrightarrow{\;k\;}\;}\mathrmbfit{T}_{\mathcal{M}}(\varphi^{\prime})}$ ²²²²22See the formal/semantics reflection defined in § A.1 of the paper “The FOLE Table” [11] and in § 3.1 of the paper “Relational Operations in FOLE” [13]..

Satisfaction is symbolized either by $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi{\;\vdash\;}\varphi^{\prime})$ or by $\varphi{\;\vdash_{\mathcal{M}}\;}\varphi^{\prime}$ . For each signature ${\langle{I,s}\rangle}\in\mathrmbf{List}(X)$ , satisfaction defines the fiber order ${\langle{\widehat{R}(I,s),\leq_{\mathcal{M}}}\rangle}$ , where $\varphi{\;\leq_{\mathcal{M}}\;}\varphi^{\prime}$ when $\varphi{\;\vdash_{\mathcal{M}}\;}\varphi^{\prime}$ for any two formulas $\varphi,\varphi^{\prime}\in{\widehat{R}}(I,s)$ .

Figure 3: Table-Relation Reflection

Constraint Satisfaction.

A (lax) $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies a formal $\mathcal{S}$ -constraint $\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi$ , for a pair of formulas $(\varphi^{\prime},\varphi){\,\in\,}\widehat{R}{\,\times}\widehat{R}$ connected by a signature morphism $\widehat{\sigma}(\varphi^{\prime})={\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{h}{\langle{I,s}\rangle}=\widehat{\sigma}(\varphi)$ , when the following equivalence holds

(3)

reflectively ${}^{\ref{reflection}}$ (visualized in Fig. 3)

(4)

Satisfaction is symbolized by $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi)$ .

Lemma 1

A (lax) $\mathcal{S}$ -structure $\mathcal{M}$ determines a mathematical context $\mathcal{M}^{\mathcal{S}}{\;\sqsubseteq\;}\mathrmbf{Cons}(\mathcal{S})$ , called the conceptual intent of $\mathcal{M}$ , whose objects are $\mathcal{S}$ -formulas and whose morphisms are $\mathcal{S}$ -constraints satisfied by $\mathcal{M}$ . The ${\langle{I,s}\rangle}^{\text{th}}$ fiber is the order ${\mathcal{M}^{\mathcal{S}}(I,s)}={\langle{\widehat{R}(I,s),\geq_{\mathcal{M}}}\rangle}$ . ²³²³23The satisfaction relation corresponds to the “truth classification” in Barwise and Seligman [1], where the conceptual intent $\mathcal{M}^{\mathcal{S}}$ corresponds to the “theory of $\mathcal{M}$ ”.

Proof

$\mathcal{M}^{\mathcal{S}}$ is closed under constraint identities and constraint composition.
1: $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi{\;\xrightarrow{1}\;}\varphi)$ , and 2: if $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi^{\prime\prime}{\;\xrightarrow{h^{\prime}}\;}\varphi^{\prime})$ and $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi)$ , then $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi^{\prime\prime}{\;\xrightarrow{h^{\prime}{\,\cdot\,}h}\;}\varphi)$ , since $\varphi^{\prime\prime}{\;\geq_{\mathcal{M}}\;}{\scriptstyle\sum}_{h^{\prime}}(\varphi^{\prime})$ and $\varphi^{\prime}{\;\geq_{\mathcal{M}}\;}{\scriptstyle\sum}_{h}(\varphi)$ implies $\varphi^{\prime\prime}{\;\geq_{\mathcal{M}}\;}{\scriptstyle\sum}_{h^{\prime}}({\scriptstyle\sum}_{h}(\varphi))={\scriptstyle\sum}_{h^{\prime}{\,\cdot\,}h}(\varphi)$ .

Lemma 2

For any structure $\mathcal{M}$ , there is a relation interpretation passage and a table interpretation graph morphism, ²⁴²⁴24Relational interpretation is closed under composition; tabular interpretation is closed under composition only up to key equivalence.

(5)

which extend the formula interpretation function $\mathrmbfit{T}_{\mathcal{M}}:\widehat{R}\rightarrow\mathrmbf{Tbl}(\mathcal{A})$ of § 3.2, and hence the structure interpretation function $T_{\mathcal{M}}:R\rightarrow\mathrmbf{Tbl}(\mathcal{A})$ of § 4.

Proof

objects:: An $\mathcal{S}$ -formula $\varphi\in\mathcal{M}^{\mathcal{S}}(I,s)={\langle{\widehat{R}(I,s),\leq_{\mathcal{M}}}\rangle}$ with $\mathcal{S}$ -signature ${\langle{I,s}\rangle}$ is mapped to an $\mathcal{A}$ -table $\mathrmbfit{T}_{\mathcal{M}}(\varphi)={\langle{I,s,K,t}\rangle}$ defined by induction in the top part of Tbl. 5 in in § 3.2. Reflectively, the formula $\varphi$ is mapped to an $\mathcal{A}$ -relation $\mathrmbfit{R}_{\mathcal{M}}(\varphi)={\langle{I,s,{\wp}t(K)}\rangle}$ .
morphisms:: An $\mathcal{S}$ -constraint $\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi$ satisfied by the $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ , $\mathcal{M}{\;\models_{\mathcal{S}}\;}(\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi)$ , is mapped by constraint satisfaction to the $\mathrmbf{Tbl}(\mathcal{A})$ -morphism $\mathrmbfit{T}_{\mathcal{M}}(\varphi^{\prime})=\mathcal{T}^{\prime}={\langle{I^{\prime},s^{\prime},\mathrmbfit{K}(\varphi^{\prime}),t_{\varphi^{\prime}}}\rangle}\xleftarrow{\langle{h,k}\rangle}{\langle{I,s,\mathrmbfit{K}(\varphi),t_{\varphi}}\rangle}=\mathcal{T}=\mathrmbfit{T}_{\mathcal{M}}(\varphi)$ with indexing $X$ -sorted signature morphism ${\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow{\;h\;}{\langle{I,s}\rangle}$ and a key function $\mathrmbfit{K}(\varphi^{\prime})\xleftarrow{\,k\,}\mathrmbfit{K}(\varphi)$ ²⁵²⁵25Defined by choice. However, the choice for a composite signature morphism is not identical to the composition of the component choices; only equivalent. satisfying either of the adjoint fiber morphisms in Disp.4 leading to the naturality condition $k{\;\cdot\;}t_{\varphi^{\prime}}=t_{\varphi}{\;\cdot\;}\mathrmbfit{tup}_{\mathcal{A}}(h)$ and visualized in Fig. 3. Reflectively, the constraint $\varphi^{\prime}{\;\xrightarrow{h}\;}\varphi$ is mapped to an $\mathcal{A}$ -relation morphism $\mathrmbfit{R}_{\mathcal{M}}(\varphi^{\prime})=\mathcal{R}^{\prime}={\langle{I^{\prime},s^{\prime},{\wp}t^{\prime}_{\varphi^{\prime}}(\mathrmbfit{K}(\varphi^{\prime}))}\rangle}\xleftarrow{\langle{h,r}\rangle}{\langle{I,s,{\wp}t_{\varphi}(\mathrmbfit{K}(\varphi))}\rangle}=\mathcal{R}=\mathrmbfit{R}_{\mathcal{M}}(\varphi)$ satisfying either of the adjoint fiber orderings in Disp.3 leading to the naturality condition $r{\;\cdot\;}i_{\varphi^{\prime}}=i_{\varphi}{\;\cdot\;}\mathrmbfit{tup}_{\mathcal{A}}(h)$ and visualized in Fig. 3.

4 FOLE Structures.

We define two forms of structures and structure morphisms: a classification (strict) form and an interpretation (lax) form.

4.1 Structures.

Assume that we are given a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a set of predicate symbols $R$ and a signature (header) map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ .

Definition 1

An $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ (LHS Fig. 4) consists of an entity classification $\mathcal{E}={\langle{R,K,\models_{\mathcal{E}}}\rangle}$ of predicate symbols $R$ and keys $K$ , an attribute classification (typed domain) $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ of sorts $X$ and data values $Y$ , and a list designation ${\langle{\sigma,\tau}\rangle}:\mathcal{E}\rightrightarrows\mathrmbf{List}(\mathcal{A})$ with signature map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ , tuple map $K\xrightarrow{\tau}\mathrmbf{List}(Y)$ and defining condition $k{\;\models_{\mathcal{E}}\;}r$ implies $\tau(k){\;\models_{\mathrmbf{List}(\mathcal{A})}\;}\sigma(r)$ . ²⁶²⁶26In more detail, if entity $k{\,\in\,}K$ is of type $r{\,\in\,}R$ , then the description tuple $\tau(k)={\langle{J,t}\rangle}$ is the same “size” ( $J=I$ ) as the signature $\sigma(r)={\langle{I,s}\rangle}$ and for each index $n\in I$ the data value $t_{n}$ is of sort $s_{n}$ .

Projections define the type hypergraph (schema) $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ , and an instance hypergraph (universe) $\mathcal{U}={\langle{K,\tau,Y}\rangle}$ .

classification form

interpretation form (passage)

interpretation form (bridge)

Figure 4: FOLE Structure

By dropping the global key set $K$ , the entity classification $\mathcal{E}={\langle{R,K,\models_{\mathcal{E}}}\rangle}$ can be regarded (RHS Fig. 4) as a set-valued function $\mathrmbfit{K}=R\xrightarrow[\mathrmbfit{K}]{\mathrmbfit{ext}_{\mathcal{E}}}{\wp}K\subseteq\mathrmbf{Set}$ ; that is, as an indexed collection $\mathcal{E}={\langle{R,\mathrmbfit{K}}\rangle}$ of subsets of keys $\bigl{\{}\mathrmbfit{ext}_{\mathcal{E}}(r)=\mathrmbfit{K}(r)\subseteq\mathrmbf{Set}\mid r\in R\bigr{\}}$ . The defining condition of the list designation demonstrates that a structure can be regarded (MID Fig. 4) as a table-valued function $R\xrightarrow{T_{\mathcal{M}}}\mathrmbf{Tbl}(\mathcal{A})$ ; that is, as an $R$ -indexed collection of $\mathcal{A}$ -tables $T_{\mathcal{M}}(r)={\langle{\sigma(r),\mathrmbfit{K}(r),\tau_{r}}\rangle}$ , whose tuple maps $\bigl{\{}\mathrmbfit{K}(r)\xrightarrow{\tau_{r}}\mathrmbfit{tup}_{\mathcal{A}}(\sigma(r))\mid r\in R\bigr{\}}$ are restrictions of the tuple map $K\xrightarrow{\tau}\mathrmbf{List}(Y)$ . Here, an entity type (predicate symbol) $r\in R$ is interpreted as the $\mathcal{A}$ -table $T_{\mathcal{M}}(r)={\langle{\sigma(r),\mathrmbfit{K}(r),\tau_{r}}\rangle}\in\mathrmbf{Tbl}(\mathcal{A})$ , consisting of the $X$ -signature $\sigma(r)\in\mathrmbf{List}(X)$ , the key set $\mathrmbfit{K}(r)=\mathrmbfit{ext}_{\mathcal{E}}(r)\subseteq K$ , and the tuple function $\mathrmbfit{K}(r)\xrightarrow{\tau_{r}}\mathrmbfit{tup}_{\mathcal{A}}(\sigma(r))$ , which is a restriction of the tuple function $K\xrightarrow{\tau}\mathrmbf{List}(Y)$ . The list classification $\mathrmbf{List}(\mathcal{A})={\langle{\mathrmbf{List}(X),\mathrmbf{List}(Y),\models_{\mathrmbf{List}(\mathcal{A})}}\rangle}$ can alternatively be regarded (RHS Fig. 4) (Fig. 4 of the paper [9]) as a set-valued function $\mathrmbf{List}(X)\xrightarrow[\mathrmbfit{tup}_{\mathcal{A}}]{\mathrmbfit{ext}_{\mathrmbf{List}(\mathcal{A})}}{\wp}\mathrmbf{List}(Y)$ ; that is, as an indexed collection $\mathrmbf{List}(\mathcal{A})={\langle{\mathrmbf{List}(X),\mathrmbfit{tup}_{\mathcal{A}},\mathrmbf{List}(Y)}\rangle}$ of subsets of tuples $\bigl{\{}\mathrmbfit{ext}_{\mathrmbf{List}(\mathcal{A})}(I,s)=\mathrmbfit{tup}_{\mathcal{A}}(I,s)\subseteq\mathrmbf{List}(Y)\mid(I,s)\in\mathrmbf{List}(X)\bigr{\}}$ . The bridge $K\xRightarrow{\tau_{{\scriptscriptstyle{\llcorner}}}\;}{\wp}\tau{\;\circ\;}\mathrmbfit{inc}$ provides “restrictions” of the bridge $K\xRightarrow{\;\tau\;}\mathrmbf{List}(Y)$ to subsets of $K$ .

4.2 Structure Morphisms.

Assume that we are given a schema morphism (Tbl. 13 in § 0.A.1)

\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{\;{\langle{r,\grave{\varphi},f}\rangle}\;}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}

(6)

consisting of a function on relation symbols $R_{2}\xrightarrow{\,\mathrmit{r}\;}R_{1}$ , a sort function $X_{2}\xrightarrow{f}\mathcal{X}_{1}$ , and a schema bridge $\sigma_{2}{\;\cdot\;}{\scriptstyle\sum}_{f}{\;\xRightarrow{\,\grave{\varphi}\;\,}\;}r{\;\cdot\;}\sigma_{1}$ , whose $r_{2}^{\text{th}}$ -component is the morphism ${{\scriptstyle\sum}_{f}(\sigma_{2}(r_{2}))}\xrightarrow[h]{\grave{\varphi}_{r_{2}}}{\sigma_{1}(r(r_{2}))}$ in $\mathrmbf{List}(X_{1})$ .

Definition 2

A structure morphism $\mathcal{M}_{2}\xrightleftharpoons{{\langle{r,k,\grave{\varphi},\beta,f,g}\rangle}}\mathcal{M}_{1}$ from source structure $\mathcal{M}_{2}={\langle{\mathcal{E}_{2},{\langle{\sigma_{2},\tau_{2}}\rangle},\mathcal{A}_{2}}\rangle}$ to target structure $\mathcal{M}_{1}={\langle{\mathcal{E}_{1},{\langle{\sigma_{1},\tau_{1}}\rangle},\mathcal{A}_{1}}\rangle}$ along (top Fig. 5) a schema morphism (Disp.6) is a list designation morphism consisting of (back Fig. 5) an entity infomorphism $\mathcal{E}_{2}\xrightleftharpoons{{\langle{r,k}\rangle}}\mathcal{E}_{1}$ , and (front Fig. 5) an attribute infomorphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ . These are bridged by the above schema morphism and (bottom Fig. 5) a universe morphism $\mathcal{U}_{2}\xLeftarrow{\;{\langle{k,\beta,g}\rangle}\;}\mathcal{U}_{1}$ with tuple bridge ${k{\;\cdot\;}\tau_{2}{\;\xRightarrow{\,\beta\,\;}\;}\tau_{1}{\;\cdot\;}{\scriptstyle\sum}_{g}}$ , whose $k_{1}^{\text{th}}$ -component is the morphism ${\tau_{2}(k(k_{1}))}\xrightarrow[h]{\beta_{k_{1}}}{{\scriptstyle\sum}_{g}(\tau_{1}(k_{1}))}$ in $\mathrmbf{List}(Y_{2})$ , with equal arity

${\footnotesize{{\underset{{(I_{2}\xrightarrow[h]{\grave{\varphi}_{r_{2}}}I_{1})\;=\;(J_{2}\xrightarrow[h]{\beta_{k_{1}}}J_{1})}}{\underbrace{\grave{\varphi}_{r_{2}}{\;\circ\;}\mathrmbfit{arity}_{X_{1}}=\beta_{k_{1}}{\;\circ\;}\mathrmbfit{arity}_{Y_{2}}}}}}}$ when ${\footnotesize{{\underset{{k_{1}{\;\models_{{\langle{r,k}\rangle}}\;}r_{2}}}{\underbrace{k(k_{1}){\;\models_{\mathcal{E}_{2}}\;}r_{2}\text{ \text@underline{iff} }k_{1}{\;\models_{\mathcal{E}_{1}}\;}r(r_{2})}}}}}$ .

Figure 5: Structure Morphism

Let $\mathrmbf{Struc}$ denote the mathematical context of structures and their morphisms.

4.3 Transition.

In this section (§ 4), we define two forms of structures and structure morphisms: a classification (strict) form and an interpretation (lax) form. Fig. 5 illustrates the classification (strict) form; whereas Fig. 7 illustrates the interpretation (lax) form. Here we define a transition from the strict form to the lax form.

Note 1

By forgetting the full key sets and the full key function, the entity infomorphism becomes a (lax) entity infomorphism $\overset{\mathrmbfit{K}_{2}}{\mathrmbfit{ext}_{\mathcal{E}_{2}}}\xLeftarrow{\;\,\kappa\;}{r}{\;\circ\;}\overset{\mathrmbfit{K}_{1}}{\mathrmbfit{ext}_{\mathcal{E}_{1}}}$ consisting of an $R_{2}$ -indexed collection of key functions
$\bigl{\{}\overset{{\mathrmbfit{K}_{2}}}{\mathrmbfit{ext}_{\mathcal{E}_{2}}}(r_{2})\xleftarrow[k]{\kappa_{r_{2}}}\overset{{\mathrmbfit{K}_{1}}}{\mathrmbfit{ext}_{\mathcal{E}_{1}}}(r(r_{2}))\mid r_{2}\in R_{2}\bigr{\}}$ .
Map $k_{1}{\,\in\,}\overset{{\mathrmbfit{K}_{1}}}{\mathrmbfit{ext}_{\mathcal{E}_{1}}}(r(r_{2}))$ with $k_{1}{\;\models_{\mathcal{E}_{1}}\;}r(r_{2})$ to $\kappa_{r_{2}}(k_{1})=k(k_{1}){\,\in\,}\overset{{\mathrmbfit{K}_{2}}}{\mathrmbfit{ext}_{\mathcal{E}_{2}}}(r_{2})$ with $k(k_{1}){\;\models_{\mathcal{E}_{2}}\;}r_{2}$ . The collection of $\mathrmbf{List}(X_{1})$ -signature morphisms $\bigl{\{}{\scriptstyle\sum}_{f}(\overset{\mathrmbfit{S}_{2}}{\sigma_{2}}(r_{2}))\xrightarrow[h]{\;\grave{\varphi}_{r_{2}}\;}\overset{\mathrmbfit{S}_{1}}{\sigma_{1}}(r(r_{2}))\mid r_{2}\in R_{2}\bigr{\}}$ defines the $\mathrmbf{List}(Y_{1})$ -tuple functions
$\bigl{\{}\mathrmbfit{tup}_{\mathcal{A}_{1}}({\scriptstyle\sum}_{f}(\sigma_{2}(r_{2})))\xleftarrow[\mathrmbfit{tup}_{\mathcal{A}_{1}}(h)]{\;\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}})\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}(\sigma_{1}(r(r_{2})))\mid r_{2}\in R_{2}\bigr{\}}$ .

Figure 6: Transition

For any source predicate $r_{2}\in R_{2}$ , there is a bridge $\kappa_{r_{2}}{\,\cdot\,}\bar{\tau}_{2,r_{2}}\xRightarrow{\;\beta_{r_{2}}\;}\bar{\tau}_{1,r(r_{2})}{\,\cdot\,}{\scriptstyle\sum}_{g}$ that is a restriction of the bridge $k{\;\cdot\;}\tau_{2}{\;\xRightarrow{\,\beta\,\;}\;}\tau_{1}{\;\cdot\;}{\scriptstyle\sum}_{g}$ to the subset $\mathrmbfit{K}_{1}(r(r_{2})){\;\subseteq\;}K_{1}$ , where $\bar{\tau}_{2,r_{2}}=\tau_{2,r_{2}}{\;\cdot\;}\mathrmbfit{inc}$ and $\bar{\tau}_{1,r(r_{2})}=\tau_{1,r(r_{2})}{\;\cdot\;}\mathrmbfit{inc}$ . For each key $k_{1}{\in}\mathrmbfit{K}_{1}(r(r_{2}))$ , the $k_{1}^{\text{th}}$ -component of the bridge $\beta_{r_{2}}$ is the $\mathrmbf{List}(Y_{2})$ -morphism
$\underset{\tau_{2}(k(k_{1}))}{\bar{\tau}_{2,r_{2}}(\kappa_{r_{2}}(k_{1}))}\xrightarrow[h]{\beta_{k_{1}}}\underset{{\scriptstyle\sum}_{g}(\tau_{1}(k_{1}))}{{\scriptstyle\sum}_{g}(\bar{\tau}_{1,r(r_{2})}(k_{1}))}$ . ²⁷²⁷27Note that we have used the equal arity condition for a structure morphism (Def 2): $\grave{\varphi}_{r_{2}}{\;\circ\;}\mathrmbfit{arity}_{X_{1}}=\beta_{k_{1}}{\;\circ\;}\mathrmbfit{arity}_{Y_{2}}$ when ${\footnotesize{k(k_{1}){\;\models_{\mathcal{E}_{2}}\;}r_{2}\text{ \text@underline{iff} }k_{1}{\;\models_{\mathcal{E}_{1}}\;}r(r_{2})}}$ .

Proposition 1 (Key)

Any structure morphism $\mathcal{M}_{2}\xrightleftharpoons{{\langle{r,k,\grave{\varphi},\beta,f,g}\rangle}}\mathcal{M}_{1}$ (Def 2) satisfies the following condition: for any source predicate $r_{2}\in R_{2}$ ,
$\kappa_{r_{2}}{\;\cdot\;}\tau_{2,r_{2}}=\tau_{1,r(r_{2})}{\;\cdot\;}{\mathrmbfit{tup}_{\mathcal{A}_{1}}({\grave{\varphi}_{r_{2}}})}{\;\cdot\;}{\grave{\tau}_{{\langle{f,g}\rangle}}({\sigma_{2}}(r_{2}))}$ . ²⁸²⁸28 The tuple bridge $\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\grave{\tau}_{{\langle{f,g}\rangle}}\;}({\scriptstyle\sum}_{f})^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ is defined and used in the paper “The FOLE Table”[11].

Proof

For suppose that $k_{1}{\,\in\,}\mathrmbfit{ext}_{\mathcal{E}_{1}}(r(r_{2}))$ with $k_{2}=\kappa_{r_{2}}(k_{1})=k(k_{1}){\,\in\,}\mathrmbfit{ext}_{\mathcal{E}_{2}}(r_{2})$ . Define $(I_{1},t_{1})=\tau_{1,r(r_{2})}(k_{1})=\tau_{1}(k_{1}){\,\in\,}\mathrmbfit{tup}_{\mathcal{A}_{1}}(\sigma_{1}(r(r_{2})))$ and $(I_{2},t_{2})=\tau_{2,r_{2}}(\kappa_{r_{2}}(k_{1}))=\tau_{2}(k_{2}){\,\in\,}\mathrmbfit{tup}_{\mathcal{A}_{2}}(\sigma_{2}(r_{2}))$ . We have the $\mathrmbf{List}(Y_{2})$ morphism $(I_{2},t_{2})=\tau_{2}(k(k_{1}))\xrightarrow[h]{\beta_{k_{1}}}{\scriptstyle\sum}_{g}(\tau_{1}(k_{1}))={\scriptstyle\sum}_{g}(I_{1},t_{1})$ . Thus, $t_{2}=h{\,\cdot\,}t_{1}{\,\cdot\,}g$ . This means that $(I_{2},t_{2})=\mathrmbfit{tup}(h,f,g)(I_{1},t_{1})=\grave{\tau}_{{\langle{f,g}\rangle}}(\sigma_{2}(r_{2}))(\mathrmbfit{tup}_{\mathcal{A}_{1}}(h)(I_{1},t_{1}))=\grave{\tau}_{{\langle{f,g}\rangle}}(\sigma_{2}(r_{2}))(\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}})(I_{1},t_{1}))$ . Hence, $\tau_{2,r_{2}}(\kappa_{r_{2}}(k_{1}))=\grave{\tau}_{{\langle{f,g}\rangle}}(\sigma_{2}(r_{2}))(\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}})(\tau_{1,r(r_{2})}(k_{1})))=\mathrmbfit{tup}(\grave{\varphi}_{r_{2}},f,g)(\tau_{1,r(r_{2})}(k_{1}))$ , for all $k_{1}{\,\in\,}\mathrmbfit{ext}_{\mathcal{E}_{1}}(r(r_{2}))$ .

Corollary 1

For $r_{2}\in R_{2}$ , each bridge $\kappa_{r_{2}}{\,\cdot\,}\bar{\tau}_{2,r_{2}}\xRightarrow{\;\beta_{r_{2}}\;}\bar{\tau}_{1,r(r_{2})}{\,\cdot\,}{\scriptstyle\sum}_{g}$ reduces to the composite $\beta_{r_{2}}=\tau_{1,r(r_{2})}{\;\cdot\;}\tau_{\grave{\varphi}_{r_{2}}}{\;\circ\;}{\scriptstyle\sum}_{g}$ for the bridge $\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}}){\,\circ\,}\mathrmbfit{inc}\xRightarrow{\tau_{\grave{\varphi}_{r_{2}}}}\mathrmbfit{inc}$ associated with the function $\mathrmbfit{tup}_{\mathcal{A}_{1}}({\scriptstyle\sum}_{f}(\sigma_{2}(r_{2})))\xleftarrow[h{\,\cdot\,}{(\mbox{-})}]{\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}})}\mathrmbfit{tup}_{\mathcal{A}_{1}}(\sigma_{1}(r(r_{2})))$ . ²⁹²⁹29For tuple $(I_{1},t_{1}){\,\in\,}\mathrmbfit{tup}_{\mathcal{A}_{1}}(\sigma_{1}(r(r_{2})))$ , the $(I_{1},t_{1})^{\text{th}}$ component of $\tau_{\grave{\varphi}_{r_{2}}}$ is the $\mathrmbf{List}(Y_{1})$ -morphism $\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}})(I_{1},t_{1})=(I_{1},h{\,\cdot\,}t_{1})\xrightarrow[h]{\tau_{\grave{\varphi}_{r_{2}}}(I_{1},t_{1})}(I_{1},t_{1})$ .

Proof

Straightforward.

4.4 Lax Structures.

To show equivalence between sound logics and databases, we need to use lax structures. ³⁰³⁰30A structure becomes lax when we forget the global set of keys $K$ and use only a lax entity classification $\mathcal{E}={\langle{R,\mathrmbfit{K}}\rangle}$ . We can retrieve a “crisp” entity classification by defining the disjoint union of key subsets $\coprod_{r\in R}\mathrmbfit{K}(r)$ . But, using the extent form of a structure (laxness), we have lost a certain coordination of tuple functions $\{\mathrmbfit{ext}_{\mathcal{E}}(r)\xrightarrow{\tau_{r}}\mathrmbfit{tup}_{\mathcal{A}}(\sigma(r))\mid r\in R\bigr{\}}$ here, which may or may not be important. Again, assume that we are given a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a set of predicate symbols $R$ and a signature (header) map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ .

Definition 3

A (lax) $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ consists of a lax entity classification $\mathcal{E}={\langle{R,\mathrmbfit{K}}\rangle}$ , an attribute classification (typed domain) $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ , the schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ , and one of the two equivalent descriptions:

$\bullet$

either (MID Fig. 4) a function $R\xrightarrow{T_{\mathcal{M}}}\mathrmbf{Tbl}(\mathcal{A})$ consisting of an $R$ -indexed collection of $\mathcal{A}$ -tables $T_{\mathcal{M}}(r)={\langle{\sigma(r),\mathrmbfit{K}(r),\tau_{r}}\rangle}$ ;
$\bullet$

or (RHS Fig. 4) a tuple bridge $\mathrmbfit{K}\xRightarrow{\;\tau\;}\sigma{\;\circ\;}\mathrmbfit{tup}_{\mathcal{A}}$ consisting of an indexed collection of tuple functions $\{\mathrmbfit{K}(r)\xrightarrow{\tau_{r}}\mathrmbfit{tup}_{\mathcal{A}}(\sigma(r))\mid r\in R\}$ .

Hence, we can think of a lax structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ as extending the FOLE schema $R\xrightarrow{\,\sigma}\mathrmbf{List}(X)$ to the tabular interpretation function $R\xrightarrow{\;T_{\mathcal{M}}\;}\mathrmbf{Tbl}(\mathcal{A})$ .

Proposition 2

A (lax) $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ defines, is the same as, the constraint-free aspect of a database $\mathcal{R}={\langle{R,\sigma,\mathcal{A},\mathrmbfit{K},\tau}\rangle}$ consisting of a set of predicate types $R$ , a key function $R\xrightarrow{\;\mathrmbfit{K}\;}\mathrmbf{Set}$ , a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a signature function $R\xrightarrow{\;\sigma\;}\mathrmbf{List}(X)$ , and a (constraint-free) tuple bridge $\mathrmbfit{K}\xRightarrow{\;\tau\;}{S}\,{\,\circ\,}\mathrmbfit{tup}_{\mathcal{A}}$ consisting of an $R$ -indexed collection of tuple maps $\bigl{\{}\mathrmbfit{K}(r)\xrightarrow{\;\tau_{r}\;}\mathrmbfit{tup}_{\mathcal{A}}(\sigma(r))\mid r\in R\bigr{\}}$ .

Proof

See the previous discussion.

4.5 Lax Structure Morphisms.

In order to make sound logic morphisms equivalent to database morphisms, we need to eliminate the global key function $K_{2}\xleftarrow{\;k\,}K_{1}$ . To do this we define a lax version of Def. 2. Note 1 eliminated the need for the global key function in the entity infomorphism¿ Prop. 1 and Cor. 1 eliminated the need for the universe morphism with its global key function. However, we do need to include the condition of Prop. 1.

Definition 4

For any two (lax) structures $\mathcal{M}_{2}={\langle{\mathcal{E}_{2},\sigma_{2},\tau_{2},\mathcal{A}_{2}}\rangle}$ and $\mathcal{M}_{1}={\langle{\mathcal{E}_{1},\sigma_{1},\tau_{1},\mathcal{A}_{1}}\rangle}$ , a (lax) structure morphism (Tbl. 13 in § 0.A.1) (Fig. 7)

$\mathcal{M}_{2}={\langle{\mathcal{E}_{2},\sigma_{2},\tau_{2},\mathcal{A}_{2}}\rangle}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{E}_{1},\sigma_{1},\tau_{1},\mathcal{A}_{1}}\rangle}=\mathcal{M}_{1}$

consists of (RHS Fig. 7) a schemed domain morphism

$\mathcal{D}_{2}={\langle{R_{2},\sigma_{2},\mathcal{A}_{2}}\rangle}\xrightarrow{\;{\langle{\mathrmit{r},\grave{\varphi},f,g}\rangle}\;}{\langle{R_{1},\sigma_{1},\mathcal{A}_{1}}\rangle}=\mathcal{D}_{1}$

consisting of a typed domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ and a schema morphism $\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{\;{\langle{\mathrmit{r},\grave{\varphi},f}\rangle}\;}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}$ (Disp.6 in § 4.2) with common type function $X_{2}\xrightarrow{\;\mathrmit{f}\;\,}X_{1}$ , and (LHS Fig. 7) a lax entity infomorphism

$\mathcal{E}_{2}={\langle{R_{2},\mathrmbfit{K}_{2}}\rangle}\xleftharpoondown{{\langle{r,\kappa}\rangle}}{\langle{R_{1},\mathrmbfit{K}_{1}}\rangle}=\mathcal{E}_{1}$

with a predicate function $R_{2}\xrightarrow{\;r\,}R_{1}$ and a key bridge $\mathrmbfit{K}_{2}\xLeftarrow{\;\,\kappa\;}r{\,\circ\,}\mathrmbfit{K}_{1}$ consisting of the key functions $\bigl{\{}{\mathrmbfit{K}_{2}}(r_{2})\xleftarrow{\kappa_{r_{2}}}{\mathrmbfit{K}_{1}}(r(r_{2}))\mid r_{2}\in R_{2}\bigr{\}}$ , which satisfy the condition

{{\Big{\{}\kappa_{r_{2}}{\;\cdot\;}\tau_{2,r_{2}}=\tau_{1,r(r_{2})}{\;\cdot\;}{\mathrmbfit{tup}_{\mathcal{A}_{1}}({\grave{\varphi}_{r_{2}}})}{\;\cdot\;}{\grave{\tau}_{{\langle{f,g}\rangle}}({\sigma_{2}}(r_{2}))}\mid r_{2}\in R_{2}\Bigr{\}}.}}

(7)

See the (Key) Prop. 1.

Corollary 2

A (lax) structure morphism $\mathcal{M}_{2}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}\mathcal{M}_{1}$ defines a tabular interpretation bridge function $\mathrmit{R}_{2}\xrightarrow{\;\xi\;}\mathrmbf{mor}(\mathrmbf{Tbl})$ , which maps a predicate symbol $r_{2}\in{\mathrmit{R}_{2}}$ with image $r(r_{2})\in{\mathrmit{R}_{1}}$ to the table morphism

{\scriptstyle{\overset{\textstyle{\mathrmbfit{T}_{2}(r_{2})}}{\overbrace{\langle{\sigma_{2}(r_{2}),\mathcal{A}_{2},\mathrmbfit{K}_{2}(r_{2}),\tau_{2,r_{2}}}\rangle}}\;\xleftarrow[\langle{\grave{\varphi}_{r_{2}},f,g,\kappa_{r_{2}}}\rangle]{\xi_{r_{2}}}\;\overset{\textstyle{\mathrmbfit{T}_{1}(r(r_{2}))}}{\overbrace{\langle{\sigma_{1}(r(r_{2})),\mathcal{A}_{1},\mathrmbfit{K}_{1}(r(r_{2})),\tau_{1,r(r_{2})}}\rangle}}.}}

(8)

visualized by the diagram

where

$\bullet$

$T_{2}(r_{2})={\langle{\sigma_{2}(r_{2}),\mathcal{A}_{2},\mathrmbfit{K}_{2}(r_{2}),\tau_{2,r_{2}}}\rangle}$ is a table defined by the tabular interpretation function $R_{2}\xrightarrow{\;T_{2}\;}\mathrmbf{Tbl}(\mathcal{A}_{2})$ of structure $\mathcal{M}_{2}$ , and
$\bullet$

$T_{1}(r(r_{2}))={\langle{\sigma_{1}(r(r_{2})),\mathcal{A}_{1},\mathrmbfit{K}_{1}(r(r_{2})),\tau_{1,r(r_{2})}}\rangle}$ is the table defined by the tabular interpretation function $R_{1}\xrightarrow{\;T_{1}\;}\mathrmbf{Tbl}(\mathcal{A}_{1})$ of structure $\mathcal{M}_{1}$ .

Proof

See Disp. 7 above.

Let $\mathring{\mathrmbf{Struc}}$ denote the mathematical context of (lax) structures and their morphisms. Since any structure is a lax structure and any structure morphism is a lax structure morphism, there is an passage $\mathrmbf{Struc}\xrightarrow{\;\mathrmbfit{lax}\;}\mathring{\mathrmbf{Struc}}$ .

Figure 7: Lax Structure Morphism

5 FOLE Specifications.

A FOLE specification $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{S}}\rangle}$ consists of a context $\mathrmbf{R}$ of predicates linked by constraints and a diagram $\mathrmbfit{S}:\mathrmbf{R}\rightarrow\mathrmbf{Set}$ of lists. A specification morphism is a diagram morphism ${\langle{\mathrmbfit{R},\zeta}\rangle}:{\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2}}\rangle}\Rightarrow{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1}}\rangle}$ consisting of a shape-changing passage $\mathrmbf{R}_{2}\xrightarrow{\>\mathrmbfit{R}\>}\mathrmbf{R}_{1}$ and a bridge $\zeta:\mathrmbfit{S}_{2}\Rightarrow\mathrmbfit{R}\circ\mathrmbfit{S}_{1}$ . Composition is component-wise. The mathematical context of FOLE specifications is denoted by $\mathrmbf{SPEC}=\mathrmbf{List}^{\scriptscriptstyle{\Downarrow}}=\bigl{(}{(\mbox{-})}{\,\Downarrow\,}\mathrmbf{List}\bigr{)}$ . The subcontext of FOLE specifications (with fixed sort sets and fixed sort functions) is denoted by $\mathrmbf{Spec}\subseteq\mathrmbf{SPEC}$ .

5.1 Specifications.

Assume that we are given a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a set of predicate symbols $R$ and a signature (header) map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ .

Definition 5

A (formal) $\mathcal{S}$ -specification is a subgraph $\mathrmbf{R}{\;\sqsubseteq\;}\mathrmbf{Cons}(\mathcal{S})$ , whose nodes are $\mathcal{S}$ -formulas and whose edges are $\mathcal{S}$ -constraints. ³²³²32We can place axiomatic restrictions on specifications in various manners. A FOLE specification requires entailment to be a preorder, satisfying reflexivity and transitivity. It could also require satisfaction of sufficient axioms (Tbl. 3 of the paper [10]) to described the various logical operations (connectives, quantifiers, etc.) used to build formulas in first-order logic.

Let $\mathrmbf{Spec}(\mathcal{S})={\wp}\mathrmbf{Cons}(\mathcal{S})$ denote the set of all $\mathcal{S}$ -specifications. ³³³³33For any graph $\mathcal{G}$ , ${\wp}\mathcal{G}={\langle{{\wp}\mathcal{G},\sqsubseteq}\rangle}$ denotes the power preorder of all subgraphs of $\mathcal{G}$ .

Definition 6

An (abstract) $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ ³⁴³⁴34An abstract specification is also known as a database schema (Def. 13 in § 7.1). consists of: a context $\mathrmbf{R}$ , whose objects $r\in R$ are predicate symbols and whose arrows $r^{\prime}\xrightarrow{\,p\,}r$ are called abstract $\mathcal{S}$ -constraints, and a passage $\mathrmbf{R}\xrightarrow{\;\mathrmbfit{S}\;}\mathrmbf{List}(X)$ , which extends the signature map ${R}\xrightarrow{\;\sigma\;}\mathrmbf{List}(X)$ by mapping an abstract constraint $r^{\prime}\xrightarrow{\,p\,}r$ to an $X$ -signature morphism $\mathrmbfit{S}(r^{\prime})=\sigma(r^{\prime})={\langle{I^{\prime},s^{\prime}}\rangle}\xrightarrow[h]{\mathrmbfit{S}(p)=\sigma(p)}{\langle{I,s}\rangle}=\sigma(r)=\mathrmbfit{S}(r)$ .

An abstract $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ has a companion formal $\mathcal{S}$ -specification $\widehat{\mathcal{T}}={\langle{\widehat{\mathrmbf{R}},\widehat{\mathrmbfit{S}},X}\rangle}$ , whose graph $\widehat{\mathrmbf{R}}\sqsubseteq\mathrmbf{Cons}(\mathcal{S})$ is the set of all formal constraints $\big{\{}r^{\prime}\xrightarrow[h]{\,\sigma(p)\,}r\mid r^{\prime}\xrightarrow{\,p\,}r\in\mathrmbf{R}\big{\}}$ . ³⁵³⁵35These are formal constraints, since any predicate symbol is a formula. Since $\widehat{\mathrmbf{R}}$ is closed under composition and contains all identities, $\widehat{\mathcal{T}}$ is an abstract $\mathcal{S}$ -specification with signature passage $\widehat{\mathrmbf{R}}\xrightarrow{\widehat{\mathrmbfit{S}}}\mathrmbf{List}(X)$ .

…

5.2 Specification Morphisms.

A FOLE (abstract) specification morphism in $\mathrmbf{Spec}$ , with constant sort function $f:X_{2}\rightarrow X_{1}$ , is a diagram morphism ${\langle{\mathrmbfit{R},\zeta}\rangle}:{\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2}}\rangle}\rightarrow{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1}}\rangle}$ in $\mathrmbf{List}$ consisting of a relation passage $\mathrmbfit{R}:\mathrmbf{R}_{2}\rightarrow\mathrmbf{R}_{1}$ and a list interpretation bridge ${\mathrmbfit{S}_{2}{\,\xRightarrow{\,\zeta\;\,}\,}\mathrmbfit{R}{\,\circ\,}\mathrmbfit{S}_{1}}$ that factors (Fig. 8)

\zeta=(\grave{\varphi}\circ\mathrmbfit{inc}_{X_{1}})\bullet(\mathrmbfit{S}_{2}\circ\grave{\iota}_{f})

(9)

through the fiber adjunction $\mathrmbf{List}(X_{2})\xleftarrow{\acute{\mathrmbfit{list}}_{f}\;\dashv\;\grave{\mathrmbfit{list}}_{f}}\mathrmbf{List}(X_{1})$ ³⁶³⁶36Fibered by signature over the adjunction $\mathrmbf{List}(X_{2})\xleftarrow[\langle{{\scriptscriptstyle\sum}_{f}{\;\dashv\;}f^{\ast}}\rangle]{{\langle{\acute{\mathrmbfit{list}}_{f}{\!\dashv\,}\grave{\mathrmbfit{list}}_{f}}\rangle}}\mathrmbf{List}(X_{1})$ (Kent [11]) representing list flow along a sort function $f:X_{2}\rightarrow X_{1}$ . in terms of

$\bullet$

some bridge $\grave{\varphi}:\mathrmbfit{S}_{2}\circ{\scriptstyle\sum}_{f}\Rightarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{S}_{1}$ and
$\bullet$

the inclusion bridge $\grave{\iota}_{f}:\mathrmbfit{inc}_{X_{2}}\Rightarrow{\scriptstyle\sum}_{f}\circ\mathrmbfit{inc}_{X_{1}}$ .

We normally just use the bridge restriction $\grave{\varphi}$ for the specification morphism. The original definition can be computed with the factorization in Disp. 9.

Definition 7

An (abstract) specification morphism (Tbl. 13 in § 0.A.1) ³⁷³⁷37Visualized on the right side Fig. 8. ³⁸³⁸38This is the same as a database schema morphism of § 7.2.
$\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightarrow{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$ ,
along a schema morphism (Disp.6 in § 4.2) consists of a relation passage $\mathrmbf{R}_{2}\xrightarrow{\;\mathrmbfit{R}\;}\mathrmbf{R}_{1}$ extending the predicate function $R_{2}\xrightarrow{\;r\;}R_{1}$ of the schema morphism to constraints, the sort function $X_{2}\xrightarrow{\;f\;}X_{1}$ of the schema morphism, and a bridge $\mathrmbfit{S}_{2}{\;\circ\;}{\scriptstyle\sum}_{f}\xRightarrow{\;\grave{\varphi}\;\,}\mathrmbfit{R}{\;\circ\;}\mathrmbfit{S}_{1}$ extending the schema bridge to naturality. ³⁹³⁹39Naturality means that for any source constraint $r^{\prime}_{2}\xrightarrow{\,p_{2}\,}r_{2}$ with target constraint $\mathrmbfit{R}(r^{\prime}_{2})=r(r^{\prime}_{2})\xrightarrow[\mathrmbfit{R}(p_{2})]{\,p_{1}\,}r(r_{2})=\mathrmbfit{R}(r_{2})$ , if their signature morphisms are ${\langle{I^{\prime}_{2},s^{\prime}_{2}}\rangle}\xrightarrow{\,h_{2}\,}{\langle{I_{2},s_{2}}\rangle}$ and ${\langle{I^{\prime}_{1},s^{\prime}_{1}}\rangle}\xrightarrow{\,h_{1}\,}{\langle{I_{1},s_{1}}\rangle}$ , we have the naturality diagram ${\scriptstyle\sum}_{f}(h_{2}){\,\circ\,}\grave{\varphi}_{r_{2}}=\grave{\varphi}_{r^{\prime}_{2}}{\,\circ\,}h_{1}$ . ⁴⁰⁴⁰40An example of a non-trivial bridge is projection: assume that the arity functions $I^{\prime}_{2}{\,\xhookrightarrow{\grave{\varphi}_{r^{\prime}_{2}}}\,}I^{\prime}_{1}$ and $I_{2}{\,\xhookrightarrow{\grave{\varphi}_{r_{2}}}\,}I_{1}$ are inclusion, thus defining signature projection, and assume that $I^{\prime}_{2}\xrightarrow{\,h_{2}\,}I_{2}$ is a restriction of $I^{\prime}_{1}\xrightarrow{\,h_{1}\,}I_{1}$ .

As noted before, $\mathrmbf{Spec}\subseteq\mathrmbf{SPEC}$ denotes the mathematical context of abstract FOLE specifications (with fixed sort sets). This context is the same as the context of database schemas and their morphisms.

Figure 8: Specification Morphism

There is an (abstract) $\mathcal{S}$ -specification morphism (LHS Fig. 9 in § 5.3)
$\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}\xrightarrow{\;\mathrmbfit{R}\;}{\langle{\widehat{\mathrmbf{R}},\widehat{\mathrmbfit{S}},X}\rangle}=\widehat{\mathcal{T}}$
with a object-identical passage $\mathrmbf{R}\xrightarrow{\;\mathrmbfit{R}\;}\widehat{\mathrmbf{R}}$ that preserves signature
$\mathrmbf{R}\!\xrightarrow{\;\mathrmbfit{R}\;}\widehat{\mathrmbf{R}}\xrightarrow{\widehat{\mathrmbfit{S}}}\mathrmbf{List}(X)=\mathrmbf{R}\xrightarrow{\mathrmbfit{S}}\mathrmbf{List}(X)$ .

5.3 Specification Satisfaction.

Assume that we are given a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ with a set of predicate symbols $R$ and a signature (header) map $R\xrightarrow{\sigma}\mathrmbf{List}(X)$ .

Definition 8

(formal satisfaction) An $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies a (formal) $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ , symbolized $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ , when it satisfies every constraint in the specification: $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ iff $\mathcal{M}^{\mathcal{S}}\sqsupseteq\mathrmbf{R}$ . Hence, $\mathcal{M}^{\mathcal{S}}$ is the largest and most specialized (formal) $\mathcal{S}$ -specification satisfied by $\mathcal{M}$ . ⁴¹⁴¹41So, $\mathcal{M}^{\mathcal{S}}$ is not just a mathematical context, but also an $\mathcal{S}$ -specification.

Definition 9

(abstract satisfaction) An $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies an abstract $\mathcal{S}$ -constraint $r^{\prime}{\;\xrightarrow{p}\;}r$ in $\mathrmbf{R}$ , symbolized by $\mathcal{M}{\;\models_{\mathcal{S}}\;}(r^{\prime}{\;\xrightarrow{p}\;}r)$ , when it satisfies the associated formal constraint $r^{\prime}\xrightarrow{\,\sigma(p)\,}r$ in $\widehat{\mathrmbf{R}}$ . An $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies (is a model of) an abstract $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ , symbolized $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ , when it satisfies every abstract constraint in the specification. Equivalently, an $\mathcal{S}$ -structure $\mathcal{M}\in\mathrmbf{Struc}(\mathcal{S})$ satisfies an abstract $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ when it satisfies the companion formal specification $\widehat{\mathcal{T}}={\langle{\widehat{\mathrmbf{R}},\widehat{\mathrmbfit{S}},X}\rangle}$ : $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ iff $\mathcal{M}^{\mathcal{S}}\sqsupseteq\widehat{\mathrmbf{R}}$ .

Definition 10

When $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ holds, the abstract table passage ${\mathrmbf{R}}^{\mathrm{op}}\!\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Rel}(\mathcal{A})$ is defined to be the composition (RHS Fig. 9) of the object-identical passage $\mathrmbf{R}\!\xrightarrow{\;\mathrmbfit{R}\;}\widehat{\mathrmbf{R}}$ with the “inclusion” $\widehat{\mathrmbf{R}}\sqsubseteq\mathcal{M}^{\mathcal{S}}$ and the relation interpretation passage ${\mathcal{M}^{\mathcal{S}}}^{\mathrm{op}}\!\xrightarrow{\;\mathrmbfit{R}_{\mathcal{M}}\;}\mathrmbf{Rel}(\mathcal{A})$ of Lem. 2 in § 3.3. ⁴²⁴²42The passage ${\mathcal{M}^{\mathcal{S}}}^{\mathrm{op}}\!\xrightarrow{\;\mathrmbfit{R}_{\mathcal{M}}\;}\mathrmbf{Rel}(\mathcal{A})$ was defined in Lemma. 2 of § 3.3 on satisfaction.

Note that the the abstract table passage ${\mathrmbf{R}}^{\mathrm{op}}\!\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Rel}(\mathcal{A})$ extends the table-valued function $R\xrightarrow{T_{\mathcal{M}}}\mathrmbf{Tbl}(\mathcal{A})\xhookrightarrow{im_{\mathcal{A}}}\mathrmbf{Rel}(\mathcal{A})$ of the structure $\mathcal{M}$ to constraints.

Proposition 3 (Key)

Satisfaction is equivalent to tabular interpretation.

Proof

On the one hand, if $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ , then the tabular interpretation passage ${\mathrmbf{R}}^{\mathrm{op}}\!\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Rel}(\mathcal{A})\xhookrightarrow{\mathrmbfit{inc}_{\mathcal{A}}}\mathrmbf{Tbl}(\mathcal{A})$ maps a constraint $r^{\prime}\xrightarrow{\,p\,}r$ in $\mathrmbf{R}$ to the $\mathcal{A}$ -relation morphism
$\mathrmbfit{T}(r^{\prime})={\langle{\mathrmbfit{S}(r^{\prime}),{\wp}t^{\prime}_{r^{\prime}}(\mathrmbfit{K}(r^{\prime}))}\rangle}\xleftarrow[\langle{h_{p},r_{p}}\rangle]{\mathrmbfit{T}(p)}{\langle{\mathrmbfit{S}(r),{\wp}t_{r}(\mathrmbfit{K}(r))}\rangle}=\mathrmbfit{T}(r)$
as pictured in Fig. 3 of §3.3. ⁴³⁴³43 We use relations here rather than tables, since (Lem. 2 of § 3.3): relational interpretation is closed under composition; but tabular interpretation is closed under composition only up to key equivalence.

On the other hand, if there is a tabular interpretation passage ${\mathrmbf{R}}^{\mathrm{op}}\!\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Tbl}(\mathcal{A})$ , then the adjoint flow of $\mathcal{A}$ -tables ⁴⁴⁴⁴44See the discussion about type domain indexing in § 3.4.1 of the paper [11]. demonstrates that the $\mathcal{S}$ -structure $\mathcal{M}$ satisfies each abstract $\mathcal{S}$ -constraint $r^{\prime}{\;\xrightarrow{p}\;}r$ in $\mathrmbf{R}$ (see Disp.4 in § 3.3).

in general

with satisfaction

Figure 9: Specification Passages

Specification
(formal) $\mathcal{S}$ -specification – subgraph :	$\mathrmbf{R}{\;\sqsubseteq\;}\mathrmbf{Cons}(\mathcal{S})$
signature passage :	$\mathrmbf{Cons}(\mathcal{S})\rightarrow\mathrmbf{List}(X)$
(abstract) $\mathcal{S}$ -specification – passage :	$\mathrmbf{R}\xrightarrow{\;\mathrmbfit{S}\;}\mathrmbf{List}(X)$
Sound Logic
(formal) $\mathcal{S}$ -specification – subgraph :	$\mathrmbf{R}{\;\sqsubseteq\;}\mathcal{M}^{\mathcal{S}}$
table passage :	${\mathcal{M}^{\mathcal{S}}}^{\mathrm{op}}\!\!\xrightarrow{\;\mathrmbfit{R}_{\mathcal{M}}\;}\mathrmbf{Rel}(\mathcal{A})\xhookrightarrow{\mathrmbfit{inc}_{\mathcal{A}}}\mathrmbf{Tbl}(\mathcal{A})$
(abstract) $\mathcal{S}$ -specification – table passage :	${\mathrmbf{R}}^{\mathrm{op}}\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Rel}(\mathcal{A})\xhookrightarrow{\mathrmbfit{inc}_{\mathcal{A}}}\mathrmbf{Tbl}(\mathcal{A})$

Table 7: Comparisons

6 FOLE Sound Logics.

6.1 Sound Logics.

Definition 11

A (lax) sound logic $\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathcal{T}}\rangle}$ with a schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ , consists of a (lax) $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ and an (abstract) $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ , where the structure $\mathcal{M}$ satisfies the specification $\mathcal{T}$ : $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ .

Proposition 4

Any (lax) FOLE sound logic $\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathcal{T}}\rangle}$ defines a FOLE relational database with constant type domain $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}$ . ⁴⁵⁴⁵45A (lax) FOLE sound logic is described in terms of its components in Tbl. 8. In § 7.1, a FOLE relational database is defined in Def. 13 and is described in terms of its components in Tbl. 10.

Proof

By the definition of satisfaction (Def. 9 and Def. 10 in § 5.3), the tabular interpretation $R\xrightarrow{T}\mathrmbf{Tbl}(\mathcal{A})$ (Def. 3 of § 4.4) extends to a table passage $\mathrmbf{R}^{\text{op}}\!\xrightarrow{\mathrmbfit{T}}\mathrmbf{Rel}(\mathcal{A})\subseteq\mathrmbf{Tbl}(\mathcal{A})$ , which forms a relational database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}$ .

$\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathcal{T}}\rangle}$ sound logic
schema	$\mathcal{S}={\langle{R,\sigma,X}\rangle}$
signature function	$R\xrightarrow{\;\sigma\;}\mathrmbf{List}(X)$
(lax) $\mathcal{S}$ -structure	$\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$
(lax) entity classification	$\mathcal{E}={\langle{R,\mathrmbfit{K}}\rangle}$
attribute classification	$\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$
tuple bridge	$\mathrmbfit{K}\xRightarrow{\;\tau\;}\sigma{\,\circ\;}\mathrmbfit{tup}_{\mathcal{A}}$
table function	$R\xrightarrow{\;T_{\mathcal{M}}\;}\mathrmbf{Tbl}(\mathcal{A})$
$\mathcal{S}$ -specification	$\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$
signature passage	$\mathrmbf{R}\xrightarrow{\;\mathrmbfit{S}\;}\mathrmbf{List}(X)$
satisfaction	$\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$
table passage	$\mathrmbf{R}^{\mathrm{op}}\!\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Rel}(\mathcal{A})\xhookrightarrow{\mathrmbfit{inc}_{\mathcal{A}}}\mathrmbf{Tbl}(\mathcal{A})$

Table 8: Sound Logic

6.2 Sound Logic Morphisms.

Definition 12

For any two sound logics $\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}$ and $\mathcal{L}_{1}={\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}$ , a (lax) sound logic morphism (Tbl. 13 in § 0.A.1)
$\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}=\mathcal{L}_{1}$
consists of a (lax) structure morphism
$\mathcal{M}_{2}={\langle{\mathcal{E}_{2},{\langle{\sigma_{2},\tau_{2}}\rangle},\mathcal{A}_{2}}\rangle}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{E}_{1},{\langle{\sigma_{1},\tau_{1}}\rangle},\mathcal{A}_{1}}\rangle}=\mathcal{M}_{1}$ and
an (abstract) specification morphism
$\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightarrow{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$
along a common schema morphism
$\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{{\langle{r,\grave{\varphi},f}\rangle}}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}$ .

Let $\mathring{\mathrmbf{Snd}}$ denote the context of (lax) sound logics and their morphisms.

Note 2

At this point we know that a (lax) sound logic morphism
$\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}=\mathcal{L}_{1}$
has tabular interpretation passages $\mathrmbf{R}_{2}\xrightarrow{\;\mathrmbfit{T}_{2}\;}\mathrmbf{Rel}(\mathcal{A}_{2})\subseteq\mathrmbf{Tbl}(\mathcal{A}_{2})$ and $\mathrmbf{R}_{1}\xrightarrow{\;\mathrmbfit{T}_{1}\;}\mathrmbf{Rel}(\mathcal{A}_{1})\subseteq\mathrmbf{Tbl}(\mathcal{A}_{1})$ at the source and target sound logics and a predicate passage $\mathrmbf{R}_{2}\xrightarrow{\;\mathrmbfit{R}\;}\mathrmbf{R}_{1}$ . We complete the picture in Prop. 5 by proving that sound logic morphisms preserve satisfaction in some way.

Proposition 5

There is a (tabular interpretation) bridge

$\xi=(\grave{\psi}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\mathrmbfit{T}_{2}\circ\grave{\chi}_{{\langle{f,g}\rangle}}):\mathrmbfit{T}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\!{\,\circ\,}\mathrmbfit{T}_{1}$

that extends the collection of tabular interpretation bridge functions

$\bigl{\{}{\footnotesize{\mathrmbfit{T}_{2}(r_{2})\;\xleftarrow[\langle{\grave{\varphi}_{r_{2}},f,g,\kappa_{r_{2}}}\rangle]{\xi_{r_{2}}}\;\mathrmbfit{T}_{1}(r(r_{2}))}}\mid r_{2}\in R_{2}\bigr{\}}$

(see Cor. 2 of § 4.5) to constraints: for any source constraint $r^{\prime}_{2}\xrightarrow{p_{2}}r_{2}$ in $\mathrmbf{R}_{2}$ with $\mathrmbfit{R}$ -image target constraint $r^{\prime}_{1}\xrightarrow{p_{1}}r_{1}$ in $\mathrmbf{R}_{1}$ , we have the following naturality diagram, which represents “preservation or linkage of satisfaction”. ⁴⁶⁴⁶46The sound logic morphism $\mathcal{L}_{2}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}\mathcal{L}_{1}$ maps the table morphism $\mathrmbfit{T}_{1}(r^{\prime}_{1})\xleftarrow{\mathrmbfit{T}_{1}(p_{1})}\mathrmbfit{T}_{1}(r_{1})$ representing the satisfaction $\mathcal{M}_{1}{\;\models_{\mathcal{S}_{1}}\;}(r^{\prime}_{1}{\;\xrightarrow{p_{1}}\;}r_{1})$ to the table morphism $\mathrmbfit{T}_{2}(r^{\prime}_{2})\xleftarrow{\mathrmbfit{T}_{2}(p_{2})}\mathrmbfit{T}_{2}(r_{2})$ representing the satisfaction $\mathcal{M}_{2}{\;\models_{\mathcal{S}_{2}}\;}(r^{\prime}_{2}{\;\xrightarrow{p_{2}}\;}r_{2})$ .

Proof

The above diagram is expanded into more detail in Fig. 10.

Figure 10: Naturality Combined

To understand this, we discuss each part (facet) separately. In short: the front/back is due to Cor. 2 in § 4.5 for (lax) structure morphisms; the left/right hold by satisfaction of source/target sound logics; the bottom-right is due to the (abstract) specification morphism; the bottom-left is due to naturality of $\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\grave{\tau}_{{\langle{f,g}\rangle}}\;}{\scriptstyle\sum}_{f}^{\mathrm{op}}{\;\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ ; and the top holds for relations. We now discuss each facet in more detail.

front/back:

For each source predicate $r_{2}\in\mathrmbf{R}_{2}$ , the (lax) structure morphism $\mathcal{M}_{2}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}\mathcal{M}_{1}$ defines (Cor. 2 of § 4.5) the table morphism
$\underset{\mathrmbfit{T}_{2}(r_{2})}{\langle{\overset{\mathrmbfit{S}}{\sigma}(r_{2}),\mathcal{A}_{2},\overset{\mathrmbfit{K}}{\mathrmbfit{ext}}_{\mathcal{E}_{2}}(r_{2}),\tau_{r_{2}}}\rangle}\xleftarrow[\xi_{r_{2}}]{\;{\langle{\grave{\varphi}_{r_{2}},f,g,\kappa_{r_{2}}}\rangle}\;}\underset{\mathrmbfit{T}_{1}(\mathrmbfit{R}(r_{2}))}{\langle{\overset{\mathrmbfit{S}}{\sigma}(r_{1}),\mathcal{A}_{1},\overset{\mathrmbfit{K}}{\mathrmbfit{ext}}_{\mathcal{E}_{1}}(r_{1}),\tau_{r_{1}}}\rangle}$
(same for $r^{\prime}_{2}\in\mathrmbf{R}_{2}$ ).
left/right (sat):

Satisfaction for source/target sound logics (§ 5.3) define table morphisms
${\langle{\sigma(r^{\prime}_{i}),\mathrmbfit{ext}_{\mathcal{E}}(r^{\prime}_{i}),\tau_{r^{\prime}_{i}}}\rangle}\xleftarrow[\mathrmbfit{T}_{i}(p_{i})]{\;{\langle{h_{p_{i}},k_{p_{i}}}\rangle}\;}{\langle{\sigma(r_{i}),\mathrmbfit{ext}_{\mathcal{E}}(r_{i}),\tau_{r_{i}}}\rangle}$ ,
which are equivalent to naturality of the bridges $\mathrmbfit{K}_{i}\xRightarrow[\mathrmbfit{T}_{i}{\,\circ\,}\tau_{\mathcal{A}_{i}}]{\,\tau_{i}\;}\mathrmbfit{S}_{i}^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{i}}$ .

bottom right:

The structure and specification morphisms have the same underlying schema morphism $\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{{\langle{r,\grave{\varphi},f}\rangle}}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}$ . Apply the tuple function $\mathrmbfit{tup}_{\mathcal{A}_{1}}$ to the naturality of the bridge $\mathrmbfit{S}_{2}{\;\circ\;}{\scriptstyle\sum}_{f}\xRightarrow{\;\grave{\varphi}\;\,}\mathrmbfit{R}{\;\circ\;}\mathrmbfit{S}_{1}$ for any abstract $\mathcal{S}$ -constraint $r^{\prime}_{2}\xrightarrow{\,p_{2}\,}r_{2}$ in $\mathrmbf{R}_{2}$ : for any constraint $r^{\prime}_{2}\xrightarrow{p_{2}}r_{2}$ in $\mathrmbf{R}_{2}$ , the following diagram commutes.

bottom left:

The tuple bridge $\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\grave{\tau}_{{\langle{f,g}\rangle}}\;}{\scriptstyle\sum}_{f}^{\mathrm{op}}{\;\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ of the type domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ (see footnote 28 in § 4.2) satisfies naturality: for any constraint $r^{\prime}_{2}\xrightarrow{p_{2}}r_{2}$ in $\mathrmbf{R}_{2}$ , the following diagram commutes.

top:

By the other naturality conditions just proven, for any constraint $r^{\prime}_{2}\xrightarrow{p_{2}}r_{2}$ in $\mathrmbf{R}_{2}$ with $\mathrmbfit{R}$ -image $r^{\prime}_{1}\xrightarrow{p_{1}}r_{1}$ in $\mathrmbf{R}_{1}$ , we know that $k_{p_{1}}{\,\cdot\,}\kappa_{r^{\prime}_{2}}{\,\cdot\,}\tau_{r^{\prime}_{2}}=\kappa_{r_{2}}{\,\cdot\,}k_{p_{2}}{\,\cdot\,}\tau_{r^{\prime}_{2}}$ . If the tuple map $\mathrmbfit{ext}_{\mathcal{E}_{2}}(r^{\prime}_{2})\xrightarrow{\tau_{r^{\prime}_{2}}}\mathrmbfit{tup}_{\mathcal{A}_{2}}(\sigma_{2}(r^{\prime}_{2}))$ were injective, the bridge $\overset{\mathrmbfit{K}_{2}}{\mathrmbfit{ext}_{\mathcal{E}_{2}}}\xLeftarrow{\;\kappa\;}\overset{\mathrmbfit{R}}{r}{\;\circ\;}\overset{\mathrmbfit{K}_{1}}{\mathrmbfit{ext}_{\mathcal{E}_{1}}}$ would satisfy “extent naturality”:

Here, we use the image part of the table-relation reflection ${\langle{\mathrmbfit{im}{\;\dashv\;}\mathrmbfit{inc}}\rangle}:\mathrmbf{Tbl}{\;\rightleftarrows\;}\mathrmbf{Rel}$ . ⁴⁷⁴⁷47The reflection ${\langle{\mathrmbfit{im}{\;\dashv\;}\mathrmbfit{inc}}\rangle}:\mathrmbf{Tbl}{\;\rightleftarrows\;}\mathrmbf{Rel}$ (“The FOLE Table”[11]) of the context of relations into the context of tables embodies the notion of “informational equivalence”. Then, we use diagonal fill-in Fig. 10. Hence, extent naturality holds for the relational interpretation into $\mathrmbf{Rel}$ .

Proposition 6

A (lax) sound logic morphism
$\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{R}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{R}_{1}}\rangle}=\mathcal{L}_{1}$
defines a database morphism

\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},\mathcal{A}_{2},\mathrmbfit{K}_{2},\tau_{2}}\rangle}\xrightarrow[\langle{\mathrmbfit{R},\xi}\rangle]{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},\mathcal{A}_{1},\mathrmbfit{K}_{1},\tau_{1}}\rangle}=\mathcal{R}_{1}

whose tabular interpretation bridge ${\mathrmbfit{T}_{2}{\,\xLeftarrow{\;\,\xi\,}\,}\mathrmbfit{R}{\,\circ\,}\mathrmbfit{T}_{1}}$ factors
$\xi=(\grave{\psi}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\mathrmbfit{T}_{2}\circ\grave{\chi}_{{\langle{f,g}\rangle}})$
through the fiber adjunction $\mathrmbf{Tbl}(\mathcal{A}_{2})\xleftarrow{\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\;\dashv\;\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}}\mathrmbf{Tbl}(\mathcal{A}_{1})$ .

Proof

By Prop. 4 the sound logics $\mathcal{L}_{2}$ and $\mathcal{L}_{1}$ define two databases $\mathcal{R}_{2}$ and $\mathcal{R}_{1}$ . By Prop. 5 the (lax) sound logic morphism $\mathcal{L}_{2}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}\mathcal{L}_{1}$ defines a database morphism ${\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\xi}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1}}\rangle}$ , whose tabular interpretation bridge ${\mathrmbfit{T}_{2}{\,\xLeftarrow{\;\,\xi\,}\,}\mathrmbfit{R}{\,\circ\,}\mathrmbfit{T}_{1}}$ factors as above.

Theorem 6.1

There is a passage $\mathring{\mathrmbf{Snd}}^{\mathrm{op}}\!\xrightarrow{\;\mathring{\mathrmbfit{db}}\;}\mathrmbf{Db}$ .

Proof

A sound logic $\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathcal{T}}\rangle}$ is mapped to its associated database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{K},\mathrmbfit{S},\tau,\mathcal{A}}\rangle}$ by Prop. 4. A sound logic morphism $\mathcal{L}_{2}\xrightleftharpoons{{\langle{\mathrmbfit{R},k,\grave{\varphi},f,g}\rangle}}\mathcal{L}_{1}$ is mapped to its associated database morphism $\mathcal{R}_{2}\xrightarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}\mathcal{R}_{1}$ by Prop. 6.

sound logic morphism $\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}=\mathcal{L}_{1}$ $\bullet$ schema morphism $\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{\;{\langle{r,\grave{\varphi},f}\rangle}\;}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}$ $\bullet$ (lax) struc morph $\mathcal{M}_{2}={\langle{\overset{\textstyle{\mathcal{E}_{2}}}{\langle{R_{2},\mathrmbfit{K}_{2}}\rangle},\sigma_{2},\tau_{2},\mathcal{A}_{2}}\rangle}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\overset{\textstyle{\mathcal{E}_{1}}}{\langle{R_{1},\mathrmbfit{K}_{1}}\rangle},\sigma_{1},\tau_{1},\mathcal{A}_{1}}\rangle}=\mathcal{M}_{1}$ $\circ$ type domain morphism $\mathcal{A}_{2}={\langle{X_{2},Y_{2},\models_{\mathcal{A}_{2}}}\rangle}\xrightleftharpoons{{\langle{f,g}\rangle}}{\langle{X_{1},Y_{1},\models_{\mathcal{A}_{1}}}\rangle}=\mathcal{A}_{1}$ $\circ$ (lax) entity infomorphism $\mathcal{K}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{K}_{2}}\rangle}\xrightarrow{\;{\langle{\mathrmbfit{R},\kappa}\rangle}\;}{\langle{\mathrmbf{R}_{1},\mathrmbfit{K}_{1}}\rangle}=\mathcal{K}_{1}$ which satisfy the constraint
$\kappa\bullet\tau_{2}=(\mathrmbfit{R}^{\mathrm{op}}\!{\circ\;}\tau_{1}){\;\bullet\;}(\grave{\varphi}^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}){\;\bullet\;}(\mathrmbfit{S}_{2}^{\mathrm{op}}{\;\circ\;}\grave{\tau}_{{\langle{f,g}\rangle}})$ $\bullet$ specification morphism $\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightarrow{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$

Table 9: Sound Logic Morphism

7 FOLE Databases.

A FOLE relational database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T}}\rangle}$ consists of a context $\mathrmbf{R}$ of predicates linked by constraints and an interpretation diagram $\mathrmbfit{T}:\mathrmbf{R}^{\mathrm{op}}\rightarrow\mathrmbf{Tbl}$ of tables. A relational database morphism ${\langle{\mathrmbfit{R},\xi}\rangle}:{\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2}}\rangle}\leftarrow{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1}}\rangle}$ (Tbl. 13 in § 0.A.1) is a diagram morphism (LHS Fig. 12 in § 7.2) consisting of a shape-changing passage $\mathrmbf{R}_{2}\xrightarrow{\>\mathrmbfit{R}\>}\mathrmbf{R}_{1}$ and a bridge $\xi:\mathrmbfit{T}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}$ . Composition is component-wise. The mathematical context of FOLE relational databases is denoted by $\mathrmbf{DB}=\mathrmbf{Tbl}^{\scriptscriptstyle{\Downarrow}}=\bigl{(}{(\mbox{-})}^{\mathrm{op}}{\Downarrow\,}\mathrmbf{Tbl}\bigr{)}$ . ⁴⁹⁴⁹49See § 4.2.1 in the paper “The FOLE Database” [12].

7.1 Databases.

Definition 13

A FOLE database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}$ , with constant type domain $\mathcal{A}$ , is a database with an interpretation diagram $\mathrmbfit{T}:\mathrmbf{R}^{\mathrm{op}}\rightarrow\mathrmbf{Tbl}(\mathcal{A})\hookrightarrow\mathrmbf{Tbl}$ that factors through the context of $\mathcal{A}$ -tables.

Figure 11: Database: Type Domain

Definition 14

Using $\mathcal{A}$ -table projection passages ⁵⁰⁵⁰50See § 3.4.1 of the paper “The FOLE Table” [11]. (Fig. 11), a database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{K},\mathrmbfit{S},\tau,\mathcal{A}}\rangle}$ , with constant type domain $\mathcal{A}$ , consists of

$\bullet$

a context $\mathrmbf{R}$ of predicates,
$\bullet$

a relational database schema $\mathcal{S}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ with signature diagram $\mathrmbfit{S}=\mathrmbfit{T}^{\mathrm{op}}{\circ\;}\mathrmbfit{sign}_{\mathcal{A}}:\mathrmbf{R}\rightarrow\mathrmbf{List}(X)$ ,
$\bullet$

a key diagram $\mathrmbfit{K}=\mathrmbfit{T}{\;\circ\;}\mathrmbfit{key}_{\mathcal{A}}:\mathrmbf{R}^{\mathrm{op}}\rightarrow\mathrmbf{Set}$ , and
$\bullet$

a tuple bridge $\tau=\mathrmbfit{T}{\,\circ\,}\tau_{\mathcal{A}}:\mathrmbfit{K}\Rightarrow\mathrmbfit{S}^{\mathrm{op}}\!{\,\circ\,}\mathrmbfit{tup}_{\mathcal{A}}$ .

$\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}$ relational database
predicate context	$\mathrmbf{R}$
type domain (attribute classification)	$\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$
table passage	$\mathrmbf{R}^{\text{op}}\xrightarrow{\;\mathrmbfit{T}\;}\mathrmbf{Tbl}(\mathcal{A})$
$\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{S},\mathrmbfit{K},\tau,\mathcal{A}}\rangle}$
database schema (specification)	$\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$
signature passage	$\mathrmbf{R}\xrightarrow[\mathrmbfit{T}^{\mathrm{op}}{\circ\;}\mathrmbfit{sign}_{\mathcal{A}}]{\mathrmbfit{S}}\mathrmbf{List}(X)$
key passage	$\mathrmbf{R}^{\mathrm{op}}\xrightarrow[\mathrmbfit{T}{\;\circ\;}\mathrmbfit{key}_{\mathcal{A}}]{\mathrmbfit{K}}\mathrmbf{Set}$
tuple bridge	$\mathrmbfit{K}\xRightarrow[\mathrmbfit{T}{\,\circ\,}\tau_{\mathcal{A}}]{\tau}\mathrmbfit{S}^{\mathrm{op}}\!{\,\circ\,}\mathrmbfit{tup}_{\mathcal{A}}$

Table 10: Relational Database

Proposition 7

The constraint-free aspect of a FOLE database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{K},\mathrmbfit{S},\tau,\mathcal{A}}\rangle}$ , with constant type domain $\mathcal{A}$ , is the same as a (lax) FOLE structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ in $\mathring{\mathrmbf{Struc}}$ .

Proof

We define the various components of the (lax) structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ listed in Def. 3 of § 4.4 and pictured in Fig. 4 of § 4.1.

$\mathcal{A}$ :

The attribute classification (typed domain) $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ is given.
$\sigma$ :

The schema (type hypergraph) $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ consists of the set $R$ of relation symbols (predicates) and the signature map $\sigma:R\rightarrow\mathrmbf{List}(X):r\mapsto\sigma(r)=\mathrmbfit{S}(r)$ . This is the constraint-free aspect of the database schema $\mathcal{S}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ with signature diagram $\mathrmbfit{S}:\mathrmbf{R}\rightarrow\mathrmbf{List}(X)$ .
$\mathcal{E}$ :

The (lax) entity classification $\mathcal{E}={\langle{R,\mathrmbfit{K}}\rangle}$ consists of the set $R$ of relation symbols (predicates) and the key function $R\xrightarrow{\mathrmbfit{K}}\mathrmbf{Set}$ . This is the constraint-free aspect of the key diagram $\mathrmbf{R}^{\mathrm{op}}\xrightarrow{\mathrmbfit{K}}\mathrmbf{Set}$ .
$\tau$ :

The tuple bridge $\tau:\mathrmbfit{K}\Rightarrow\sigma{\;\circ\;}\mathrmbfit{tup}_{\mathcal{A}}$ is the constraint-free aspect of the tuple bridge $\tau:\mathrmbfit{K}\xRightarrow{\,\tau}\mathrmbfit{S}^{\mathrm{op}}\!{\,\circ\,}\mathrmbfit{tup}_{\mathcal{A}}$ .

Proposition 8

Any FOLE database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}={\langle{\mathrmbf{R},\mathrmbfit{K},\mathrmbfit{S},\tau,\mathcal{A}}\rangle}$ in $\mathrmbf{Db}(\mathcal{A})$ defines a (lax) FOLE sound logic $\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathcal{T}}\rangle}$ in $\mathring{\mathrmbf{Snd}}$ .

Proof

The schema $\mathcal{S}={\langle{R,\sigma,X}\rangle}$ is the structure schema (mentioned above), the constraint-free aspect of the database schema ${\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ . The $\mathcal{S}$ -structure $\mathcal{M}={\langle{\mathcal{E},\sigma,\tau,\mathcal{A}}\rangle}$ is defined in Prop. 7 above. The (abstract) $\mathcal{S}$ -specification $\mathcal{T}={\langle{\mathrmbf{R},\mathrmbfit{S},X}\rangle}$ is the same as the database schema, as discussed in § 5.1. By Prop 3 in § 5.3, the tabular interpretation passage $\mathrmbf{R}^{\mathrm{op}}\!\xrightarrow{\mathrmbfit{T}\;}\mathrmbf{Tbl}(\mathcal{A})$ demonstrates satisfaction $\mathcal{M}{\;\models_{\mathcal{S}}\;}\mathcal{T}$ .

7.2 Database Morphisms.

A FOLE database morphism, with constant type domain morphism ${\langle{f,g}\rangle}:\mathcal{A}_{2}\rightleftarrows\mathcal{A}_{1}$ , is a FOLE database morphism ${\langle{\mathrmbfit{R},\xi}\rangle}:{\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2}}\rangle}\leftarrow{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1}}\rangle}$ , whose tabular interpretation bridge ${\mathrmbfit{T}_{2}{\,\xLeftarrow{\;\,\xi\,}\,}\mathrmbfit{R}{\,\circ\,}\mathrmbfit{T}_{1}}$ factors (Fig. 12)

\xi=(\grave{\psi}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\mathrmbfit{T}_{2}\circ\grave{\chi}_{{\langle{f,g}\rangle}})

(10)

through the fiber adjunction $\mathrmbf{Tbl}(\mathcal{A}_{2})\xleftarrow{\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\;\dashv\;\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}}\mathrmbf{Tbl}(\mathcal{A}_{1})$ ⁵¹⁵¹51 There is a table fiber adjunction $\mathrmbf{Tbl}(\mathcal{A}_{2})\xleftarrow{{\langle{\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}{\!\dashv\,}\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}}\rangle}}\mathrmbf{Tbl}(\mathcal{A}_{1})$ representing tabular flow along a type domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ . See § 3.4.2 of Kent [11]. The fiber passage $\mathrmbf{Tbl}(\mathcal{A}_{2})\xleftarrow{\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}}\mathrmbf{Tbl}(\mathcal{A}_{1})$ is define in terms of the tuple bridge ${f^{\ast}}^{\mathrm{op}}{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\acute{\tau}_{{\langle{f,g}\rangle}}\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ and the substitution function $\mathrmbf{List}(X_{2})\xleftarrow{f^{\ast}}\mathrmbf{List}(X_{1})$ . The adjoint fiber passage $\mathrmbf{Tbl}(\mathcal{A}_{2})\xrightarrow{\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}}\mathrmbf{Tbl}(\mathcal{A}_{1})$ is define in terms the adjoints, the tuple bridge $\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\grave{\tau}_{{\langle{f,g}\rangle}}\;}{\scriptstyle\sum}_{f}^{\mathrm{op}}{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ and the existential quantifier function $\mathrmbf{List}(X_{2})\xrightarrow{{\scriptscriptstyle\sum}_{f}}\mathrmbf{List}(X_{1})$ . in terms of

$\bullet$

some bridge $\grave{\psi}:\mathrmbfit{T}_{2}\circ\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}$ and
$\bullet$

the inclusion bridge $\grave{\chi}_{{\langle{f,g}\rangle}}:\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}}$ ⁵²⁵²52Equivalently, in terms of their levo bridge adjoints in Tbl. 12 of § 0.A.1. .

We normally just use the bridge restriction $\grave{\psi}$ for the database morphism. The original definition can be computed with the factorization in Disp. 10.

Figure 12: Database Morphism

levo

dextro

\mathcal{A}_{2}\xrightleftharpoons{\;{\langle{f,g}\rangle}\;}\mathcal{A}_{1}

\begin{array}[]{|@{\hspace{5pt}}l@{\hspace{15pt}}l@{\hspace{5pt}}|}\lx@intercol\text{levo}\hfil\lx@intercol&\lx@intercol\text{dextro}\hfil\lx@intercol\\ \hline\cr\hskip 5.0pt\lx@intercol\acute{\chi}_{{\langle{f,g}\rangle}}:\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\mathrmbfit{inc}_{\mathcal{A}_{1}}\hfil\hskip 15.0&\grave{\chi}_{{\langle{f,g}\rangle}}:\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}}\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\chi}_{{\langle{f,g}\rangle}}=(\eta_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\grave{\chi}_{{\langle{f,g}\rangle}})\hfil\hskip 15.0&\grave{\chi}_{{\langle{f,g}\rangle}}=(\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\acute{\chi}_{{\langle{f,g}\rangle}})\bullet(\varepsilon_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}})\rule[-7.0pt]{0.0pt}{10.0pt}\hfil\hskip 5.0\\ \hline\cr\end{array}

Figure 13: Inclusion Bridge: Tables

The inclusion bridges for the table fiber adjunction ⁵³⁵³53Notation from § 3.4.2.

are defined by

\overset{\textstyle{\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}(\mathcal{T}_{1})}}{\overbrace{\langle{f^{\ast}(I_{1},s_{1}),{\scriptscriptstyle\sum}_{\acute{\tau}_{{\langle{f,g}\rangle}}(I_{1},s_{1})}(K_{1},t_{1})}\rangle}}\xleftarrow[{\langle{\varepsilon_{f}(I_{1},s_{1}),f,g,1_{K_{1}}}\rangle}]{\acute{\chi}_{{\langle{f,g}\rangle}}(\mathcal{T}_{1})}\overset{\textstyle{\mathcal{T}_{1}}}{\overbrace{\langle{I_{1},s_{1},K_{1},t_{1}}\rangle}}

\overset{\textstyle{\mathcal{T}_{2}}}{\overbrace{\langle{I_{2},s_{2},K_{2},t_{2}}\rangle}}\xrightarrow[{\langle{1_{I_{2}},f,g,\hat{k}}\rangle}]{\grave{\chi}_{{\langle{f,g}\rangle}}(\mathcal{T}_{2})}\overset{\textstyle{\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}(\mathcal{T}_{2})}}{\overbrace{\langle{{\scriptstyle\sum}_{f}(I_{2},s_{2}),(\grave{\tau}_{{\langle{f,g}\rangle}}(I_{2},s_{2}))^{\ast}(K_{2},t_{2})}\rangle}}

Definition 15

For any two databases $\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2},\mathcal{A}_{2}}\rangle}$ and $\mathcal{R}_{1}={\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1},\mathcal{A}_{1}}\rangle}$ , a database morphism, with constant type domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ , (Fig. 12)

$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2},\mathcal{A}_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\grave{\psi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1},\mathcal{A}_{1}}\rangle}=\mathcal{R}_{1}$

(Tbl. 13 in § 0.A.1) consists of a shape-changing relation passage $\mathrmbfit{R}:\mathrmbf{R}_{2}\rightarrow\mathrmbf{R}_{1}$ and a bridge $\grave{\psi}:\mathrmbfit{T}_{2}\circ\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}$ .

The subcontext of FOLE relational databases (with constant type domains and constant type domain morphisms) is denoted by $\mathrmbf{Db}\subseteq\mathrmbf{DB}$ . ⁵⁴⁵⁴54See § 4.2.2 in the paper “The FOLE Database” [12].

Definition 16

Using projections (Fig. 14), a FOLE database morphism, with constant type domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ ,

\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},\mathcal{A}_{2},\mathrmbfit{K}_{2},\tau_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},\mathcal{A}_{1},\mathrmbfit{K}_{1},\tau_{1}}\rangle}=\mathcal{R}_{1}

(Tbl. 13 in § 0.A.1) consists of a relation passage $\mathrmbf{R}_{2}\xrightarrow{\,\mathrmbfit{R}\;}\mathrmbf{R}_{1}$ as above, and

$\bullet$

a schema bridge $\grave{\varphi}=\grave{\psi}^{\mathrm{op}}{\circ\;}\mathrmbfit{sign}:\mathrmbfit{S}_{2}{\;\circ\;}{\scriptstyle\sum}_{f}\Rightarrow\mathrmbfit{R}{\;\circ\;}\mathrmbfit{S}_{1}$ ⁵⁵⁵⁵55This defines a database schema morphism
$\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$ ,
which is the same as the (abstract) specification morphism in Def. 7 of § 5.2. , and
$\bullet$

a key bridge $\kappa=\grave{\psi}{\;\circ\;}\mathrmbfit{key}:\mathrmbfit{K}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}{\circ\;}\mathrmbfit{K}_{1}$ consisting of an $R_{2}$ -indexed collection $\{\mathrmbfit{K}_{2}(r_{2})\xleftarrow{\kappa_{r_{2}}}\mathrmbfit{K}_{1}(r(r_{2}))\mid r_{2}\in R_{2}\}$ of key functions. ⁵⁶⁵⁶56This defines a lax entity infomorphism $\mathrmbfit{K}_{2}\xLeftarrow{\;\,\kappa\;}{r}{\;\circ\;}\mathrmbfit{K}_{1}$ consisting of an $R_{2}$ -indexed collection of key functions $\bigl{\{}\mathrmbfit{K}_{2}(r_{2})\xleftarrow{\kappa_{r_{2}}}\mathrmbfit{K}_{1}(r(r_{2}))\mid r_{2}\in R_{2}\bigr{\}}$

These components satisfy the condition

\kappa{\;\bullet\;}\tau_{2}=(\mathrmbfit{R}^{\mathrm{op}}\!{\circ\;}\tau_{1}){\;\bullet\;}(\grave{\varphi}^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}){\;\bullet\;}(\mathrmbfit{S}_{2}^{\mathrm{op}}{\;\circ\;}\grave{\tau}_{{\langle{f,g}\rangle}}),

(11)

as pictured in the following bridge diagram.

$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{K}_{2},\mathrmbfit{S}_{2},\tau_{2},\mathcal{A}_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{K}_{1},\mathrmbfit{S}_{1},\tau_{1},\mathcal{A}_{1}}\rangle}=\mathcal{R}_{1}$ $\bullet$ schema bridge $\grave{\varphi}:\mathrmbfit{S}_{2}{\;\circ\;}{\scriptstyle\sum}_{f}\Rightarrow\mathrmbfit{R}{\;\circ\;}\mathrmbfit{S}_{1}$ $\bullet$ a key bridge $\kappa:\mathrmbfit{K}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}{\circ\;}\mathrmbfit{K}_{1}$ $\bullet$ constraint $\kappa\bullet\tau_{2}=(\mathrmbfit{R}^{\mathrm{op}}\!{\circ\;}\tau_{1}){\;\bullet\;}(\grave{\varphi}^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}){\;\bullet\;}(\mathrmbfit{S}_{2}^{\mathrm{op}}{\;\circ\;}\grave{\tau}_{{\langle{f,g}\rangle}})$

Table 11: Database Morphism

Figure 14: Database Morphism: Type Domain

Proposition 9

The constraint-free aspect of a FOLE database morphism
$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},\mathcal{A}_{2},\mathrmbfit{K}_{2},\tau_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},\mathcal{A}_{1},\mathrmbfit{K}_{1},\tau_{1}}\rangle}=\mathcal{R}_{1}$ ,
in $\mathrmbf{Db}$ defines, is the same as, a (lax) FOLE structure morphism
$\mathcal{M}_{2}={\langle{\mathcal{E}_{2},\sigma_{2},\tau_{2},\mathcal{A}_{2}}\rangle}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{E}_{1},\sigma_{1},\tau_{1},\mathcal{A}_{1}}\rangle}=\mathcal{M}_{1}$
in $\mathring{\mathrmbf{Struc}}$ .

Proof

We define the various components of the (lax) structure morphism above, as defined in Def.4 and pictured in Fig. 7 of § 4.5.

$r$ :

The predicate function $R_{2}\xrightarrow{\;r\,}R_{1}$ is the constraint-free aspect of the relation passage $\mathrmbf{R}_{2}\xrightarrow{\mathrmbfit{R}}\mathrmbf{R}_{1}$ .
${\langle{f,g}\rangle}$ :

The type domain morphism $\mathcal{A}_{2}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}_{1}$ is given.
${\langle{r,\grave{\varphi},f}\rangle}$ :

The schema morphism $\mathcal{S}_{2}={\langle{R_{2},{\sigma_{2}},X_{2}}\rangle}\xRightarrow{{\langle{r,\grave{\varphi},f}\rangle}}{\langle{R_{1},{\sigma_{1}},X_{1}}\rangle}=\mathcal{S}_{1}$ , consisting of the $R_{2}$ -indexed collection of signature morphisms $\{{\scriptstyle\sum}_{f}({\sigma_{2}}(r_{2}))\xrightarrow[h]{\;\grave{\varphi}_{r_{2}}\;}{\sigma_{1}}(r(r_{2}))\mid r_{2}\in R_{2}\}$ , is the constraint-free aspect of the database schema morphism in Def. 16.

{\langle{r,\kappa}\rangle}

The lax entity infomorphism $\mathcal{E}_{2}={\langle{R_{2},\mathrmbfit{K}_{2}}\rangle}\xleftharpoondown{{\langle{r,\kappa}\rangle}}{\langle{R_{1},\mathrmbfit{K}_{1}}\rangle}=\mathcal{E}_{1}$ , consisting of the $R_{2}$ -indexed collection of key functions $\bigl{\{}{\mathrmbfit{K}_{2}}(r_{2})\xleftarrow{\kappa_{r_{2}}}{\mathrmbfit{K}_{1}}(r(r_{2}))\mid r_{2}\in R_{2}\bigr{\}}$ , is the constraint-free aspect of the key bridge $\kappa:\mathrmbfit{K}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}{\circ\;}\mathrmbfit{K}_{1}$ . These components satisfy the condition ⁵⁷⁵⁷57This is the constraint-free aspect of the database morphism condition
$\kappa{\;\bullet\;}\tau_{2}=(\mathrmbfit{R}^{\mathrm{op}}\!{\circ\;}\tau_{1}){\;\bullet\;}(\grave{\varphi}^{\mathrm{op}}\!{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}){\;\bullet\;}(\mathrmbfit{S}_{2}^{\mathrm{op}}{\;\circ\;}\grave{\tau}_{{\langle{f,g}\rangle}})$ .
See Def. 16 above. ⁵⁸⁵⁸58See Disp.7 in Def.4 of § 4.5.

{{\Big{\{}\kappa_{r_{2}}{\;\cdot\;}\tau_{2,r_{2}}=\tau_{1,r(r_{2})}{\;\cdot\;}\underset{\mathrmbfit{tup}(\grave{\varphi}_{r_{2}},f,g)}{\underbrace{\mathrmbfit{tup}_{\mathcal{A}_{1}}(\grave{\varphi}_{r_{2}}){\;\cdot\;}\grave{\tau}_{{\langle{f,g}\rangle}}({\sigma_{2}}(r_{2}))}}\mid r_{2}\in R_{2}\Bigr{\}}.}}

Proposition 10

Any FOLE database morphism
$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},\mathcal{A}_{2},\mathrmbfit{K}_{2},\tau_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},\mathcal{A}_{1},\mathrmbfit{K}_{1},\tau_{1}}\rangle}=\mathcal{R}_{1}$
in $\mathrmbf{Db}$ defines a (lax) FOLE sound logic morphism
$\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}=\mathcal{L}_{1}$
in $\mathring{\mathrmbf{Snd}}$ .

Proof

The source and target sound logics are defined by Prop. 8 above. The structure morphism is given by Prop. 9 above. The (abstract) specification morphism is the same as the database schema morphism
$\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$ ,
as discussed in § 5.1.

Theorem 7.1

There is a passage $\mathrmbf{Db}^{\mathrm{op}}\xrightarrow{\;\mathring{\mathrmbfit{snd}}\;}\mathring{\mathrmbf{Snd}}$ .

Proof

A database $\mathcal{R}={\langle{\mathrmbf{R},\mathrmbfit{T},\mathcal{A}}\rangle}$ in $\underline{\mathrmbf{Db}}$ is mapped to its associated sound logic $\mathcal{L}={\langle{\mathcal{S},\mathcal{M},\mathrmbf{T}}\rangle}$ by Prop. 8. A database morphism $\mathcal{R}_{2}\xleftarrow{{\langle{\mathrmbfit{R},\psi,f,g}\rangle}}\mathcal{R}_{1}$ in $\underline{\mathrmbf{Db}}$ is mapped to its associated sound logic morphism $\mathcal{L}_{2}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\alpha,f,g}\rangle}}\mathcal{L}_{1}$ by Prop. 10.

Theorem 7.2

The contexts of databases and (lax) sound logics form a reflection

$\begin{array}[]{c}{\begin{picture}(120.0,30.0)(0.0,-12.0)\put(10.0,0.0){\makebox(0.0,0.0)[]{\footnotesize{$\mathrmbf{Db}^{\mathrm{op}}$}}} \put(110.0,2.0){\makebox(0.0,0.0)[]{\footnotesize{$\mathring{\mathrmbf{Snd}}$}}} \put(60.0,22.0){\makebox(0.0,0.0)[]{\scriptsize{$\mathrmbfit{im}$}}} \put(62.0,0.0){\makebox(0.0,0.0)[]{\scriptsize{$\dashv$}}} \put(66.0,-20.0){\makebox(0.0,0.0)[]{\scriptsize{$\mathrmbfit{inc}$}}} \put(35.0,10.0){\vector(1,0){50.0}} \put(85.0,-10.0){\vector(-1,0){50.0}} \put(85.0,-6.0){\oval(8.0,8.0)[r]} \end{picture}}\end{array}$ ,

so that these two representation of FOLE are “informationally equivalent”. ⁵⁹⁵⁹59The database-logic reflection
$\mathrmbf{Db}(\mathcal{A})\;\xrightarrow{{\langle{\mathrmbfit{im}_{\mathcal{A}}{\;\dashv\;}\mathrmbfit{inc}_{\mathcal{A}}}\rangle}}\;\mathrmbf{Log}(\mathcal{A})$
generalizes the table-relation reflection $\mathrmbf{Tbl}(\mathcal{A})\;\xrightarrow{{\langle{\mathrmbfit{im}_{\mathcal{A}}{\;\dashv\;}\mathrmbfit{inc}_{\mathcal{A}}}\rangle}}\;\mathrmbf{Rel}(\mathcal{A})$ . These reflections embody the notion of informational equivalence. ⁶⁰⁶⁰60See Prop. 12 in § A.1 of the paper [11] “The FOLE Table”.

Proof

The passages in Thm. 6.1 and Thm. 7.1 form a reflection. Here, we use the image part $\mathrmbf{Tbl}{\;\xhookrightarrow{\;\mathrmbfit{im}\;}\;}\mathrmbf{Rel}$ of the table-relation reflection. ⁶¹⁶¹61The reflection ${\langle{\mathrmbfit{im}{\;\dashv\;}\mathrmbfit{inc}}\rangle}:\mathrmbf{Tbl}{\;\rightleftarrows\;}\mathrmbf{Rel}$ (“The FOLE Table”[11]) of the context of relations into the context of tables embodies the notion of “informational equivalence”. For an alternate proof, first compose with image part of the table-relation reflection ${}^{\mathrm{\ref{tbl:rel:refl}}}$ , and then restrict to fixed type domains.

Appendix 0.A Appendix

0.A.1 FOLE Components

Bridges.

Although adjointly equivalent, no levo bridges are used throughout this paper, except for the levo tuple bridge ${f^{\ast}}^{\mathrm{op}}{\circ\;}\mathrmbfit{tup}_{\mathcal{A}_{2}}\xLeftarrow{\;\acute{\tau}_{{\langle{f,g}\rangle}}\;}\mathrmbfit{tup}_{\mathcal{A}_{1}}$ discussed in footnote 51 in § 7.2.

$\begin{array}[]{|@{\hspace{5pt}}l@{\hspace{15pt}}l@{\hspace{5pt}}|}\lx@intercol\text{levo}\hfil\lx@intercol&\lx@intercol\text{dextro}\hfil\lx@intercol\\ \hline\cr\hskip 5.0pt\lx@intercol\acute{\varphi}:\mathrmbfit{S}_{2}\Rightarrow\mathrmbfit{R}\circ\mathrmbfit{S}_{1}\circ{f^{\ast}}\hfil\hskip 15.0&\grave{\varphi}:\mathrmbfit{S}_{2}\circ{{\Sigma}_{f}}\Rightarrow\mathrmbfit{R}\circ\mathrmbfit{S}_{1}\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\varphi}=(\mathrmbfit{S}_{2}\circ\eta_{f})\bullet(\grave{\varphi}\circ{f^{\ast}})\hfil\hskip 15.0&\grave{\varphi}=(\acute{\varphi}\circ{{\Sigma}_{f}})\bullet(\mathrmbfit{R}\circ\mathrmbfit{S}_{1}\circ\varepsilon_{f})\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\varphi}=(\acute{\psi}\circ\mathrmbfit{sign}_{\mathcal{A}_{2}}^{\mathrm{op}})^{\mathrm{op}}\hfil\hskip 15.0&\grave{\varphi}=(\grave{\psi}\circ\mathrmbfit{sign}_{\mathcal{A}_{1}}^{\mathrm{op}})^{\mathrm{op}}\hfil\hskip 5.0\\ \hline\cr\hskip 5.0pt\lx@intercol\acute{\psi}:\mathrmbfit{T}_{2}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}\circ\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\hfil\hskip 15.0&\grave{\psi}:\mathrmbfit{T}_{2}\circ\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\psi}=(\grave{\psi}\circ\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}})\bullet(\mathrmbfit{T}_{2}\circ\varepsilon_{{\langle{f,g}\rangle}})\hfil\hskip 15.0&\grave{\psi}=(\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1})\eta_{{\langle{f,g}\rangle}}\bullet(\acute{\psi}\circ\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}})\hfil\hskip 5.0\\ \hline\cr\hskip 5.0pt\lx@intercol\acute{\chi}_{{\langle{f,g}\rangle}}:\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\mathrmbfit{inc}_{\mathcal{A}_{1}}\hfil\hskip 15.0&\grave{\chi}_{{\langle{f,g}\rangle}}:\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}}\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\chi}_{{\langle{f,g}\rangle}}=(\eta_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\acute{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ\grave{\chi}_{{\langle{f,g}\rangle}})\hfil\hskip 15.0&\grave{\chi}_{{\langle{f,g}\rangle}}=(\grave{\mathrmbfit{tbl}}_{{\langle{f,g}\rangle}}\circ{\chi}_{{\langle{f,g}\rangle}})\bullet(\varepsilon_{{\langle{f,g}\rangle}}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}})\hfil\hskip 5.0\\ \hline\cr\hskip 5.0pt\lx@intercol\acute{\tau}_{{\langle{f,g}\rangle}}:(f^{\ast})^{\mathrm{op}}\circ\mathrmbfit{tup}_{\mathcal{A}_{2}}\Leftarrow\mathrmbfit{tup}_{\mathcal{A}_{1}}\hfil\hskip 15.0&\grave{\tau}_{{\langle{f,g}\rangle}}:\mathrmbfit{tup}_{\mathcal{A}_{2}}\Leftarrow{\scriptstyle\sum}_{f}^{\mathrm{op}}\circ\mathrmbfit{tup}_{\mathcal{A}_{1}}\hfil\hskip 5.0\\ \hskip 5.0pt\lx@intercol\acute{\tau}_{{\langle{f,g}\rangle}}=(\varepsilon_{f}^{\mathrm{op}}\circ\mathrmbfit{tup}_{\mathcal{A}_{1}})\bullet((f^{\ast})^{\mathrm{op}}\circ\grave{\tau}_{{\langle{f,g}\rangle}})\hfil\hskip 15.0&\grave{\tau}_{{\langle{f,g}\rangle}}=({\scriptstyle\sum}_{f}^{\mathrm{op}}\circ\acute{\tau}_{{\langle{f,g}\rangle}})\bullet(\eta_{f}^{\mathrm{op}}\circ\mathrmbfit{tup}_{\mathcal{A}_{2}})\hfil\hskip 5.0\\ \hline\cr\vrule\lx@intercol\hfil\xi:\mathrmbfit{T}_{2}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}}\Leftarrow\mathrmbfit{R}^{\mathrm{op}}\circ\mathrmbfit{T}_{1}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}}\hfil\lx@intercol\vrule\lx@intercol\\ \vrule\lx@intercol\hfil(\mathrmbfit{R}^{\mathrm{op}}{\!\circ}\mathrmbfit{T}_{1}\circ\acute{\chi}_{{\langle{f,g}\rangle}})\bullet(\acute{\psi}\circ\mathrmbfit{inc}_{\mathcal{A}_{2}})\;=\;\xi\;=\;(\grave{\psi}\circ\mathrmbfit{inc}_{\mathcal{A}_{1}})\bullet(\mathrmbfit{T}_{2}{\;\circ\;}\grave{\chi}_{{\langle{f,g}\rangle}})\hfil\lx@intercol\vrule\lx@intercol\\ \hline\cr\end{array}$

Table 12: FOLE Adjoint Bridges

Morphisms.

The FOLE equivalence is explained and understood principally in terms of its various morphisms (Tbl. 13).


schema morphism	$\mathcal{S}_{2}={\langle{R_{2},\sigma_{2},X_{2}}\rangle}\xRightarrow{\;{\langle{r,\grave{\varphi},f}\rangle}\;}{\langle{R_{1},\sigma_{1},X_{1}}\rangle}=\mathcal{S}_{1}$
schemed domain morphism	$\mathcal{D}_{2}={\langle{R_{2},\sigma_{2},\mathcal{A}_{2}}\rangle}\xrightarrow{\;{\langle{r,\grave{\varphi},f,g}\rangle}\;}{\langle{R_{1},\sigma_{1},\mathcal{A}_{1}}\rangle}=\mathcal{D}_{1}$
(lax) structure morphism	$\mathcal{M}_{2}={\langle{\mathcal{E}_{2},\sigma_{2},\tau_{2},\mathcal{A}_{2}}\rangle}\xrightleftharpoons{{\langle{r,\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{E}_{1},\sigma_{1},\tau_{1},\mathcal{A}_{1}}\rangle}=\mathcal{M}_{1}$
specification morphism	$\mathcal{T}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},X_{2}}\rangle}\xrightarrow{{\langle{\mathrmbfit{R},\grave{\varphi},f}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},X_{1}}\rangle}=\mathcal{T}_{1}$
sound logic morphism	$\mathcal{L}_{2}={\langle{\mathcal{S}_{2},\mathcal{M}_{2},\mathcal{T}_{2}}\rangle}\xrightleftharpoons{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathcal{S}_{1},\mathcal{M}_{1},\mathcal{T}_{1}}\rangle}=\mathcal{L}_{1}$
$\text{database morphism}_{1}$	$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\xi}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1}}\rangle}=\mathcal{R}_{1}$
$\text{database morphism}_{2}$	$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{T}_{2},\mathcal{A}_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\grave{\psi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{T}_{1},\mathcal{A}_{1}}\rangle}=\mathcal{R}_{1}$
$\text{database morphism}_{3}$	$\mathcal{R}_{2}={\langle{\mathrmbf{R}_{2},\mathrmbfit{S}_{2},\mathcal{A}_{2},\mathrmbfit{K}_{2},\tau_{2}}\rangle}\xleftarrow{{\langle{\mathrmbfit{R},\kappa,\grave{\varphi},f,g}\rangle}}{\langle{\mathrmbf{R}_{1},\mathrmbfit{S}_{1},\mathcal{A}_{1},\mathrmbfit{K}_{1},\tau_{1}}\rangle}=\mathcal{R}_{1}$
1 full, 2 fixed type domain, 3 with projections

Table 13: FOLE Morphisms

0.A.2 Classifications and Infomorphisms

The concept of a “classification” comes from the theory of Information Flow: see the book Information Flow: The Logic of Distributed Systems by Barwise and Seligman [1]. A classification is also important in the theory of Formal Concept Analysis, where it is called a “formal context”: see the book Formal Concept Analysis: Mathematical Foundations by Ganter and Wille [4].

Classification.

A classification $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ consists of: a set $Y=\mathrmbfit{inst}(\mathcal{A})$ of objects to be classified, called tokens or instances; a set $X=\mathrmbfit{typ}(\mathcal{A})$ of objects that classify the instances, called types; and a binary relation $\models_{\mathcal{A}}{\;\subseteq\;}Y{\times}X$ between instances and types. The extent of any type $x{\,\in\,}X$ is the subset of instances classified by $x$ : $\mathrmbfit{ext}_{\mathcal{A}}(x)=\{y\in Y\mid y\;\models_{\mathcal{A}}x\}$ . Dually, the intent of any instance $y{\,\in\,}Y$ is the subset of types that classify $y$ : $\mathrmbfit{int}_{\mathcal{A}}(y)=\{x\in X\mid y\;\models_{\mathcal{A}}x\}$ . Two types $x,x^{\prime}\in X$ are coextensive in $\mathcal{A}$ when $\mathrmbfit{ext}_{\mathcal{A}}(x)=\mathrmbfit{ext}_{\mathcal{A}}(x^{\prime})$ . Two instances $y,y^{\prime}\in Y$ are cointensive or indistinguishable in $\mathcal{A}$ when $\mathrmbfit{int}_{\mathcal{A}}(y)=\mathrmbfit{int}_{\mathcal{A}}(y^{\prime})$ . A classification $\mathcal{A}$ is separated or intensional when there are no two indistinguishable instances: $y\neq y^{\prime}$ implies $\mathrmbfit{int}_{\mathcal{A}}(y)\neq\mathrmbfit{int}_{\mathcal{A}}(y^{\prime})$ . A classification $\mathcal{A}$ is extensional when all coextensive types are identical: $\mathrmbfit{ext}_{\mathcal{A}}(x)=\mathrmbfit{ext}_{\mathcal{A}}(x^{\prime})$ implies $x=x^{\prime}$ ; equivalently, $x\neq x^{\prime}$ implies $\mathrmbfit{ext}_{\mathcal{A}}(x)\neq\mathrmbfit{ext}_{\mathcal{A}}(x^{\prime})$ . More strongly, a classification $\mathcal{A}$ is disjoint when distinct types have disjoint extents: $x\neq x^{\prime}$ implies $\mathrmbfit{ext}_{\mathcal{A}}(x)\cap\mathrmbfit{ext}_{\mathcal{A}}(x^{\prime})=\emptyset$ . Even more strongly, a classification $\mathcal{A}$ is partitioned when it is disjoint and all instances are classified: $\mathrmbfit{int}_{\mathcal{A}}(y)\neq\emptyset$ equivalently $y\in\mathrmbfit{ext}_{\mathcal{A}}(x)$ some $x\in X$ for all $y\in Y$ . A classification $\mathcal{A}$ is pseudo-partitioned when it is disjoint and all instances are classified except for one special instance ${\cdot}\in Y$ : $\mathrmbfit{int}_{\mathcal{A}}({\cdot})=\emptyset$ .

Infomorphism.

An infomorphism $\mathcal{A}_{2}={\langle{X_{2},Y_{2},\models_{\mathcal{A}_{2}}}\rangle}\xrightleftharpoons{{\langle{f,g}\rangle}}{\langle{X_{1},Y_{1},\models_{\mathcal{A}_{1}}}\rangle}=\mathcal{A}_{1}$ consists of a type map $X_{2}\xrightarrow{\;f\;}X_{1}$ and an instance map $Y_{2}\xleftarrow{\;g\;}Y_{1}$ , which satisfy the following:

${\begin{array}[]{c}g(y_{1}){\;\models_{\mathcal{A}_{2}}\;}x_{2}{\;\;\;\text{\text@underline{iff}}\;\;\;}y_{1}{\;\models_{\mathcal{A}_{1}}\;}x_{1}=f(x_{2})\\ g(y_{1}){\,\in\,}\underset{\mathrmbfit{Y}_{2}(x_{2})}{\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2})}{\;\;\;\text{\text@underline{iff}}\;\;\;}y_{1}{\,\in\,}\underset{\mathrmbfit{Y}_{1}(f(x_{2}))}{\mathrmbfit{ext}_{\mathcal{A}_{1}}(f(x_{2}))}\\ g^{-1}(\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2}))=\mathrmbfit{ext}_{\mathcal{A}_{1}}(f(x_{2}))\end{array}}$

Figure 15: Infomorphism

If two distinct source types $x_{2},x^{\prime}_{2}\in X_{2}$ , $x_{2}\not=x^{\prime}_{2}$ , are mapped by the type map to the same target type ⁶²⁶²62Are you producting the two types by doing this? Remember how the sum and product of classifications is defined. $f(x_{2})=f(x^{\prime}_{2})=x_{1}\in X_{1}$ , then any target instance in the extent $y_{1}\in\mathrmbfit{ext}_{\mathcal{A}_{1}}(x_{1})$ is mapped by the instance map to the extent intersection $g(y_{1})\in\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2}){\;\cap\;}\mathrmbfit{ext}_{\mathcal{A}_{2}}(x^{\prime}_{2})$ . Hence, if extent sets are disjoint in the source classification, then the type map must be injective. Note however that there is restricted map $\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2}){\;\times\;}\mathrmbfit{ext}_{\mathcal{A}_{2}}(x^{\prime}_{2})\xleftarrow{\;g\;}\mathrmbfit{ext}_{\mathcal{A}_{1}}(x_{1})$ . Let $\mathrmbf{Cls}$ denote the context of classifications and infomorphisms.

Type Domains.

In the FOLE theory of data-types [9], a classification $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ is known as a type domain. A type domain [11] is an sort-indexed collection of data types from which a table’s tuples are chosen. It consists of a set of sorts (data types) $X$ , a set of data values (instances) $Y$ , and a binary (classification) relation $\models_{\mathcal{A}}$ between data values and sorts. The extent of any sort (data type) $x\in X$ is the subset $\mathrmbfit{ext}_{\mathcal{A}}(x)=A_{x}=\{y\in Y\mid y{\;\models_{\mathcal{A}}\;}x\}$ . Hence, a type domain is equivalent to be a sort-indexed collection of subsets of data values $X\xrightarrow{\;\mathcal{A}\;}{\wp}Y:x\mapsto\mathrmbfit{ext}_{\mathcal{A}}(x)=A_{x}$ . ⁶³⁶³63Some examples of data-types useful in databases are as follows. The real numbers might use sort symbol $\Re$ with extent $\{-\infty,\cdots,0,\cdots,\infty\}$ . The alphabet might use sort symbol $\aleph$ with extent $\{a,b,c,\cdots,x,y,z\}$ . Words, as a data-type, would be lists of alphabetic symbols with sort symbol $\aleph^{\ast}$ with extent $\{a,b,c,\cdots,x,y,z\}^{\ast}$ being all strings of alphabetic symbols. The periodic table of elements might use sort symbol E with extent $\{\text{H, He, Li, He,}\cdots\text{, Hs,Mt}\}$ . Of course, chemical elements can also be regarded as entity types in a database with various properties such as name, symbol, atomic number, atomic mass, density, melting point, boiling point, etc. The list classification $\mathrmbf{List}(\mathcal{A})={\langle{\mathrmbf{List}(X),\mathrmbf{List}(Y),\models_{\mathrmbf{List}(\mathcal{A})}}\rangle}$ has $X$ -signatures as types and $Y$ -tuples as instances, with classification by common arity and universal $\mathcal{A}$ -classification: a $Y$ -tuple ${\langle{J,t}\rangle}$ is classified by an $X$ -signature ${\langle{I,s}\rangle}$ when $J=I$ and $t_{k}\models_{\mathcal{A}}s_{k}$ for all $k\in J=I$ . ⁶⁴⁶⁴64In particular, when $I=1$ is a singleton, an $X$ -signature ${\langle{1,s}\rangle}$ is the same as a sort $s({\cdot)}=x\in X$ , a $Y$ -tuple ${\langle{1,t}\rangle}$ is the same as a data value $t({\cdot})=y\in Y$ , and $\mathrmbfit{tup}(1,s,\mathcal{A})=\mathrmbfit{tup}_{\mathcal{A}}(1,s)=\mathrmbfit{ext}_{\mathrmbf{List}(\mathcal{A})}(1,s)=\mathcal{A}_{x}$ . In the FOLE theory of data-types, an infomorphism $\mathcal{A}^{\prime}\xrightleftharpoons{{\langle{f,g}\rangle}}\mathcal{A}$ is known as a type domain morphism, and consists of a sort function $X^{\prime}\xrightarrow{\;f\;}X$ and a data value function $Y^{\prime}\xleftarrow{\;g\;}Y$ that satisfy the condition $g(y){\;\models_{\mathcal{A}^{\prime}}\;}x^{\prime}$ iff $y{\;\models_{\mathcal{A}}\;}f(x^{\prime})$ for any source sort $x^{\prime}{\,\in\,}X^{\prime}$ and target data value $y{\,\in\,}Y$ .

Lax Classification.

From an extensional point-of-view, a classification $\mathcal{A}={\langle{X,Y,\models_{\mathcal{A}}}\rangle}$ is a set-valued function $X\xrightarrow[\mathrmbfit{Y}]{\mathrmbfit{ext}_{\mathcal{A}}}{\wp}Y$ ; that is, an indexed collection of (sub)sets $\bigl{\{}\mathrmbfit{ext}_{\mathcal{A}}(x)=\mathrmbfit{Y}(x)\mid x\in X\bigr{\}}$ . In a lax classification we omit the global set of data values $Y$ . ⁶⁵⁶⁵65We can always define a global set of instances; for example, $Y=\bigcup_{x\in X}\mathrmbfit{Y}(x)$ , $Y=\coprod_{x\in X}\mathrmbfit{Y}(x)$ , etc. Hence, a (lax) classification is just the pair $\mathcal{A}={\langle{X,\mathrmbfit{Y}}\rangle}$ consisting of a set $X=\mathrmbfit{typ}(\mathcal{A})$ of objects called types that classify the instances, and a collection of indexed subsets $\bigl{\{}\mathrmbfit{Y}(x)\mid x\in X\bigr{\}}$ , where $\mathrmbfit{Y}(x)=\mathrmbfit{ext}_{\mathcal{A}}(x)$ is the set of instances (tokens) classified by the type $x\in X$ . More briefly, a (lax) classification is a $\mathrmbf{Set}$ -valued diagram $X\xrightarrow{\,\mathrmbfit{Y}\;}\mathrmbf{Set}$ .

Lax Infomorphism.

Tbl. 14 motivates the definition of a lax infomorphism. In a lax infomorphism $\mathcal{A}_{2}={\langle{X_{2},\mathrmbfit{Y}_{2}}\rangle}\xleftharpoondown{{\langle{f,\gamma}\rangle}}{\langle{X_{1},\mathrmbfit{Y}_{1}}\rangle}=\mathcal{A}_{1}$ the instance function $Y_{2}\xleftarrow{\;g\,}Y_{1}$ is replaced by the collection of instance functions $\bigl{\{}\mathrmbfit{Y}_{2}(x_{2})\xleftarrow{\gamma_{r_{2}}}\mathrmbfit{Y}_{1}(f(x_{2}))\mid x_{2}\in X_{2}\bigr{\}}$ . Hence, an infomorphism is a $\mathrmbf{Set}$ -valued instance bridge $\mathrmbfit{Y}_{2}\xLeftarrow{\;\,\gamma\;}f{\,\circ\,}\mathrmbfit{Y}_{1}$ . Let $\mathring{\mathrmbf{Cls}}$ denote the context of lax classifications and lax infomorphisms. There is a passage $\mathrmbf{Cls}\xrightarrow{\mathrmbfit{lax}}\dot{\mathrmbf{Cls}}$ .

$\begin{array}[]{r@{\hspace{5pt}}c@{\hspace{5pt}}l}\lx@intercol\hfil\underline{\text{infomorphism}}\hfil\lx@intercol\rule[-10.0pt]{0.0pt}{10.0pt}\\ \mathcal{A}_{2}={\langle{X_{2},Y_{2},\models_{\mathcal{A}_{2}}}\rangle}\hskip 5.0&\xrightleftharpoons{{\langle{f,g}\rangle}}\hfil\hskip 5.0&{\langle{X_{1},Y_{1},\models_{\mathcal{A}_{1}}}\rangle}=\mathcal{A}_{1}\\ g(y_{1}){\;\models_{\mathcal{A}_{2}}\;}x_{2}\hskip 5.0&\;\Longleftrightarrow\hfil\hskip 5.0&y_{1}{\;\models_{\mathcal{A}_{1}}\;}f(x_{2})\\ g(y_{1}){\;\in\;}\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2})\hskip 5.0&\;\Longleftrightarrow\hfil\hskip 5.0&y_{1}{\;\in\;}\mathrmbfit{ext}_{\mathcal{A}_{1}}(f(x_{2}))\\ g^{-1}(\mathrmbfit{ext}_{\mathcal{A}_{2}}(x_{2}))\hskip 5.0&\;=\hfil\hskip 5.0&\mathrmbfit{ext}_{\mathcal{A}_{1}}(f(x_{2}))\\ ...............................................\hskip 5.0&\text{\text@underline{implies}}\hfil\hskip 5.0&...............................................\\ g^{-1}(\overset{\mathrmbfit{Y}_{2}}{\mathrmbfit{ext}_{\mathcal{A}_{2}}}(x_{2}))\hskip 5.0&\;\supseteq\hfil\hskip 5.0&\overset{\mathrmbfit{Y}_{1}}{\mathrmbfit{ext}_{\mathcal{A}_{1}}}(f(x_{2}))\\ g(x_{1}){\;\in\;}\overset{\mathrmbfit{Y}_{2}}{\mathrmbfit{ext}_{\mathcal{A}_{2}}}(x_{2})\hskip 5.0&\;\Longleftarrow\hfil\hskip 5.0&x_{1}{\;\in\;}\overset{\mathrmbfit{Y}_{1}}{\mathrmbfit{ext}_{\mathcal{A}_{1}}}(f(x_{2}))\\ g(y_{1}){\;\models_{\mathcal{A}_{2}}\;}x_{2}\hskip 5.0&\;\Longleftarrow\hfil\hskip 5.0&y_{1}{\;\models_{\mathcal{A}_{1}}\;}f(x_{2})\\ \mathcal{A}_{2}={\langle{X_{2},\mathrmbfit{Y}_{2}}\rangle}\hskip 5.0&\xleftharpoondown{{\langle{f,\gamma}\rangle}}\hfil\hskip 5.0&{\langle{X_{1},\mathrmbfit{Y}_{1}}\rangle}=\mathcal{A}_{1}\\ \lx@intercol\hfil\text{\text@underline{lax infomorphism}}\hfil\lx@intercol\rule[6.0pt]{0.0pt}{10.0pt}\\ \hskip 5.0&\hfil\hskip 5.0&\end{array}$

Table 14: Lax Infomorphisms

strict

lax

Figure 16: Lax Infomorphism

References

[1] Barwise, J., and Seligman, J.: Information Flow: The Logic of Distributed Systems. Cambridge University Press, Cambridge (1997).
[2] Chen, P.: “The Entity-Relationship Model - Toward a Unified View of Data”. ACM Trans. on Database Sys., 1 (1): pp. 9-36. doi:10.1145/320434.320440.
[3] Codd, E.F.: The relational model for database management : version 2. Addison Wesley, Boston (1990).
[4] Ganter, B., and Wille, R.: Formal Concept Analysis: Mathematical Foundations. Springer, New York (1999).
[5] Goguen, J.: A categorical manifesto. Mathematical Structures in Computer Science 1, 49–67 (1991).
[6] Gruber, T. “Ontology”. In: Ling Liu and M. Tamer Özsu (eds.) The Encyclopedia of Database Systems, Springer-Verlag (2009). Available online: tomgruber.org/writing/ontology-definition-2007.htm.
[7] Kent, R.E.: “Database Semantics”. (2011). Available online:
https://arxiv.org/abs/1209.3054.
[8] Kent, R.E.: “The First-order Logical Environment”. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., and Nagarjuna G. (eds.) Conceptual Structures in Research and Education, LNCS vol. 7735, pp. 210–230. Springer, Heidelberg (2013). Available online: https://arxiv.org/abs/1305.5240.
[9] Kent, R.E.: “The ERA of FOLE: Foundation” (2015). Submitted for publication. Available online: https://arxiv.org/abs/1512.07430.
[10] Kent, R.E.: “The ERA of FOLE: Superstructure” (2016). Available online:
https://arxiv.org/abs/1602.04268.
[11] Kent, R.E.: “The FOLE Table”. Submitted for publication. Available online:
https://arxiv.org/abs/1810.12100.
[12] Kent, R.E.: “The FOLE Database”. Available online:
https://arxiv.org/abs/2302.05997.
[13] Kent, R.E.: “Relational Operations in FOLE”. Submitted for publication. Available online: https://arxiv.org/abs/2103.11027.
[14] Kent, R.E.: “Semantic Integration in the IFF”. Presented at the Semantic Integration Workshop of the 2nd International Semantic Web Conference (ISWC2003), Sanibel Island, Florida, October 20, 2003. Available online:
https://arxiv.org/abs/1109.0032.
[15] Kent, R.E.: “Semantic Integration in the Information Flow Framework”. Dagstuhl Seminar Proceedings 04391, Semantic Interoperability and Integration, Schloss Dagstuhl, Leibniz-Zentrum fur Informatik GmbH, 2005. Available online:
https://arxiv.org/abs/1810.08236.
[16] The Information Flow Framework (IFF). Start document available from the IEEE P1600.1 Standard Upper Ontology Working Group (SUO WG) Home Page.
http://ontolog.cim3.net/file/resource/historic-archives/IEEE-SUO-WG/.