The undecidability theorem for the Horn-like fragment of linear logic (Revisited)

Abstract

There has been an increased interest in the decision problems for linear logic and its fragments. Here, we give a fully self-contained, easy-to-follow, but fully detailed, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, which is accessible to a wide range of people. Namely, we show that there is a direct correspondence between terminated computations of a Minsky machine M and cut-free linear logic derivations for a Horn-like sequent of the form

\begin{equation*} \bang{\Phi_M},\ l_1 \vdash l_0, \end{equation*}

where Φ_M consists only of Horn-like implications of the following simple forms

\begin{equation*} (l \llto l'),\ \ ((l\otimes r) \llto l'),\ \ (l\llto (r\otimes l')),\ \ and \ \ (l\llto (l'\oplus l'')), \end{equation*}

where l₁, l₀, l, l′, l″ and r stand for literals.

Neither negation, nor &, nor constants, nor embedded implications/bangs are used here.

Furthermore, our particular correspondence constructed above provides decidability for each of the Horn-like fragments whenever we confine ourselves to any two forms of the above Horn-like implications, along with the complexity bounds that come from the proof.