2025/08/31 by Jun Suzuki, Katsuhiko Sano, Suzuki, Jun +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2509.00644
openalex publication_date 2025/08/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The goal of this paper is to establish that it remains undecidable whether a sequent is provable in two systems in which a weakening rule for an exponential modality is completely omitted from classical propositional linear logic CLL introduced by Girard (1987), which is shown to be undecidable by Lincoln et al. (1992). We introduce two logical systems, CLLR and CLLRR. The first system, CLLR, is obtained by omitting the weakening rule for the exponential modality of CLL. The system CLLR has been studied by several authors, including Meliès-Tabareau (2010), but its undecidability was unknown. This paper shows the undecidability of CLLR by reducing it to the undecidability of CLL, where the units 1 and \bot play a crucial role in simulating the weakening rule. We also omit these units from the syntax and inference rules of CLLR in order to define the second system, CLLRR. The undecidability of CLLRR is established by showing that the system can simulate any two-counter machine proposed by Minsky (1961).