The undecidability theorem for the Horn-like fragment of linear logic (Revisited).
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds.
Later an alternative proof for the LL undecidability has been developed based on simulation Minsky machines in linear logic:
Kanovich, M. (1995). The direct simulation of Minsky machines in linear logic. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Notes, volume 222, Cambridge University Press 123–145.
Notice that this direct simulation approach has been successfully applied for a large number
of formal systems with resolving a number of open problems in computer science
and even computational linguistics, e.g.,
James Brotherston, Max I. Kanovich: Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61(2): 14:1-14:43 (2014),
Max Kanovich, Stepan Kuznetsov, Andre Scedrov: Undecidability of the Lambek Calculus with a Relevant Modality. FG 2016: 240-256.
Nevertheless, recently the undecidability of linear logic is questioned by some people. They claim that
they have found lacunae in the LMSS 1992 paper, and, moreover, they have a proof that propositional linear logic is decidable!!!
I have been asked to submit a paper, as clear as possible, to the Journal, in order to sort out such a confusing problem, once and for all.
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, the proof 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
\Phi_M, l1 |- l0
where \Phi_M consists only of Horn-like implications of the very simple forms.
Neither negation, nor &, nor constants, nor embedded implications/bangs are used here.
Furthermore, our particular correspondence constructed above provides decidability for
some smaller Horn-like fragments along with the complexity bounds that come from the proof.