Undecidability of Multiplicative Subexponential Logic

TL;DR

This paper demonstrates that extending multiplicative linear logic with certain subexponentials leads to undecidability by encoding the halting problem for two register Minsky machines.

Contribution

It proves the undecidability of a specific extension of multiplicative linear logic with subexponentials, highlighting the limits of decidability in this logical framework.

Findings

Encoding of the halting problem for Minsky machines

Undecidability result for extended multiplicative linear logic

Identification of conditions leading to undecidability

Abstract

Subexponential logic is a variant of linear logic with a family of exponential connectives--called subexponentials--that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that classical propositional multiplicative linear logic extended with one unrestricted and two incomparable linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable.