# Undecidability of Linear Logics without Weakening

## TL;DR

This paper proves that determining provability in certain linear logic systems without weakening rules remains undecidable, extending known results to new variants by reducing from established undecidable systems.

## Contribution

It introduces two new logical systems, $ extbf{CLLR}$ and $ extbf{CLLRR}$, and proves their undecidability by reduction from classical linear logic and two-counter machines.

## Key findings

- $ extbf{CLLR}$ is undecidable, extending previous results.
- $ extbf{CLLRR}$ is undecidable via simulation of two-counter machines.
- Undecidability holds even without units $ extbf{1}$ and $ot$.

## Abstract

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 $\mathbf{CLL}$ introduced by Girard (1987), which is shown to be undecidable by Lincoln et al. (1992). We introduce two logical systems, $\mathbf{CLLR}$ and $\mathbf{CLLRR}$. The first system, $\mathbf{CLLR}$, is obtained by omitting the weakening rule for the exponential modality of $\mathbf{CLL}$. The system $\mathbf{CLLR}$ has been studied by several authors, including Meli\`es-Tabareau (2010), but its undecidability was unknown. This paper shows the undecidability of $\mathbf{CLLR}$ by reducing it to the undecidability of $\mathbf{CLL}$, where the units $\mathbf{1}$ and $\bot$ play a crucial role in simulating the weakening rule. We also omit these units from the syntax and inference rules of $\mathbf{CLLR}$ in order to define the second system, $\mathbf{CLLRR}$. The undecidability of $\mathbf{CLLRR}$ is established by showing that the system can simulate any two-counter machine proposed by Minsky (1961).