https://hal.inria.fr/hal-01870148Strassburger, LutzLutzStrassburgerPARSIFAL - Proof search and reasoning with logic specifications - LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau] - X - École polytechnique - CNRS - Centre National de la Recherche Scientifique - Inria Saclay - Ile de France - Inria - Institut National de Recherche en Informatique et en AutomatiqueOn the Decision Problem for MELLHAL CCSD2018decidabilitylinear logicMELL[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]Straßburger, Lutz - La structure fine des systèmes formels de démonstration et leurs interprétations calculatoires - - FISP2015 - ANR-15-CE25-0014 - AAPG2015 - VALID - 2018-09-07 11:04:212023-03-24 14:53:082018-09-07 11:27:29enReportsapplication/pdf1In this short paper I will exhibit several mistakes in the recent attempt by Bimbò to prove the decidability of the multiplicative exponential fragment of linear logic (MELL). In fact, the main mistake is so serious that there is no obvious fix, and therefore the decidability of MELL remains to be an open problem. As a side effect, this paper contains a complete (syntactic) proof of the decidability of the relevant version of MELL (called RMELL in this paper), that is the logic obtained from MELL by replacing the linear logic contraction rule by a general unrestricted version of the contraction rule. This proof can also be found (with a small error) in Bimbò's work, and a semantic proof has been given by Okada and Terui.