A Substructural View of Multilattice Logic
Norihiro Kamide
In this study, a new logic called the linear multilattice logic (LMLn) is introduced as one-sided sequent calculus. This logic is regarded as a substructural refinement of Shramko’s multilattice logic. Theorems for embedding LMLn into a one-sided sequent calculus for classical linear logic and vice versa are proved. The cut-elimination theorem for LMLn is shown. Phase semantics is introduced for LMLn, and the completeness theorem with respect to this semantics is proved. Similar results are also shown for the logic that is obtained from LMLn by adding the structural rules of weakening and contraction.
Keywords: Multilattice logic, multilattice, phase semantics, sequent calculus, substructual logic, cut-elimination theorem, completeness theorem.