Modalities in lattice-R

  • Modalities in lattice-R

  • Author(s) / Creator(s)
  • This paper considers modalities added to the relevance logic LR (lattice-R), which is R with the distributivity of conjunction and disjunction omitted. First, the modalities are defined from the Ackermann constants and the lattice connectives. Then, we introduce modalities as primitives equipped with some fairly usual properties. We also consider some other logics in the neighborhood. For each logic, including classical linear logic, we prove decidability. Lincoln, Mitchell, Scedrov, and Shankar (1992) claimed to have proved classical linear logic undecidable. We examine their work and find that their paper does not contain a proof of the admissibility of the cut rule, which would be essential for their claims to hold. Furthermore, according to their interpretation of proofs in linear logic, computations that lead to a dead-end state are not considered, unlike computations from inaccessible states that are included. The same problem with the direction of a proof vs the direction of a computation appears in all other publications that claim undecidability, including Kanovich (2016).

  • Date created
  • Subjects / Keywords
  • Type of Item
  • DOI
  • License
    Attribution-NonCommercial-NoDerivatives 4.0 International