Revision b0a1478b-d5b7-4125-8b20-c4d51fb44f00 - Theoretical Computer Science Stack Exchange

The Question in short
=====================

Here is the question in its pure form. Details of my reasoning can be found below.

The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of predicates. The way they define a Model is Isomorphic to the following type definition.

$RDFModel = \mathscr{P}(IR \times IP \times IR)$

Note that any Model is thus a [Quiver](https://ncatlab.org/nlab/show/quiver) as can be seen by noticing that for any $M: RDFModel$ the first and third projections give us the functions we need:

$ \pi_1, \pi_3: M \to IR$

so that the graph representation of a model below is justified. 

Anyway since RDFModel is a powerset one can look at it as a poset category where the element Models built from a set of Resources R and Predicates P are the objects, and the morphisms are the subset relations. Call this category $\Bbb{M}_{RP}$

Questions:

 1. Is such a Poset category $\Bbb{M}_{RP}$ what an RDF Institution would send a Signature $\Sigma$ to? Ie is this the right type $ Mod(\Sigma): \Bbb{M}_{RP}$ ?
 2. Since there can be many such categories of different sizes depending on IP and IR ([Appendix B: Finite Interpretations][1]), it is likely that these categories of poset can form a category which we could call $\Bbb{M}$. (Somewhat like the category of boolean algebras). Is that the category that the functor $Mod$ has as range? Ie. $Mod: Sig^{op} \to \Bbb{M}$
 3. In the category $\Bbb{M}$ what is the smallest category (initial or final object?)
 4. Any category $\Bbb{M}$ contains many models so for any such model some sentences will be satisfied others not. In modal logics those are thought of as possible worlds. But in David Lewis' sense those are complete objects. It looks like possible worlds must be fixed points - or final objects - in a category of models of ever increasing size. Is there a way to capture these purely category theoretically? (Also can one call those mini models possible worlds?)
 5. Is there a way to state how the open world assumption works in this context?

Context of the Question
=======================

The [RDF1.1 semantic spec][2] comes with a simple model discussed in a [previous Stack Exchange question](https://math.stackexchange.com/questions/2905226/what-kind-of-categorical-object-is-an-rdf-model/2905287#2905287). The aim of this question is to see how that can be brought into the larger space of [Category Theoretical Institutional Theory][3] started by the famous computer scientist [Joseph Goguen][4]. The longer term aim is to make sense of modal logic in RDF. For a list of academic papers on Category Theory and RDF as well as institutional theory and modal logic see [RDF and Institution Theory (IT) message on ncatlab][5]. These papers are good at locating things in the abstract framework, but don't even get into the detail of what the RDF Models are. I just want to make sureI understand correctly what is going on by developing some simple examples. 

Example using RDF1.1 modelling
------------------------------

So here is a simple example Model written out in the structure presented by the [RDF1.1 semantic spec][2]. (As we will see a bit further below this can be made a lot easier to understand with arrow diagrams) We need a set of Resources IR, and Predicates IP,  so I chose a simple example with 6 objects in IR, 5 Properties in IP and 4 types of relations on IR

[![Illustration of model as described by RDF 1.1 Semantics spec][6]][6] 

I start with predicates in terms of colors to emphasize that we are dealing with models here. Later we move on to syntax, and so it will be natural to have names for the colored arrows. Initially we just want to say the world contains distinctions. Here the colors represents type of relations, grey {0} for is "older than", dark green {1,3} for "shook hands", light green {2,4} for "knows", pink {5,6} for the relation relating a person to a statement written on their T-Shirt, and light blue {7,8} relating a person to their name (another literal). 

Making the model simpler using Triple based Graphs
--------------------------------------------------

We have shown in a [previous Stack Exchange question](https://math.stackexchange.com/questions/2905226/what-kind-of-categorical-object-is-an-rdf-model/2905287#2905287) that way of writing things to be isomorphic to the following definition of $RdfModel$ 

$RdfModel = \mathscr{P}(IR \times IP \times IR)$

So that we can redraw the above diagram in the much clearer category
theoretical diagramatic style. We can justify this mathematically because Category Theory defines a [Quiver][7] - which other call a Graph, and other call a Directed Graph - as two sets A and N and two functions $domain$  and $codomain$ such that

$domain, codomain: A \to N$

Clearly we have these here since the first projection of $RdfModel$ could be thought of as the $domain$ and the third projection as the $codomain$ function. Note also that every Quiver gives rise to a free category. 

What models add to a Quiver is that it can state that a number of arrows have the same type, which we express here by giving arrows colors.

[![an RDF Model as explained by W3C RDF1.1 spec][8]][8]

This image of Vint Cerf shaking hands with Tim Berners-Lee should make it
more intutive, and help show why this is useful, as it helps us describe things like Tim meeting Vint.

[![Vint Cerf And Tim Berners-Lee][9]][9] 

As practical semanticist we like to have non set elements in the sets of our Models to describe practical stuff like that, and that is fine: we have a [category of Sets with Ur-elements][10] we can work with.

Ok, that is for an illustrated background.

Simple Category of Models organised by subset inclusion
-------------------------------------------------------

Now given that any graph is a subset of $IR \times IP \times IR$ we can
draw up a simplified version of the relation between all such models using just the subset Partial Order that stems from such a set of subobject (Category Theory's generalisation of the notion of subsets - do we need to generalise? Who knows: it could be useful...). Because this works with powersets and these quickly explode in complexity I have limited myself to 4 elements of IR, to real objects and 2 literals, and 2 types of relations: "older than" and "has name". 

[![category of subset ordered rdf models][12]][12]

In yellow above are all the models that fit the actual world. The most comprehensive such model is M7. In light blue we have different possible worlds/models (I may be able to have different shades for different incompatible possible worlds there). The biggest graph before Top N8 models worlds where Tim and Vint have the same age, worlds which presumably would require quite a lot of change to the actual one - some complex scenario involving Vint being frozen for over a decade or so before being born... In pink we have models that we don't really want to allow at all, such as model X1 which states that Tim is older than the literal "Vint Cerf", or X2 where Tim is related by the name relation to Vint (but Vint Cerf is a person not a name). X3 is the union of that nonsense (are these what one would term impossible worlds?) [RDFS][13] and Description Logic Based [OWL][14] vocabularies allow one to exclude those as models, but I think the basic minimal RDF framework does not. 

We can see that moving up any arrows into a model (eg M7) is the union of the models into it, which form a logical conjunction or a categorical coproduct. Moving in the opposite direction, say looking at the opposite category we have arrows out of a model such as M7 form its logical disjunctions, or categorical products. 

Relating to Institution Theory
------------------------------

  This brings us to [Institution Theory][15]. The few articles on [RDF and Institution Theory (IT)][5] explain as any IT intro does that an institution consists of 

 1. a category of $Sig$ of Signatures $\Sigma$: For our example we could have a ground graph signature $\Sigma$ containing only a small subset of IRIs and some literals to correspond to the objects in our model. (No existential quantifiers (aka blank nodes) for example). IRIs are just the web equivalent of mathematical symbols, designed so that people can globally coin new symbols without fearing a name clash. They stand for International Resource Identifiers and are specified syntactically by [RFC3987][16]. IRI ⊇ URI ⊇ URL ∪ URN 
 2. a functor $Mod$ from $Sig^{op}$ to $Cat$ the category of categories selecting for each object in the category $\vert Sig \vert$ a category of models. So I guess that a signature with 4 IRIs and 2 literals can give us a signature to the category of Partially ordered models I drew above.
 3. a functor $Sen$ from $Sig$ to sets of Sentences in $Set$ (here we need no ur-elements I think, since we can encode the Unicode alphabet with the empty set and sets thereof)
 4. A relation $\models_\Sigma \space \subseteq \vert Mod(\Sigma) \vert \times Sen(\Sigma)$

But those papers don't really tell me what such a category of models is. So that's what I am trying to make sure I have understood correctly with the simple example given above.

Now, IT does not state what their set of sentences look like. RDF has so many different syntaxes (RDF/XML, NTriples, Turtle, JSON-LD, ...) to cater to the different (at times religious) fashions that it would be silly to put real syntactic sentences there. Better have sets of [Abstract Syntax Graphs][17] as our sentences. As it happens those look very much like our models. If we can distinguish just IRIs and Literals types as defined by IETF and W3C, and just define the type 

$GNode = IRI+Literal$

We may want to specialise this to a signature $\Sigma$ which only contains a subset of IRIs and Literals needed for a model (as the RDF1.1 Semantic web syntax hints at in [Appendix B: Finite Interpretations][1]). So we could have $\Sigma_{IRI}$ to refer to the set of IRIs used by that signature, $\Sigma_{Literal}$ to refer to the set of Literals used by that signature and $\Sigma_{GNode}$ to refer the disjoint union of the IRIs and Literals of that signature.

Then we can define the type of (syntactic) RdfGraph for a signature as

 $Sen(\Sigma) = \mathscr{P}(\Sigma_{GNode} \times \Sigma_{IRI} \times \Sigma_{GNode}) $  

which clearly is a subcategory of our Models. It would be interesting to regard that indeed as a category, in which case we could get from those to the Set required by Institution Theory by selecting the set of objects $|Sen(\Sigma)|$ of our signature.

So now I suppose if G7 is the top yellow model in the model Poset category above then given that 
$ ":" : IRIRef \times String \to IRIRef$

is the append operation on the string component of a IRIRef, and we have defined the strings 

    foaf = <http://xmlns.com/foaf/0.1/>
    timbl = <https://www.w3.org/People/Berners-Lee/card#i>

where surrounding a string with angle brackets turns it into a IRI reference (as opposed to a literal string)

$ G7 \models \text { { timbl  foaf:name "Tim Berners-Lee" . }}$

but so does the top green model $J7$ where Tim and Vint have the same age

$ J7 \models \text { { timbl  foaf:name "Tim Berners-Lee" . }}$

So I guess now that the category which is the range of the $Mod$ functor - which remember maps each signature $\Sigma$ to a category of models - must be a category with growing number of objects in IR and PR, up to something like infinity. The morphisms in this category would relate one poset category to the next, in a way that is faithful to the poset structure in some way - presumably by keeping the same types of distinctions. (I am not quite sure what this is yet) 


  [1]: https://www.w3.org/TR/rdf11-mt/#finite-interpretations-informative
  [2]: https://www.w3.org/TR/rdf11-mt/#simple-interpretations
  [3]: https://en.wikipedia.org/wiki/Institution_(computer_science)
  [4]: https://en.wikipedia.org/wiki/Joseph_Goguen
  [5]: https://nforum.ncatlab.org/discussion/9002/abstract-model-theory-institutions-modal-logic-contexts/
  [6]: https://i.sstatic.net/7mQfY.png
  [7]: https://ncatlab.org/nlab/show/quiver
  [8]: https://i.sstatic.net/tuHKT.png
  [9]: https://i.sstatic.net/7RYxy.png
  [10]: https://math.stackexchange.com/questions/2909429/is-there-a-category-set-with-ur-elements
  [11]: https://i.sstatic.net/pgrAx.jpg
  [12]: https://i.sstatic.net/k6teO.png
  [13]: https://www.w3.org/2001/sw/wiki/RDFS
  [14]: https://www.w3.org/2001/sw/wiki/OWL
  [15]: https://www.iep.utm.edu/insti-th/
  [16]: https://tools.ietf.org/html/rfc3987
  [17]: https://www.w3.org/TR/rdf11-concepts/