Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2509.00644 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
Tabla de Contenidos:
- 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ès-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).