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: reading & references

Topic: Bonchi's Diagrammatic Algebra of First Order Logic

Jacob Zelko (May 05 2024 at 00:25):

Hi folks,

I just recently finished watching Filippo Bonchi's Topos Institute Colloquium talk, "Diagrammatic Algebra of First Order Logic" (link to video). It was based on a paper of the same name he co-authored with Di Giorgio, Haydon, and Sobociński. I thought it was a fascinating talk as I have been slowly working through some of Bonchi's other works in rewrite theory, namely being:

• String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
• String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure

I had a few outstanding questions from the talk that I was wondering if folks can help me with as well as thoughts that I wanted to share. Would be curious what everyone thinks!

(P.S. I am making multiple messages here in this Zulip stream to enable easier responses for folks)

Jacob Zelko (May 05 2024 at 00:28):

My first question is that when Bonchi was talking about predicate functor logic, I was curious by how logic operators are captured by the fundamental notion of adjunction. I am still working on building my understanding of adjoints and, subsequently, adjunctions. Could someone explain how logic operator are captured within the notion of adjunctions?

Jacob Zelko (May 05 2024 at 00:31):

Second, Bonchi introduces this notion of "black and white" composition operators in his talk (I included a photo of that slide as follows):

image.png

This was in the context of first introducing the calculus of relations. He referenced that Tarski originated these notions but try as I might, I could not find reference to this notion of defining and constructing operators in this way. Is there a place I can learn more about these "black and white" structures and their origins?

Jacob Zelko (May 05 2024 at 00:33):

It was found and proven by Monk in $1961$ that the calculus of relations did not have a complete axiomatisation and was therefore less expressive than first order logic. What does it mean for something to have a "complete axiomatisation"?

Jacob Zelko (May 05 2024 at 00:36):

When Bonchi introduces the calculus of neo-Peircean relations, he mentions that this is accomplished by changing the syntax from Cartesian syntax to Monoidal syntax and by changing its semantics from binary relations to Monoidal relations. Seen in the following photo, what does syntax and semantics mean broadly in this case?

image.png

Jacob Zelko (May 05 2024 at 00:41):

After the calculus of neo-Peircean relations is introduced, Bonchi introduces these two constants called copier's and discard-er's. It seems like a copier simply creates a set of tuples where all values in each element are the same? Am I reading that right? Is that what is meant by "copier"? And similarly, for discards, is the big idea that they are "discarding" some information from the set? The discard constant is the more confusing of the two for me.

image.png

Jacob Zelko (May 05 2024 at 00:47):

Otherwise, I just had some final thoughts on the talk overall:

• After I finished watching the talk, I was trying to summarize the big idea of what the calculus of neo-Peircean relations gives us. To me, it seems quite fantastic as we can stick to point free reasoning and have a perhaps simplified but equally as powerful toolkit in this calculus to reason about the composition of complex equations. To me, what I thought was quite powerful was the notion of the fact you can now write proofs in this logic as diagram rewrites. I think the big idea is that this calculus provides a fantastic place for one to combine multiple aspects of category theory, logic, and relations together

image.png

Jacob Zelko (May 05 2024 at 00:51):

• Finally, it needs to be stated but the diagrammatic algebra that you get working within the calculus of neo-Peircean relations is absolutely stunning from a purely aesthetic sense. Some of the diagrams (which I copied here) are amazing to me because they both are aesthetically beautiful as well as their significance becomes clear in its diagrammatic language. Here are some of the diagrams but I encourage you to check out more of Bonchi's paper as there are several wonderful diagrams and explanations.

image.png

image.png

Jacob Zelko (May 05 2024 at 00:51):

Any ways, thanks for chatting all! :grinning:

Jean-Baptiste Vienney (May 05 2024 at 03:19):

I started watching the talk and I’ll try to write what I understand about your questions as I progress into it.
Jacob Zelko said:

Second, Bonchi introduces this notion of "black and white" composition operators in his talk (I included a photo of that slide as follows):

image.png

This was in the context of first introducing the calculus of relations. He referenced that Tarski originated these notions but try as I might, I could not find reference to this notion of defining and constructing operators in this way. Is there a place I can learn more about these "black and white" structures and their origins?

The calculus of relation originates from Peirce. He says that later Tarski falled in love with it. So if you want to know more about the origins, you could maybe try to look into resources on Peirce’s work. I only know about these slides by Nathan. At the end, there are two references on the history of the calculus of relations. Maybe interesting for you?

Jean-Baptiste Vienney (May 05 2024 at 03:36):

Jacob Zelko said:

It was found and proven by Monk in $1961$ that the calculus of relations did not have a complete axiomatisation and was therefore less expressive than first order logic. What does it mean for something to have a "complete axiomatisation"?

I think the two issues “no complete axiomatisation” and “less expressive than first order logic” are separate. I’m not sure what they mean exactly. In logic and computer science, it can be difficult to know what a proposition means if you don’t give the full details. For instance if I remember well you can both say “integration is decidable” (i.e. there exists an algorithm to integrate) or “integration is indecidable” (i.e. there doesn’t exist such an algorithm. Everything depends on what problem you’re exactly talking about when you say “integration”. Here, we run into the same issue. It is difficult to know what exactly he means. I would say that a complete axiomatisation of a mathematical object is a set of identities or other kinds of axioms which are verified by the object and which verifies moreover that you can deduce whatever is verified by this object with the sole use of these axioms. “less expressive than first order logic” should mean that you can translate somehow the calculus of relations into first-order logic but not the other way around.

Jean-Baptiste Vienney (May 05 2024 at 03:41):

Jacob Zelko said:

My first question is that when Bonchi was talking about predicate functor logic, I was curious by how logic operators are captured by the fundamental notion of adjunction. I am still working on building my understanding of adjoints and, subsequently, adjunctions. Could someone explain how logic operator are captured within the notion of adjunctions?

I’m also intersected in learning about that. The original reference is Adjointness in foundations
of Lawvere. I’ve started to read it. So, I could maybe explain what I’ve understood later.

Ralph Sarkis (May 05 2024 at 05:14):

Jacob Zelko said:

I had a few outstanding questions from the talk that I was wondering if folks can help me with as well as thoughts that I wanted to share. Would be curious what everyone thinks!

Ugh, I want to answer all these questions, but I have a deadline next week... I first learned about their work on the calculus of relations in this paper during the ACT adjoint school, and I wrote a blogpost with Phoebe Klett here. It is only about the white part of this new paper. (The white and black structure to separate existential and universal quantification are their invention if I understood correctly.)

Ralph Sarkis (May 05 2024 at 05:15):

Jacob Zelko said:

(P.S. I am making multiple messages here in this Zulip stream to enable easier responses for folks)

Btw, you can now quote parts of a message in a reply by selecting the relevant part and clicking '>'.

David Corfield (May 05 2024 at 06:55):

For quantifiers as adjoints you could try the nLab page and references there. Here you can see the adjunctions:
image.png

Jean-Baptiste Vienney (May 05 2024 at 10:22):

What does the notation $Q \vdash_\Gamma \Delta$ mean? I can’t find an explanation in the nLab entry. In particular I don’t understand the difference with $Q, \Gamma \vdash \Delta$.

Spencer Breiner (May 05 2024 at 11:19):

I think that Q is a formula, while $\Gamma$ is a context of typed variables.

Spencer Breiner (May 05 2024 at 11:21):

The contexts might only allow (generating) sorts/types, a opposed to subobjects

Spencer Breiner (May 05 2024 at 11:22):

Wrt logic and adjunctions, I'd say the first thing to understand is why limits and colimits are adjoint to diagonals. That is a baby version of quantifiers as adjoints to pullback.

Alessandro Di Giorgio (May 05 2024 at 11:50):

Jacob Zelko said:

Second, Bonchi introduces this notion of "black and white" composition operators in his talk (I included a photo of that slide as follows):

image.png

This was in the context of first introducing the calculus of relations. He referenced that Tarski originated these notions but try as I might, I could not find reference to this notion of defining and constructing operators in this way. Is there a place I can learn more about these "black and white" structures and their origins?

Hi! The "black composition" is also known in the literature as "relative sum" and I think Peirce was the first to introduce it. Pratt mentions it here

Evan Washington (May 05 2024 at 17:39):

Jacob Zelko said:

It was found and proven by Monk in $1961$ that the calculus of relations did not have a complete axiomatisation and was therefore less expressive than first order logic. What does it mean for something to have a "complete axiomatisation"?

By "the calculus of relations" here, all we mean is the equational theory of relation algebras given by Tarski (and his students). By a "theory" I just mean a set of first-order sentences closed under logical consequence. For a theory $T$ to have a complete axiomatization, we usually mean an "effective" axiomatization. That is, we want to give a finite or recursively enumerable set of sentences that have as their logical consequence the entire theory $T$.

Here's where the connection with first-order logic comes in. The calculus of relations is actually equivalent to first-order logic with at most three variables. But it turns out this fragment is really powerful: within it you can already express Peano arithmetic! But by Gödel's incompleteness theorem, no consistent theory that can express Peano arithmetic can have an effective complete axiomatization.

Evan Washington (May 05 2024 at 17:42):

Also note that Quine's predicate functor logic (another attempt to algebraicize first order logic) has nothing to do with functors or adjoints, but is just an unfortunate coincidence of terminology.

Zoltan A. Kocsis (Z.A.K.) (May 06 2024 at 00:10):

@Evan Washington , you write:

we want to give a finite or recursively enumerable set of sentences that have as their logical consequence the entire theory T.

Alas, I find this a bit misleading. The equational theory $T$ of relation algebras _does_ admit a finite set of sentences $\Sigma$ so that $T \vdash \varphi$ precisely if $\Sigma \vdash \varphi$ - indeed it is outright defined using such a set of sentences by Tarski.

What does not admit a finite equational axiomatization is the set of equations that hold in precisely the representable relation algebras, i.e. the ones where the underlying set is a family of binary relations on some set, and the operations are interpreted as the usual Boolean or relational operations. One can prove this using simple model-theoretic machinery without invoking Goedel.

I think this is what the authors mean when they write that "there is no finite complete axiomatisations for the whole calculus". In any case, this is the only thing established in the reference they give, which is good, since the common equational theory of representable relation algebras is recursively enumerable.

Zoltan A. Kocsis (Z.A.K.) (May 06 2024 at 00:41):

Since we're in a learning thread, let me mention a neat technique for proving the absence of finite axiomatizability.

If you already know some infinite axiomatization $\Sigma$ of your theory $T$, then it's usually easy to prove that $T$ admits no finite axiomatization. All you have to prove is that no finite subset of $\Sigma$ itself suffices to axiomatize $T$!

Why?

Well, assume that $T$ admits some finite axiomatization using axioms $A_1, A_2, \dots, A_n$, possibly unrelated to the axioms already in $\Sigma$. Then the conjunction $A_1, \wedge A_2, \wedge \dots \wedge A_n$ is enough to prove any sentence in the set $\Sigma$. And vice versa, there is a proof $p$ of the sentence $A_1, \wedge A_2, \wedge \dots \wedge A_n$ starting only from the axioms of $\Sigma$. But this latter proof $p$ is finite, so it uses only a finitely subset $\Sigma_p$ of the axioms in $\Sigma$.

So we have shown that a finite set of axioms $\Sigma_p \subseteq \Sigma$ is sufficient to prove $A_1, \wedge A_2, \wedge \dots \wedge A_n$, and in turn that the sentence $A_1, \wedge A_2, \wedge \dots \wedge A_n$ lets one prove any axiom in $\Sigma$ (and hence any consequence of the theory $T$). This means that whenever $T$ has _some_ finite axiomatization, then some $\Sigma_p$ is by itself sufficient to prove all the other axioms in $\Sigma$.

So all you have to prove is that no finite subset of $\Sigma$ itself suffices to axiomatize $T$ to conclude that $T$ has no finite axiomatization.

Exercise: use this observation to prove that the theory of fields in characteristic 0 (in e.g. the language $(+,-,\cdot,0,1)$) does not admit a finite axiomatization.

Kevin Carlson (May 06 2024 at 18:28):

Jacob Zelko said:

Second, Bonchi introduces this notion of "black and white" composition operators in his talk (I included a photo of that slide as follows):

image.png

This was in the context of first introducing the calculus of relations. He referenced that Tarski originated these notions but try as I might, I could not find reference to this notion of defining and constructing operators in this way. Is there a place I can learn more about these "black and white" structures and their origins?

The "white" structure is what most people would probably think of as the "ordinary" structure forming the bicategory or double category of relations: the composite of relations has $x S\circ R z$ if and only if for some $y,$ we have $x Ry$ and $ySz.$ So you can read more about this anywhere you want to read about relations in category theory; "Categories, Allegories" is one relevant text pretty narrowly focused there, while there's also the theory of cartesian bicategories and its generalization to double categories with finite products that my colleague Evan Patterson has been writing about recently.

Kevin Carlson (May 06 2024 at 18:29):

The "black" structure is formally dual to the "white" structure in that the "black" composite of two relations is the complement of the "white" composite of their complements, so we have $x S\bullet R z$ if for all $y,$ either $x R y$ or $y S z.$

Kevin Carlson (May 06 2024 at 18:30):

I don't think there's a whole lot of literature directly about it since it's kind of weird and can be defined in terms of the more naturally useful white structure.

Kevin Carlson (May 06 2024 at 18:36):

Jacob Zelko said:

After the calculus of neo-Peircean relations is introduced, Bonchi introduces these two constants called copier's and discard-er's. It seems like a copier simply creates a set of tuples where all values in each element are the same? Am I reading that right? Is that what is meant by "copier"? And similarly, for discards, is the big idea that they are "discarding" some information from the set? The discard constant is the more confusing of the two for me.

image.png

Generally, a "copy" map is a map $A\to A\otimes A$ and a "discard" map, a map $A\to I$, in some monoidal category, together making $A$ into a commutative comonoid. We can interpret copying as duplicating a variable of type $A$ and of discarding as throwing that variable away (it could be nice to think about why any reasonable copying and discarding operations should satisfy the axioms of a commutative comonoid.) This interpretation is apparent in the case at hand: as you say, the white copy map simply relates any $x$ to the duplicate $(x,x),$ for instance. Categories admitting copy and discard maps for all objects are, imaginatively, called copy-discard categories. It's critical that the copy-discard maps are not natural transformations, or in other words not every map in a CD-category is a homomorphism of commutative comonoids. There's an important theorem of Fox that says that, in fact, a CD-category which is "homomorphic" in this sense is just a cartesian monoidal category! So the category of (white) relations is a non-homomorphic CD-category; other examples come from categorical probability theory.

Jacob Zelko (May 06 2024 at 18:45):

(Just a quick aside to folks that I am busy today but am planning on picking back up this awesome conversation tomorrow! Just wanted to give a warm thanks to everyone who has posted so far -- the thoughts are fascinating!)

David Corfield (May 07 2024 at 06:33):

Evan Washington said:

Also note that Quine's predicate functor logic (another attempt to algebraicize first order logic) has nothing to do with functors or adjoints, but is just an unfortunate coincidence of terminology.

Presumably because of the common borrowing of 'functor' by Quine and Mac Lane from Carnap. Here's Mac Lane reviewing work by Carnap and mentioning functors in the latter's sense.