Title: The finite model property for various fragments of linear logic
Abstract: To show that a formula A is not provable in propositional classical logic, it suffices to exhibit a finite boolean model which does not satisfy A . A similar property holds in the intuitionistic case, with Kripke models instead of boolean models (see for instance [11]). One says that the propositional classical logic and the propositional intuitionistic logic satisfy a finite model property . In particular, they are decidable: there is a semi-algorithm for provability (proof search) and a semi-algorithm for non provability (model search). For that reason, a logic which is undecidable, such as first order logic, cannot satisfy a finite model property. The case of linear logic is more complicated. The full propositional fragment LL has a complete semantics in terms of phase spaces [2, 3], but it is undecidable [9]. The multiplicative additive fragment MALL is decidable, in fact PSPACE-complete [9], but the decidability of the multiplicative exponential fragment MELL is still an open problem. For affine logic , that is, linear logic with weakening, the situation is somewhat better: the full propositional fragment LLW is decidable [5]. Here, we show that the finite phase semantics is complete for MALL and for LLW , but not for MELL . In particular, this gives a new proof of the decidability of LLW . The noncommutative case is mentioned, but not handled in detail.
Publication Year: 1997
Publication Date: 1997-12-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 54
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot