Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Ologs

Julius Hamilton (Mar 10 2024 at 23:52):

work in progress
commentary welcome
last updated 3/10/24 7:48 p.m.

Wikipedia Policy as an Olog

Consider the task of making an olog that codifies the Wikipedia editorial guidelines. One could start with Wikipedia’s “Five Pillars” as a simple exercise before expanding to a more robust version.

They are[1]:

“Wikipedia is an encyclopedia.” (WP:5P1)
“Wikipedia is written from a neutral point of view.” (WP:5P2)
“Wikipedia is free content that anyone can use, edit, and distribute.” (WP:5P3)
“Wikipedia's editors should treat each other with respect and civility.” (WP:5P4)
“Wikipedia has no firm rules.” (WP:5P5)

David Spivak presents the olog in [2], saying, “Ologs are basically categories which have text labels to explain their intended semantic” [2, §7]. The simplest rules for making an olog are as follows:

The objects of the olog are types of things.
The morphisms of the olog are aspects of those things.
A morphism between two objects represents a functional relationship between two things: it is something true for every member of the class, and that is uniquely determined for each member of the class under that relation; i.e., “There is only one correct answer.” If you have two brothers, then there is not a single correct answer to the question “Who is your brother”?

Preliminary Example

working draft of a wikipedia olog

Bibliography

[1]: Wikipedia contributors. Wikipedia:Five pillars. Wikipedia, The Free Encyclopedia. https://en.m.wikipedia.org/wiki/Wikipedia:Five_pillars. Accessed March 10, 2024.

[2]: Spivak, D.I.; Kent, R.E. (2012). Ologs: A Categorical Framework for Knowledge Representation. PLoS ONE 7(1): e24274. doi:10.1371/journal.pone.0024274

Work-in-progress questions:

How would I write this in Coq?
Why does an olog object have to be “a class of things”? Why can’t it be “just anything”?
How do you represent single things like “Wikipedia” if an olog object has to be a class of things, like “a website / websites”?
How do ologs prove the consistency and completeness of a set of verbal principles, such as a law?
Why do ologs require functional relationships? What useful properties does that grant?

John Baez (Mar 11 2024 at 00:16):

To make superscripts I only know two hacks. One is to use LaTeX, e.g

this ${}^3$

is made with a LaTeX command. (You can see my source code by clicking on the three dots at right.)

Another is to grab unicode superscripts off someplace like YayText, e.g.

this²

Ryan Wisnesky (Mar 11 2024 at 06:14):

The CQL tool at categoricaldata.net automatically emits Coq code from olog definitions. And TPTP code too. Your other questions have... deep answers

Spencer Breiner (Mar 11 2024 at 13:35):

Julius Hamilton said:

Why does an olog object have to be “a class of things”? Why can’t it be “just anything”?

The reason for this is that, given an olog $C$ , a model of $C$ is a functor $C\to {\bf Set}$ , and a set is a class of things, not an individual.

There are some subtleties. For any individual $x\in X$ , you can talk about the singleton $\{x\}$ . The problem is that all singletons are isomorphic, and the singleton $\{x\}$ doesn't really "know" its identity. Instead, individuals in ologs should be represented as a relationship between an abstract individual (the terminal object, often written $1=\{*\}$ ) and the original set $x:1\to X$ . This is called a [[global element]].

Julius Hamilton (Mar 12 2024 at 03:54):

given an olog $C$ , a model of $C$

Could you define “model”? Does it mean any sort of real world object which the olog describes?

is a functor $C\to {\bf Set}$ , and a set is a class of things, not an individual.

Is it in the definition of ologs that the text labels are actually just a shorthand for a functor from the objects of $C$ to a “set of some things” in ${\bf Set}$ ?

For any individual $x\in X$ , you can talk about the singleton $\{x\}$ . The problem is that all singletons are isomorphic, and the singleton $\{x\}$ doesn't really "know" its identity.

What do you mean? I as a human can look at $x$ and see what it is. But you mean the singleton lacks any internal structure to express any difference between values of $x$ ?

Instead, individuals in ologs should be represented as a relationship between an abstract individual (the terminal object, often written $1=\{*\}$ ) and the original set $x:1\to X$ . This is called a [[global element]].

So to represent “the site Wikipedia”, I could consider the class of all websites, and imply one has been chosen by a mapping from the singleton set. What is the text label of the singleton / terminal object, in the olog, though? I would be expecting a sentence, like, “[Wikipedia] [is] [a website]”. If the singleton selects Wikipedia from the collection of all websites, does the word Wikipedia appear on the olog? Where?

Perhaps the sentence would be, “[an individual] [selects] [a website]”?

John Baez (Mar 12 2024 at 05:31):

Julius Hamilton said:

Spencer Breiner wrote:

given an olog $C$ , a model of $C$

Could you define “model”? Does it mean any sort of real world object which the olog describes?

is a functor $C\to {\bf Set}$ [...]

Spence actually did define "model": in this context, it's a functor from $C$ to ${\bf Set}$ .

There's no better definition than that. So perhaps what you're asking for is some things that Spivak does with models?

Julius Hamilton (Mar 12 2024 at 05:40):

Is this a standard use of the term “model” in category theory? Is it the same notion as that of “model” in logic and model theory? I.e., the idea of mapping a syntax to a semantics; a symbolic notation to some object it describes.

A presheaf is a contravariant functor to ${\bf Set}$ . It seems like a fundamental idea that categories are often studied by their mappings into ${\bf Set}$ . Does ${\bf Set}$ retain a special place in category theory as a way of grounding abstract structures in “real/concrete things”?

John Baez (Mar 12 2024 at 05:47):

Julius Hamilton said:

Is this a standard use of the term “model” in category theory?

No. There are many definitions of "model" in category theory. Apparently this is Spivak's definition of "model of an olog". At least, that's what @Spencer Breiner is telling us.

John Baez (Mar 12 2024 at 05:51):

Julius Hamilton said:

Does ${\bf Set}$ retain a special place in category theory as a way of grounding abstract structures in “real/concrete things”?

One reason ${\bf Set}$ retains a special place in category theory is that for any two objects in a category there is a set of morphisms from the first object to the second object. This has enormous effects throughout category theory.

If you change this - if you decide to have some other sort of thing of morphisms, a thing that's an object in some category $\mathbf{V}$ - then you're doing a generalization of category theory called " $\mathbf{V}$ -enriched" category theory. Then $\mathbf{V}$ will take the place of $\mathbf{Set}$ in much of your work.

Julius Hamilton (Mar 12 2024 at 05:54):

Is there a generalization of the definition of a category where it does not matter what type of object the collection of morphisms form?

John Baez (Mar 12 2024 at 05:55):

Not that I know of. It would seem hard to work with something where you have no clue what type of object the collection of morphisms forms.

Julius Hamilton (Mar 12 2024 at 05:56):

What if you left V as a variable, stating that it was simply some category?

John Baez (Mar 12 2024 at 06:11):

So for each pair of objects $x$ and $y$ the thing of morphisms from $x$ to $y$ could be an object in some category, but that category could depend on $x$ and $y$ ?

Julius Hamilton (Mar 12 2024 at 06:18):

A model of an olog $C$ is a functor from $C$ to ${\bf Set}$ .

It was said above that this is why an object in an olog should be taken to represent “a class of things”. Why does that imply that?

Does that mean that we can only design ologs so that there would be a possible functor into ${\bf Set}$ ?

Does that mean that it is ultimately the structure of ${\bf Set}$ that ologs are grounded in? I.e., we could eliminate the idea of “a category with text labels”, and instead just say, “any subcategory of ${\bf Set}$ is basically an olog; just assume each set represents a concept.”?

John Baez (Mar 12 2024 at 06:22):

If you answer my last question I'll be able to continue the conversation.

John Baez (Mar 12 2024 at 06:23):

I can't hop around from topic to topic without getting resolution on one at a time.

Julius Hamilton (Mar 12 2024 at 06:23):

John Baez said:

If you answer my last question I'll be able to continue the conversation.

I am - my above was being drafted while your last message was sent. My response to your last message is forthcoming.

John Baez (Mar 12 2024 at 06:23):

Okay, thanks.

Julius Hamilton (Mar 12 2024 at 06:35):

John Baez said:

So for each pair of objects $x$ and $y$ the thing of morphisms from $x$ to $y$ could be an object in some category, but that category could depend on $x$ and $y$?

My thinking was that it felt undesirable to have to choose a specific, particular category, if it would have so much of a bearing on how the remainder of the theory became. If ologs have a special relationship to ${\bf Set}$ in the same way that all categories whose collections of morphisms form sets do, then it makes me wonder why we don’t instead study ologs enriched over other categories. But it would be dissatisfying to not know which enrichment is the best one, to study the world of concepts. Thus, it would be better if there was something which generalized all possible choices, so we did not have to worry that we were studying the potential of ologs from only one angle while missing others. I guess you could study 2-ologs, whose morphisms form categories.

Also, I understand Lawvere created the ETCC, but there were some problems with it, and then he made the ETCS. It seems like the ETCS still considers sets as a kind of fundamental concept you need in order to build up the rest of category theory, I guess.

The original question was, if an olog is an attempt to model semantic and/or conceptual relationships, why should it do so by choosing general classes of entities as one of its fundamental building blocks?

I think it is because ontologies in general do this. So my next thought is about how ontologies represent “specific identity”.

(John Baez, you may or may not realize it, but these conversations are really helpful to me. It may not seem like I developed a clear result, but it actually does help me realize where I need to direct my thinking.)

Ryan Wisnesky (Mar 12 2024 at 06:58):

some thoughts: first, in the modern approach to embedding query languages into lambda calculi using monad comprehensions, the monad can vary, from lists to bags to sets to trees etc. This approach is expressive enough to capture ontologies and more, and e.g. many optimizations work for some monads and not others. Second, the category Set is privileged simply because logicians and computer scientists already know a lot about modeling things with sets, and have tooling as well (theorem provers, etc). Third: when categories are understood as database schemas, a morphism is a foreign key and so a 'morphism between morphisms' doesn't quite make sense. However, categories of queries tend to have nice higher structure, with morphisms between morphisms representing e.g. inclusions between queries. Fourth: Besides CQL, to author ologs, there's algebraic Julia, and EASIK, and many CT libraries in Coq, Haskell etc implement co-presheaves and kan extensions etc

Julius Hamilton (Mar 12 2024 at 07:01):

Could you provide an example of “embedding a query language into a lambda calculus using a monad comprehension”?

Julius Hamilton (Mar 12 2024 at 07:02):

Can you provide more information on what you mean by a morphism being a “foreign key”?

Eric M Downes (Mar 12 2024 at 07:17):

(Julius Hamilton) It seems like the ETCS still considers sets as a kind of fundamental concept you need in order to build up the rest of category theory, I guess.

FWIW, ETCS (Elementary Theory of the Category of Sets) is not intending to "build up the rest of category theory", it is a different axiomatization of set theory. It is perhaps most useful for doing proofs at the undergraduate level in a style that more easily generalizes to other topoi, than "ZFC style" proofs that emphasize sets composed of concrete elements. In fact, my understanding is that the germ of this project grew in a very practical way out of Lawvere's teaching responsibilities. Here is a very nice and readable summary of the "material set" (ZFC) vs. "structural set" (ETCS) approach that is also a great sales pitch for HoTT
https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html

As to wether sets are a fundamental concept needed vs. merely a very convenient concept... I encourage you to read the opening chapter of MacLane, and then look through the 10 axioms on Tom Leinster's arxiv paper summarizing ETCS. Can you replace the axioms concerning sets with arrows, along concepts from the "arrows only" approach to category theory that MacLane mentions, and still get everything to work? I found trying to do this to be a very fun and enlightening exercise, and as it seems like you are interested in foundational questions, you might as well.

I have no wisdom or insight to share about ologs, however! Good luck!

Morgan Rogers (he/him) (Mar 12 2024 at 11:55):

Julius Hamilton said:

My thinking was that it felt undesirable to have to choose a specific, particular category, if it would have so much of a bearing on how the remainder of the theory became. [...] It would be dissatisfying to not know which enrichment is the best one, to study the world of concepts. Thus, it would be better if there was something which generalized all possible choices, so we did not have to worry that we were studying the potential of ologs from only one angle while missing others.

This is a trap. Abstraction is a tool for figuring out what features of a situation make something work. If you haven't selected that "something" ahead of time, you have no criteria for success. Think first about why you want to study ologs. What types of structure is required to capture [thing you want to describe using ologs]? That will either tell you a specific V or required properties of the enrichment. And it is preferable to pick a V which works and run with it before generalizing, because otherwise you will not be able to say anything concrete at the end of the day.

Spencer Breiner (Mar 12 2024 at 14:19):

Hi @Julius Hamilton,

This is a great set of questions. I'll try to get back to the rest soon.
Julius Hamilton said:

given an olog $C$ , a model of $C$

Could you define “model”? Does it mean any sort of real world object which the olog describes?

One of the main insights in categorical logic is that "a model is a mapping". The things that go into the mapping are called "syntax", and the things that come out are "semantics". The remarkable thing is that you have a lot of flexibility in choosing what those mean; not only do you choose what those are, you get to choose what kind of (mathematical) thing they are as well.

To connect this up with classical logic, we can decide that syntax and semantics will be Boolean algebras. Often, we also fix the semantic algebra to be $2=\{\top,\bot\}$ . Now the syntax $B$ can be any Boolean algebra (usually thought of as a propositional theory), and a model $M\models B$ determines a homomorphism $\overline{M}:B\to 2$ by setting $\overline{M}(b)$ to $\top$ if $M\models b$ and $\bot$ otherwise. However, we can also interpret $B$ in other Boolean algebras. For example, if $B$ was a theory of individual characteristics ("likes pizza") and $I$ is a set of people, then we could also give a model to the power set $B\to {\mathcal P}(I)$ by sending $b$ to $\{i\in I\mid i\models b\}$ .

For ologs, we are deciding that syntax and semantics will be categories and models will be functors. Then we decide that semantics will be sets and functions, but we can absolutely make other decisions, with sets and relations or vector spaces and linear maps being particularly important examples.

Ryan Wisnesky (Mar 12 2024 at 14:33):

Julius Hamilton said:

Could you provide an example of “embedding a query language into a lambda calculus using a monad comprehension”?

Sure, one classic is Wong's thesis, 'querying nested collections' https://www.semanticscholar.org/paper/Querying-Nested-Collections-Wong/b9cd5bc118045ea4ba3d2630eed1f3c3d0d351be

Ryan Wisnesky (Mar 12 2024 at 14:36):

Julius Hamilton said:

Can you provide more information on what you mean by a morphism being a “foreign key”?

If we look at an OLOG schema or EA Sketch such as attached, then every arrow in the diagram denotes relational database theorists call a "foreign key" constraint/skolem function https://en.wikipedia.org/wiki/Foreign_key, basically, these say that in the model, for every row in the source table, there exists a corresponding row in the target table. For example, we might have a (presumably injective) foreign key from Student to Person. SQL databases like Oracle have lots of foreign keys in practice
Screenshot-2024-03-12-at-7.34.02AM.png

Julius Hamilton (Mar 12 2024 at 15:32):

I noticed that Spivak presents an example of an olog that includes an object labeled by a proper noun.

arginine

I am going to turn to a philosophy forum to explore the question of what characterizes proper nouns as opposed to noun classes. Mathematically, it calls to mind quantifiers. In ZFC, entities with specific identities comes before the ability to define “a class of things sharing a property” (restricted set comprehension).

I may break this thread into new sub-threads to organize some of the different aspects and focus on each one.

John Baez (Mar 12 2024 at 16:28):

Julius Hamilton said:

John Baez said:

So for each pair of objects $x$ and $y$ the thing of morphisms from $x$ to $y$ could be an object in some category, but that category could depend on $x$ and $y$ ?

My thinking was that it felt undesirable to have to choose a specific, particular category, if it would have so much of a bearing on how the remainder of the theory became.

It's an interesting thought, but I don't think we can let the things of morphisms between each different pair of objects be objects in different category without choosing some way for these different categories to "talk to each other". Otherwise we couldn't do much with these morphisms.

Escaping the hold of contingent, arbitrary historical decisions is part of the goal of category theory, but even more important is finding formalisms that really "hum" - that work smoothly and powerfully. @Morgan Rogers (he/him) explained that pretty well.

After decades of work on ordinary $\mathbf{Set}$ -enriched category theory, people were ready to study categories enriched in other categories. Kelly's book Basic Concepts of Enriched Category Theory came out in 1982, and it's quite deep.

You'll notice how I said "categories enriched in other categories" - those second categories are ordinary $\mathbf{Set}$ -enriched categories! So Kelly needed a lot of ordinary category theory to prove theorems about enriched categories. You may consider that a limitation. If so, try doing something better! Improving category theory is always possible - it keeps evolving - but it takes a lot of work and deep thought.