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 18:18):I assume there are methods for expressing , or the sentence, “some elements of class have property ”, in ologs.
The most fundamental way of forming propositions, from a linguistics perspective, tends to be Subject-Predicate. A predicate can be an intransitive, transitive, or ditransitive verb, amongst other things. It seems like ologs are mainly built to express “transitive” relationships, of SUBJECT VERB OBJECT.
In linguistics, “some” would probably be a “determiner”, forming a “determiner phrase” (DP). Structurally, “some” would take a single noun as its complement / argument. I wonder if in an olog, “some” could be a morphism from class of entities to ? (An endomorphism). Like this:
.
But this wouldn’t keep with the idea of an object being “a class of things”. Instead, “some” could be an arrow between the class of all such things, and the class of such things further delimited by a property:
.
John Baez (Mar 12 2024 at 18:54):Julius Hamilton said:
I assume there are methods for expressing , or the sentence, “some elements of class have property ”, in ologs.
I don't think so: if an olog is just a category and a model of it is just a functor to , they represent a very primitive, inexpressive form of logic! You could say a functor is a database where the objects of are types of things, you have a set of things for each type of thing , and you have a map between such sets for each morphism in .
E.g. you could have a type "women", a type "men", a morphism "father of", and a database that lets you record a set of women, a set of men, and for each woman who is their father.
THAT'S ALL.
There are many levels of categorical logic. Usually people say we get and when we reach the level of [[regular categories]] - see also [[regular logic]]. Ologs are way down in the depths.
John Baez (Mar 12 2024 at 18:56):The advantage of very primitive forms of logic is that it's easy to do the necessary computations to solve problems in these forms of logic - e.g., get the list of women from a database, and who is which woman's father.
As you move up the ladder you get richer, more expressive systems, and eventually you hit Goedel's incompleteness theorem and (closely akin) the phenomenon of undecidability and uncomputability.
John Baez (Mar 12 2024 at 18:57):On the other hand, doing right and left Kan extensions of functors between categories involves a version of and , and these ideas are important for ologs - but not working within a single model of a single olog!
Julius Hamilton (Mar 12 2024 at 19:10):Could you provide an example of doing a Kan extension of a functor between ologs?
John Baez (Mar 12 2024 at 19:12):I taught a course on such stuff based on Brendan Fong and David Spivak's book, so I'll point you to my lecture notes - see lectures 49, 50 and 51. I don't say the word "olog", but I show how Kan extensions are used for databases.
Ryan Wisnesky (Mar 12 2024 at 21:58):the CQL software has dozens of built-in examples of left and right kan extensions of databases along functors and ditto for pro-functors, and has a "chase engine" that performs model completion against regular logic formulae; regular logic is in fact the standard logic used by database theorists working on data migration/integration. all of these things are difficult to compute at e.g. gigabyte scale, and undecidability occurs immediately (in e.g. just checking functoriality of mappings). Anyway here are some slides from the CQL perspective https://www.categoricaldata.net/cql/lambdaconf.pdf