The Undecidability of Second Order Linear Logic without Exponentials
Lafont, Yves
J. Symbolic Logic, Tome 61 (1996) no. 1, p. 541-548 / Harvested from Project Euclid
Recently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.
Publié le : 1996-06-14
Classification: 
@article{1183745013,
     author = {Lafont, Yves},
     title = {The Undecidability of Second Order Linear Logic without Exponentials},
     journal = {J. Symbolic Logic},
     volume = {61},
     number = {1},
     year = {1996},
     pages = { 541-548},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745013}
}
Lafont, Yves. The Undecidability of Second Order Linear Logic without Exponentials. J. Symbolic Logic, Tome 61 (1996) no. 1, pp.  541-548. http://gdmltest.u-ga.fr/item/1183745013/