×

The finite model property for various fragments of linear logic. (English) Zbl 0897.03010

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.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03B25 Decidability of theories and sets of sentences
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/0168-0072(92)90075-B · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B
[2] DOI: 10.1006/inco.1996.0019 · Zbl 0852.03003 · doi:10.1006/inco.1996.0019
[3] The undecidability of second order linear logic without exponentials 61 pp 541– (1996)
[4] Studies in logic and the foundations of mathematics 121 (1988)
[5] Advances in linear logic 222 pp 1– (1995)
[6] DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[7] Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic 56 pp 1403– (1991) · Zbl 0746.03044
[8] Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California (1995)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.