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?

Improve this question
$\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$
    – Paul Taylor
    Commented Sep 4, 2021 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
    Commented Sep 4, 2021 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$
    – Paul Taylor
    Commented Sep 4, 2021 at 13:45
  • 1
    $\begingroup$ ncatlab.org/nlab/show/polycategory ? $\endgroup$
    – Reid Barton
    Commented Sep 4, 2021 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
    Commented Sep 4, 2021 at 17:13

1 Answer 1

Reset to default
6
$\begingroup$

It sounds like you want the notion of a polycategory.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .