Multirole Logic (Extended Abstract)

TL;DR

This paper introduces multirole logic, a new logical framework where conjunction, disjunction, and negation are interpreted through ultrafilters and endomorphisms on roles, extending classical and linear logic with a multiparty cut-elimination property.

Contribution

It formalizes multirole logic and linear multirole logic as generalizations of classical logic, providing a novel interpretation and a multiparty cut-elimination theorem.

Findings

Established a formal framework for multirole logic and linear multirole logic.

Proved a multiparty cut-elimination theorem extending Gentzen's result.

Provided a filter-based interpretation for intuitionism within multirole logic.

Abstract

We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on the power set of some underlying set (of roles) and the notion of negation is generalized to endomorphisms on this underlying set. We formalize both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively, and also present a filter-based interpretation for intuitionism in multirole logic. 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 (as a generalization of a (binary) cut involving exactly two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen.