3
$\begingroup$

Define a structure made of objects $A, B, C, \dots$ and morphisms $f, g, \dots$. Each morphism has a collection of domain objects and codomain objects. For simplicity we consider the domains and codomains as unordered sets. We require that

  • For each $A$ there exists an $f : A \to A$.
  • For every $f:B_1, B_2, \dots \to C, D_1, D_2,\dots$ and $g: C, F_1, F_2, \dots \to H_1, H_2,\dots$, there exists a morphism $g \circ f : B_1, B_2, F_1, F_2 \dots \to D_1, D_2, H_1, H_2\dots$.
  • For composable $f, g, h$, $(f\circ g) \circ h = f \circ (g \circ h)$.

Note that this is richer than sequent logics, because it is sort of proof relevant; the same sequent have different proofs. If we impose that for each $f,g:\Gamma \to\Delta$ we have $f=g$, then we recover the usual sequent logic, without any connectives. (Of course, this makes axiom three trivial.)

We can then define connectives with universal properties, just as we define products, coproducts and equalizers etc.

My question is: is there any existing literature on such a structure? What's the name for it? Where can I read more about it?

$\endgroup$
6
  • 1
    $\begingroup$ It is not clear what you mean by the commas on the two sides of the sequent. If it's conjunction or product on both sides, the corresponding idea is a multicategory and is fairly widely used. However, traditionally comma on the right of a sequent means disjunction; if you clarify that in your question, I or someone might look up some references for categorical work using that idea. $\endgroup$ Sep 4 '21 at 13:33
  • $\begingroup$ @PaulTaylor The comma doesn't mean anything on its own. Its meaning is defined with the second axiom, analogous to the cut rule. But its intended semantics is indeed conjunction on the left and disjunction on the right. $\endgroup$
    – Trebor
    Sep 4 '21 at 13:35
  • 1
    $\begingroup$ OK I have seen systems of this nature, but as a tool used to capture the behaviour of some particular mathematicsl setting, rather than as a widespread treatment of logic. (Sorry for the vague wording.) I suggest doing a web search for eg "sequent category" to see if there is something similar to whatever your motivation is, or spelling that out in more detail. $\endgroup$ Sep 4 '21 at 13:45
  • 1
    $\begingroup$ ncatlab.org/nlab/show/polycategory ? $\endgroup$ Sep 4 '21 at 16:08
  • 1
    $\begingroup$ @ReidBarton Yes, that's exactly what I want. Wuld you like to write an answer so that I can accept it? $\endgroup$
    – Trebor
    Sep 4 '21 at 17:13
6
$\begingroup$

It sounds like you want the notion of a polycategory.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.