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: deprecated: logic

Topic: category of sequents?

Shea Levy (Oct 13 2020 at 13:12):

In learning about the sequent calculus, it struck me that that the identity inference rule (for any formula A, we have A ⊢ A) and cut rule (for any finite formula sequences Γ, Δ, Σ, and Π and formula A, if we have Γ ⊢ Δ, A and A, Σ ⊢ Π then we have Γ, Σ ⊢ Δ, Π) look something like identity and composition if you squint. Is there a category here? At first I was thinking the arrows would be any sequent, with the domain being the first formula on the LHS and the codomain being the last formula on the RHS, but then I'm not sure how to deal with sequents like ⊥ ⊢

Shea Levy (Oct 13 2020 at 13:12):

(ironically I'm learning about sequent calculus for a first-order formalization of category theory itself)

James Wood (Oct 13 2020 at 13:18):

Polycategories are to (sequent calculus, identity, cut) as multicategories are to (natural deduction, variable, simultaneous substitution), so that's probably a good point of comparison.

Shea Levy (Oct 13 2020 at 13:22):

Awesome, thank you!

James Wood (Oct 13 2020 at 13:25):

It must be extremely fiddly to prove, but I guess cut is associative with respect to the equational theory (of any reasonable logic).

Shea Levy (Oct 13 2020 at 13:48):

From https://ncatlab.org/nlab/show/polycategory#relation_to_properads_and_props it looks like we can compose along any one object regardless of its position in the list, but in sequent calculus that requires exchange, right? Are there "ordered" polycategories?

Nathanael Arkor (Oct 13 2020 at 13:54):

Sequent calculi would usually correspond to symmetric polycategories, which admit exchange.

Nathanael Arkor (Oct 13 2020 at 13:54):

If you don't have exchange, then you consider ordinary/planar/nonsymmetric polycategories.

Shea Levy (Oct 13 2020 at 13:55):

Got it, thanks!

sarahzrf (Oct 13 2020 at 15:38):

the nlab page probably says this, but for the record, the "structured category" notion corresponding to symmetric polycats is gonna be star-autonomous categories

sarahzrf (Oct 13 2020 at 15:39):

that is to say: star-autonomous categories are to symmetric polycategories as symmetric monoidal categories are to symmetric multicategories

sarahzrf (Oct 13 2020 at 15:40):

oh wait sorry :sweat_smile: i think that's actually wrong, ignore me

Valeria de Paiva (Oct 13 2020 at 18:35):

Shea Levy said:

In learning about the sequent calculus, it struck me that that the identity inference rule (for any formula A, we have A ⊢ A) and cut rule (for any finite formula sequences Γ, Δ, Σ, and Π and formula A, if we have Γ ⊢ Δ, A and A, Σ ⊢ Π then we have Γ, Σ ⊢ Δ, Π) look something like identity and composition if you squint. Is there a category here? At first I was thinking the arrows would be any sequent, with the domain being the first formula on the LHS and the codomain being the last formula on the RHS, but then I'm not sure how to deal with sequents like ⊥ ⊢

hi, this was the original insight of Lambek in
Lambek, Joachim (1969). "Deductive systems and categories I and II. Standard constructions and closed categories". Lecture Notes in Mathematics. 86. Berlin, Heidelberg: Springer Berlin Heidelberg. pp. 76–122. doi:10.1007/bfb0079385. ISBN 978-3-540-04605-9. ISSN 0075-8434.

Alex Gryzlov (Oct 14 2020 at 14:47):

I think this is pretty much what categorical logic studies. Take a look at @Mike Shulman's http://mikeshulman.github.io/catlog/catlog.pdf book.

Morgan Rogers (he/him) (Oct 14 2020 at 14:48):

What "this" are you referring to?

Alex Gryzlov (Oct 14 2020 at 14:49):

categories that correspond to various proof systems (and vice versa)

Fawzi Hreiki (Oct 14 2020 at 14:56):

The simplest case is just posets. Then you can interpret the objects as propositions and the morphisms as entailments

Fawzi Hreiki (Oct 14 2020 at 14:57):

The terminal object is truth, the initial object is falsity, product is and, sum is or, exponentiation is implication, etc

Fawzi Hreiki (Oct 14 2020 at 14:59):

To extend this you basically have two approaches - propositions as types, which is what is done with Lambda calculus and dependent type theory, or logic over a type theory which is what is done with hyperdoctrines

Fawzi Hreiki (Oct 14 2020 at 15:00):

The subobject fibration which sends each object to its poset of subjects is just a special case of this second approach

Fawzi Hreiki (Oct 14 2020 at 15:00):

Lawvere’s Adjointness in Foundations is a good early reference for this kind of thinking

Robert Seely (Oct 14 2020 at 17:50):

I guess this is still a work in progress - e.g. Chapter 3 seems to be missing ... (I would notice that, wouldn't I?)

Alex Gryzlov (Oct 14 2020 at 17:54):

yeah, 5 and 6 are also not there

Alex Gryzlov (Oct 14 2020 at 17:57):

There are some updates in https://github.com/mikeshulman/catlog which are not in the pdf (which seems to be from ~mid 2016), so I guess one should compile those tex files manually for the latest version

Dan Doel (Oct 14 2020 at 18:08):

They're still excellent 'notes' regardless.

Fawzi Hreiki (Oct 14 2020 at 20:25):

Yeah they are great. I like that they're much more semantically oriented than the usual treatments.

Mike Shulman (Oct 14 2020 at 20:56):

I'm glad y'all like them. Sadly the unwritten chapter 3 is the one of relevance to the OP here though...

Alex Gryzlov (Oct 16 2020 at 15:20):

By the way, I've built the latest version manually, if somebody wants it: catlog.pdf

Alex Gryzlov (Oct 16 2020 at 15:21):

It has some parts of chapter 3

Dan Doel (Oct 16 2020 at 15:32):

Incidentally, if someone wants to see another classical-ish type theory with sequents, I'd recommend Compiling with Classical Connectives. It's a lot more complicated than just classical logic to keep things computationally well-behaved, though.

GhaS Shee (Mar 07 2021 at 10:05):

I am now reading @Mike Shulman 's catlog.pdf at chapter 2 with remembering section 1.4 (referring the rule lists in p51).
I have a question around the rule $<π_1(P),π_2(P)>\ \ \ \equiv \ \ P$.
I would like to introduce this judgmental equality formally.
To do that, I think of a category, but I could not construct a 2-morphism corresponding to the rule.

So, my question is "Is there a way of formalizing this rule in a category rather than in a multicategory introduced in chapter 2?"

Nathanael Arkor (Mar 07 2021 at 14:08):

This rule (the $\eta$-rule for products) corresponds to the uniqueness of the universal property of a binary product in a category. You can check that the morphisms represented by the LHS and by the RHS both satisfy the condition to be the mediating morphism for the product, implying their equality.

GhaS Shee (Mar 07 2021 at 15:01):

@Nathanael Arkor
Ah, thanks. exactly.