The finite model property for various fragments of linear logic (Q4382470)

This paper proposes an elegant approach to the decision problems for various fragments of propositional linear logic (LL), which makes use of phase semantics. Phase spaces are the analogue of boolean algebras for classical logic: a formula \(A\) is provable in LL iff it is satisfied by every phase model. Propositional classical logic (and similarly propositional intuitionistic logic) satisfies a ``finite model property'': a formula \(A\) is provable iff it is satisfied by every finite boolean model. This entails that propositional classical logic is decidable. The main idea of the paper is to apply this method (just substitute ``boolean model'' by ``phase model'') to show the decidability of various fragments of LL. The author proves the finite model property for multiplicative and additive LL (MALL) and for affine LL, that is LL with weakening (LLW). This gives a new (rather simple) and uniform proof of decidability for MALL and LLW. It is also shown that the finite phase semantics is not complete for multiplicative and exponential linear logic (MELL), for which the decision problem is still an open question.