The undecidability of second order multiplicative linear logic (Q1917079): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1006/inco.1996.0019 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1966857180 / rank | |||
Normal rank |
Latest revision as of 20:42, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The undecidability of second order multiplicative linear logic |
scientific article |
Statements
The undecidability of second order multiplicative linear logic (English)
0 references
5 December 1996
0 references
The authors show that the multiplicative fragment of second-order propositional linear logic is undecidable. In referring to linear logic fragments, we use the standard conventions: M stands for multiplicatives, A for additives, E for exponentials, 1 for first order quantifiers, 2 for second-order propositional quantifiers, and I for the intuitionistic version. Decision problems for propositional (quantifier-free) linear logic were first studied by \textit{P. Lincoln}, \textit{J. Mitchell}, \textit{A. Scedrov}, and \textit{N. Shankar} [Ann. Pure Appl. Logic 56, 239-311 (1992; Zbl 0768.03003)]. They showed that full propositional linear logic is undecidable and that MALL is PSPACE-complete. The NP-completeness of MLL has been obtained by \textit{M. I. Kanovich} [Ann. Pure Appl. Logic 69, 195-241 (1994; Zbl 0812.03007)]. Related results have been obtained by Lincoln, Scedrov, Shankar, and Winkler. \textit{G. Amiot} showed the undecidability of MLL12 and MALL12 with function symbols [PhD. thesis, University of Paris 7 (1994)]. More recently, \textit{P. Lincoln}, \textit{A. Scedrov}, and \textit{N. Shankar} showed the undecidability of IMLL2 and IMALL2, and the undecidability of MLL12 and MALL12 without function symbols [Proc. 10th Annual IEEE Symp. on Logic in Computer Science, San Diego, California, 476-485 (1995)]. The present author then proved the undecidability of MALL2 [J. Symb. Logic 61, No. 2, 541-548 (1996)]. To establish the undecidability of MLL2, the authors combine the key ideas of the last two papers: an encoding of contraction using second-order quantifiers instead of exponentials (by Lincoln, Scedrov, and Shankar), and the use of the phase semantics to show that the counter machines are faithfully encoded into the logic (by Lafont). Because of the absence of additives, the encoding is a bit more complicated than in the previous papers.
0 references
phase semantics
0 references
multiplicative fragment of second-order propositional linear logic
0 references
undecidability
0 references
counter machines
0 references