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.
Julius Hamilton (Mar 12 2024 at 19:48):I am updating my understanding of what an olog is. The most standard notion of what it is, is, you have a sort of “abstract category” where the “objects” are, internally, not really anything. Just as we name objects of a category by variable names like “A”, “B” and “C”, we could consider the “text labels” of an olog to be variable names in the exact same way - an object named “trains”. Necessarily, an olog has a functor to . This functor maps exactly a word to the set of real-world referents of that word - like a “denotation functor”, it maps a denotation to what is being denoted.
I have one issue about this. We are commonly told that sets, as “collections of things”, can be collections of anything, like a paintbrush, a cloud, etc.
However, when you construct the sets of a set theory, you start with the empty set, and all further sets are defined as sets containing any previously constructed sets. From that perspective, the elements of a set are always other sets. To say there is a “set containing Oscar Wilde” means that there is some specific set, say, ordinal 3, that is taken by convention to represent the person Oscar Wilde.
How can we justify claiming there is a “set of all trains”? If we are to be mathematically rigorous and use sets as they are actually defined in set theory, there is no “set of all trains”. Do we assume that since there is some finite number of trains in the world, that intuitively, for each element of some ordinal set , we shall associate a specific train with that set?
Wikipedia says there are other options for the “target category” of an olog:
Another target category that can be used is the Kleisli category of the power set monad. Given an , is the power set of . The natural transformation maps to the singleton , and the natural transformation maps a set of sets to its union. (…) The verb phrases used with this target category would need to make sense with objects that are subsets: for example, "is related to" or "is greater than".
I will expand the above definition in an edit to this message asap. I wanted to say I think the idea is that this actually restricts the semantics of an olog rather than broadening them.
John Baez (Mar 12 2024 at 19:54):There's a lot to say about this.
When you construct the sets of a set theory, you start with the empty set, and all further sets are defined as sets containing any previously constructed sets. From that perspective, the elements of a set are always other sets.
That's a certain historically very popular approach called "material set theory". Most people here like a different approach called [[structural set theory]]. I think I heard you or someone recently saying something about ETCS. That's an example of structural set theory.
John Baez (Mar 12 2024 at 19:54):But even structural set theory as most mathematicians do it will not give you a set of trains!
John Baez (Mar 12 2024 at 19:55):Luckily a database does not need to contain an actual train.
John Baez (Mar 12 2024 at 19:55):It's enough for it to contain some data - strings of 0's and 1's, or letters, or numbers, or whatever - which refer to a train.
Ryan Wisnesky (Mar 12 2024 at 22:03):David Spivak develops the theory of ologs for such Kleisli categories here: https://arxiv.org/abs/1209.1011 . Although nice for modeling "in" the olog, one drawback of this approach is that, using the terminology of institutional model theory, you lose the left and/or right adjoints to the model reduct functor "outside" the olog. So e.g. in CQL, we would lose at least one of its sigma/pi operations, and hence opted to follow the traditional Set-based approach (and extend it).
Julius Hamilton (Apr 15 2024 at 22:39):I have been thinking a lot about ologs and now my view is shifting to consider their expressive power. Spivak has explicitly mentioned that ologs portray “facts”, can be “translated” into natural language “readings”, and are a way of showing the structure of language.
I am curious how ologs could express “if-then” propositions.
For example, “if x is a bug, then it has wings y”, is the same as saying “a bug x has a pair of wings y”. Does that mean that all the arrows in an olog can already be read as material implication?
But what if it is conditional? If a person eats hot sauce, then their mouth will feel spicy. I guess this could go, “a person x” |is associated with|<-- “a person x who eats a hot sauce y” —>|is associated with| “a hot sauce y”
I feel like ologs are good for talking about atemporal truths, but I am not sure what useful facts they can be used to “prove”, in that case.
In order to say a person who eats hot sauce will experience spiciness, I have to indicate that as a state, not a defining condition.
It’s as if the olog has to have a second layer where abstract ideas like “a person” are “instantiated” into time and space. Like, “an instance of a person who eats a hot sauce” is associated with “an instance of a spicy feeling”.
Ryan Wisnesky (Apr 16 2024 at 00:10):for Set-valued ologs, you would need pullbacks or Horn clause logic to specify if-then reasoning. (Or a type side.) We see rules like "for every person P such that P.age > 18 there exists an Adult a such that a.id = p.id" in data integration all the time; these are if-then rules. In fact, the datalog language itself is basically nothing but if-then rules. Anyway, these are called "constraints" in CQL and they admit "model completion" meaning you can take a model that doesn't satisfy the if-then rules and find a unique extension of that model that does satisfy the if-then rules (something that isn't true for arbitrary logic).
Julius Hamilton (Apr 16 2024 at 00:12):That’s amazing. I wish I could consult with you more about my attempts to do some formal modeling. Is there any good set of steps for designing one, like, “first define essential nouns, then list possible relations, then start trying to prove properties”?
Ryan Wisnesky (Apr 16 2024 at 01:06):Sure, as a first introduction to data modeling often cs undergrads learn the 'entity relationship model' as well as how to implement such models using SQL. https://en.wikipedia.org/wiki/Entity–relationship_model and http://infolab.stanford.edu/~ullman/fcdb/aut07/slides/er.pdf
Julius Hamilton (Apr 16 2024 at 01:55):Thanks.
I’m wondering if there are any reference materials comparing the “expressiveness” of a logic, in a mathematical sense, to what therefore it is suitable for expressing in the real, ontological world.
For example, David Spivak developed a temporal type theory. This seems to imply that such a system is optimal for expressing temporal phenomena. And yet, why would other formal methods be inadequate for that?
I’m trying to get a stronger understanding of how things like ologs, description logic, datalog, etc, are better or worse for different kinds of models.
Most of the models I want to make have some kind of “human” element in them - human experience, perception, emotion, etc. For example, imagine modeling how a certain business organization structure might affect the employees’ well-being. I need to figure out what kinds of concepts are going to be expressed, and which structure has that capability best. I guess it’s partially like a formal ontology. https://en.m.wikipedia.org/wiki/Formal_ontology
Ryan Wisnesky (Apr 16 2024 at 02:20):It is indeed possible to translate temporal logic to first order logic: https://plato.stanford.edu/entries/logic-temporal/#StaTraTLFirOrdLog . Gentzen even proved Peano arithmetic consistent by translation to the system of primitive recursive arithmetic + induction on trees. Sometimes, hierarchies of logics form: https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory . But asking for an "optimal" logic is like asking for an "optimal" airplane - different logics have different trade-offs.