Introduction

 

Namespace

Portal

Hypergraphs

Tradition

Type Languages

Conceptual Graphs

Type Language Colimits

Cyc

Terms

Common Logic

Spangraphs

OKBC

Models

 

 

Overview

 


 


Model theory is the study of the interpretations of any language, formal or natural, by means of set-theoretic or category-theoretic structures. It is the branch of mathematical logic that deals with the relation between a formal language and its interpretations. First-order model theory is the branch of mathematics that deals with the relationships between descriptions in first-order languages and the structures that satisfy these descriptions. Apart from using set theory or category theory, model theory is completely agnostic about the kinds of things that exist. The latter are described and axiomatized in object-level ontologies. The IFF Model Theory Ontology gives a (somewhat novel) category-theoretic axiomatization for first-order model theory based upon the two fundamental ideas of classification and hypergraph (see the two dimensions in Figure 1). Some of the basic notions of model theory are language, sort, sentence, theory, interpretation, model = structure, object, class, universe, model-theoretic truth, and satisfaction. The IFF Model Theory Ontology, which axiomatically represents all of these ideas (and more), is the top level of a three level structure (discussed in the outline below) that is arranged in a 3-dimensional architecture (Figure 2). In support of the IFF Model Theory Ontology are the two lower levels of this structure, which are represented by the IFF Lower Classification Ontology (middle level) and the IFF Lower Core Ontology (lower level).

Architecture

 

There are three dimensions or distinctions that make up the architecture of the IFF Model Theory Ontology.

  1. non-aligned versus aligned
  2. no classification versus classified by instance/type
  3. basic versus indexed.

A concept is aligned when there exists a background function that coordinates its effects. A concept is 2-dimensional when an instance-type distinction is part of the concept. A concept is indexed when there is a secondary indexing structure, part of whose purpose is to restrict cardinality by abstraction with an explicit denotation or indexing function.

This results (Table 1) in seven basic architectural concepts, represented by both an object concept and a morphism concept, and fourteen resulting namespaces for their axiomatization.

Table 1: Architectural Concepts and Namespaces

aligned

classified

indexed

object

morphism

no

no

no

set pair

semiquartet

yes

no

no

function

quartet

no

yes

no

semidesignation

semisquare

yes

yes

no

designation

square

no

no

yes

hypergraph

hypergraph morphism

yes

no

yes

type language

type language morphism

no

yes

yes

model

model morphism

yes

yes

yes

The concepts and namespaces of sets, set invertible pairs (of functions), classifications and infomorphisms are basic, but not architectural. The concepts and namespaces of spangraphs and spangraph morphisms give an alternative architectural view. The concepts and namespaces of type languages, type language morphisms, expressions and type interpretations are extensions to the basic architecture.

 

Text Box: classification 
dimension
Text Box: classification 
dimension

There are several unique aspects of the IFF model-theoretic approach.

·         Abstract tuples are a constituent part of IFF models. This is required in order to define a true “information flow” approach to model theory, where models are actually two-dimensional notions made up of classifications and hypergraphs. In this sense, IFF models are more refined than traditional models. However, they also need more special treatment as witnessed by the need for a more refined notion of satisfaction.

·         The cardinality of arity is unconstrained. This means that one can have relations of infinite cardinality. What this means in actual practice is another question. Can we use vector fields as relations between the elements of the field?

·         The classification between a tuple and an expression only requires that part of the tuple be used in the classification. This seems to be an intuitive and freer notion. For example, the two expressions “John and Mary were married” and “John and Mary were married at 5 o’clock in the cathedral with over one hundred people in attendance” are both examples of classifications of “marriage”, with the first being exact (and trim) and the second only using part of the tuple.

Outline

 

There are three related ontologies in the IFF lower metalevel currently under development.

1.        The IFF Model Theory Ontology (IFF-MT)

2.        The IFF Lower Classification Ontology (IFF-LCLS)

3.        The IFF Lower Core Ontology (IFF-LCO)

It is anticipated that several other ontologies will be developed: an ontology for terms that will be integrated with the model theory ontology, and an ontology for Information Flow theories and logics.

 

The IFF Model Theory Ontology

 


The IFF Model Theory Ontology (IFF-MT) contains two minor namespaces (hypergraphs and spangraphs), two major namespaces (type languages and models), and two portals (Tradition and Conceptual Graphs). More portals will be defined in the future (Common Logic, Cyc, etc.).

 


In detail, the IFF-MT contains the following namespaces (architectural elements are in boldface):

·         Hypergraphs and hypergraph morphisms: Hypergraphs and hypergraph morphisms form the category Hypergraph, which is the functorial pullback (Diagram 1, lower left) of two Set-based functors – the vertical target functor

vert-tgt : horiz(£Set) ® Set

from the horizontal category of the double category £Set of set quartets, and the tuple functor

tuple : rSet ® Set

from the category rSet of set pairs and semiquartets.  Hypergraph enjoys a special relationship with the category rSet. There is a reflection of Hypergraph onto rSet and an embedding of rSet into Hypergraph (Figure 3, lower left). This reflection is mediated in one direction by the underlying reference functor (reflector)

refer : Hypergraph ® rSet

and in the other direction by the hypergraph functor (embedding)

hgph : rSet ® Hypergraph.

·         Type languages and type language morphisms: Type languages and type language morphisms form the category Language, which is the functorial pullback (Diagram 1, lower right) of two Set-based functors – the vertical target functor

vert-tgt : horiz(£Set) ® Set

from the horizontal category of the double category £Set of set quartets, and the signature functor

tuple : horiz(£Set) ® Set

from the category horiz(£Set). Language enjoys a special relationship with the category horiz(£Set). There is a reflection of Language onto horiz(£Set) and an embedding of horiz(£Set) into Language (Figure 3, lower right). This reflection is mediated in one direction by the underlying reference functor (reflector)

refer : Language ® horiz(£Set)

and in the other direction by the type language functor (embedding)

lang : horiz(£Set) ® Language.

·         Expressions and expression morphisms

·         Type language interpretations

·         Spanmodels and spanmodel morphisms

·         Models and model morphisms: Models (model-theoretic structures) and model morphisms form the category Model, which is the functorial pullback (Diagram 1, top) of two Classification-based functors – the vertical target functor

vert-tgt : horiz(¢Classification) ® Classification

from the horizontal category of the double category ¢Classification of classification squares, and the signature functor

sign : pClassification ® Classification

from the category pClassification of semidesignations and classification semisquares. Model enjoys a special relationship with the category pClassification. There is a reflection of Model onto pClassification and an embedding of pClassification into Model (Figure 3, top). This reflection is mediated in one direction by the underlying reference functor (reflector)

refer : Model ® pClassification

and in the other direction by the model functor (embedding)

mod : pClassification ® Model.


The category Model is the vertex of a span of functors (Diagram 2): the underlying instance functor

inst : Model ® Hypergraphop

and the underlying type language functor

type : Model ® Language.

Fibers of the type functor are used to define a fiber (inverse image) operator on type language interpretations. This plays an important role in the IFF approach to the “concept lattice of theories.”

 

The IFF Lower Classification Ontology

 

In a sense, the IFF Lower Classification Ontology (IFF-LCO) is a lower metalevel analog to the IFF (upper metalevel) Classification Ontology. The IFF-LCO provides high level support for the IFF-MT. It provides this support through the following namespaces:

·         Classifications and infomorphisms

·         Semidesignations and classification semisquares

·         Designations and classification squares

 

The IFF Lower Core Ontology

 

In a comparable sense, the IFF Lower Core Ontology (IFF-LCO) is a lower metalevel analog to the IFF (upper metalevel) Core Ontology. The IFF-LCO provides low level support for the IFF-MT. It provides this support with the following namespaces:

·         Sets

·         Invertible pairs of functions

·         Set pairs and semiquartets

·         Functions and quartets

·         Function pairs

·         Relation

·         Endorelations

·         Orders and monotonic functions

·         Graphs and graph morphisms

·         Diagrams

 

Perspective

 

Merriam-Webster

Main Entry: nex·us

Function: noun

Etymology: Latin, from nectere to bind
1 : CONNECTION, LINK; also : a causal link
2 : a connected group or series
3 : CENTER, FOCUS

Main Entry: pre·hen·sion

Function: noun
1 : the act of taking hold, seizing, or grasping
2 a : mental understanding : COMPREHENSION b : apprehension by the senses

 

The hypergraphs and type languages in the IFF Model Theory Ontology represent things via the three fundamental aspects of relation, thematic role (case relation) and entity. In a sense these follow Whitehead’s notions of nexus, prehension and actuality. In the sections on hypergraphs and type languages we will also specify operations (mapping hypergraphs to spangraphs) that reify nexus as a second kind of actuality, and at the same time transform the linking prehension into a binary nexus.

However, these hypergraphs and type languages are based upon the notion of (semi)designation that is axiomatized in the IFF Lower Classification Ontology, where the trichotomy of nexus, prehension and actuality already appears (in a less specified or indexed form). We assume that prehension is relative – that there is no absolutely required prehension. Along one dimension (Figure 2) the nexus-prehension-actuality trichotomy provides a basic framework for the IFF Model Theory Ontology.

1.                    actualities: The peripheral things.

Represented idea: noun, (argument) entity, CG concept.

2.                    prehension: The spokes or connecting links, possibly partitioned into obligatory and optional case.

Represented idea: case (thematic role), argument index, CG arc.

3.                    nexus: The central thing.

Represented idea: verb sense, situation, state of affairs, relation, CG conceptual relation.

Table 2: Thematic roles (case relations)

[who?]

agent

(agentive case)

[using?]

instrument

(instrumental case)

[what?]

thematic object (theme)

(objective case)

[to(for) whom?]

recipient (patient)

(dative case)

[where?]

location

(locative case)

[when?]

time (tense)

(temporal case)

[why1?]

purpose

 

[why2?]

cause

 

[how?]

manner

 

 

epistemic source

 

 

type

 

 

 

(Semi)designations provide the representational base for the nexus-prehension-actuality trichotomy (Figure 4). In the IFF Model Theory Ontology, we view tuples and signatures as mathematical representations of nexus. Tuples represent a free version of nexus, and signatures represent an aligned version of nexus. We view the indexing elements for tuples/signatures as mathematical representations of prehension. The (tuples) signatures of the instance component of (semi)designations represent an nexus-prehension-actuality instance trichotomy, whereas the signatures of the type component of (semi)designations represent a nexus-prehension-actuality type trichotomy. Model-theoretic structures (models) (Figure 1) extend the representational base of (semi)designations to an indexed representation for the nexus-prehension-actuality trichotomy – a representation that provides indexing for nexus, at both at the instance and type level.

 


References

 

Barr, Michael. 1996. The Chu Construction. Theory and Applications of Categories 2.

Barwise, Jon and Seligman, Jerry. 1997. Information Flow: The Logic of Distributed Systems. Cambridge Tracts in Theoretical Computer Science 44. Cambridge University Press.

Chang, C. C. and Keisler, H. J. 1973. Model Theory. Studies in Logic and the Foundations of Mathematics 73. Amsterdam: North Holland.

Enderton, Herbert B. 1972. A Mathematical Introduction to Logic. New York: Academic Press.

Kent, Robert E. 2000. The Information Flow Foundation for Conceptual Knowledge Organization. In Proceedings of the 6th International Conference of the International Society for Knowledge Organization (ISKO). Toronto, Canada.

Mac Lane, Saunders. 1971. Categories for the Working Mathematician, New York/Heidelberg/Berlin: Springer-Verlag. New edition (1998).