Multirole logic

We formulate multirole logic as a new form of logic and naturally generalize Gentzen's celebrated result of cut-elimination between two sequents into one between multiple sequents. While the first and foremost inspiration for multirole logic came to us during a study on multiparty session types in distributed programming, it seems natural in retrospective to introduce multirole logic by exploring the well-known duality between conjunction and disjunction in classical logic. Let R0 be a (possibly infinite) underlying set of integers, where each integer is referred to as a role. In multirole logic, each formula A can be annotated with a set R of roles to form the i-formula [A]_R. For each ultrafilter U on the power set of R0, there is a (binary) logical connective \land_U such that [A_1\land_U A_2]_R is interpreted as the conjunction (disjunction) of [A_1]_R and [A_2]_R if R is in U (R is not in U). Furthermore, the notion of negation is generalized to endomorphisms on R0. We formulate both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents can be eliminated